#lang pie

;; Decidable
(claim Dec
  (-> U U))
(define Dec
  (lambda (X)
    (Either X (-> X Absurd))))

;; +
(claim step-+
  (-> Nat Nat))
(define step-+
  (lambda (+_n-1)
    (add1 +_n-1)))

(claim +
  (-> Nat Nat Nat))
(define +
  (lambda (n j)
    (iter-Nat n
      j
      step-+)))

;; =consequence
(claim =consequence
  (-> Nat Nat
      U))
(define =consequence
  (lambda (n j)
    (which-Nat n
      (which-Nat j
        Trivial
        (lambda (j-1)
          Absurd))
      (lambda (n-1)
        (which-Nat j
          Absurd
          (lambda (j-1)
            (= Nat n-1 j-1)))))))

;; =consequence-same
(claim =consequence-same
  (Pi ((n Nat))
    (=consequence n n)))
(define =consequence-same
  (lambda (n)
    (ind-Nat n
      (lambda (k)
        (=consequence k k))
      sole
      (lambda (n-1 =consequence_n-1)
        (same n-1)))))

;; use-Nat=
(claim use-Nat=
  (Pi ((n Nat)
       (j Nat))
    (-> (= Nat n j)
        (=consequence n j))))
(define use-Nat=
  (lambda (n j)
    (lambda (n=j)
      (replace n=j
        (lambda (k)
          (=consequence n k))
        (=consequence-same n)))))

;; zero-not-add1
(claim zero-not-add1
  (Pi ((n Nat))
    (-> (= Nat zero (add1 n))
        Absurd)))
(define zero-not-add1
  (lambda (n)
    (use-Nat= zero (add1 n))))

;; <=
(claim <=
  (-> Nat Nat U))
(define <=
  (lambda (x y)
    (Sigma ((z Nat))
      (= Nat (+ x z) y))))

;; <=consequence
(claim <=consequence
  (-> Nat Nat
      U))
(define <=consequence
  (lambda (n j)
    (which-Nat n
      Trivial
      (lambda (n-1)
        (which-Nat j
          Absurd
          (lambda (j-1)
            (<= n-1 j-1)))))))

;; use-Nat<=
(claim mot-use-Nat<=
  (Pi ((n Nat)
       (k Nat))
    U))
(define mot-use-Nat<=
  (lambda (n)
    (lambda (k)
      (Pi ((j Nat)
           (n<=j (<= n j)))
        (<=consequence k j)))))

(claim step-use-Nat<=
  (Pi ((n Nat)
       (n-1 Nat))
    (-> (mot-use-Nat<= n n-1)
        (mot-use-Nat<= n (add1 n-1)))))
(define step-use-Nat<=
  (lambda (n)
    (lambda (n-1 use-Nat<=_n-1)
      (lambda (j n<=j)
        (ind-Nat j
          (lambda (k)
            (which-Nat k
              Absurd
              (lambda (j-1)
                (<= n-1 j-1))))
          (use-Nat= (+ n (car n<=j)) j (cdr n<=j)) ; stuck here: n>0 j-0 n<=j why use-Nat= can't use?
          TODO)))
    ))

(claim use-Nat<=
  (Pi ((n Nat)
       (j Nat))
    (-> (<= n j)
        (<=consequence n j))))
(define use-Nat<=
  (lambda (n j)
    (lambda (n<=j)
      ((ind-Nat n
         (mot-use-Nat<= n)
         (the (Pi ((j Nat)
                   (n<=j (<= n j)))
                Trivial) (lambda (j n<=j) sole)) 
         (step-use-Nat<= n)) j n<=j))))

;; add1-not-<=zero
(claim add1-not-<=zero
  (Pi ((n Nat))
    (-> (<= (add1 n) zero)
        Absurd)))
(define add1-not-<=zero
  (lambda (n)
    (use-Nat<= (add1 n) zero)))

;; nat<=?
(claim mot-nat<=?
  (-> Nat U))
(define mot-nat<=?
  (lambda (k)
    (Pi ((j Nat))
      (Dec (<= k j)))))

(claim zero<=?
  (Pi ((j Nat))
    (Dec (<= zero j))))
(define zero<=?
  (lambda (j)
    (left (cons j (same j)))))

(claim step-nat<=?
  (Pi ((n-1 Nat))
    (-> (mot-nat<=? n-1)
        (mot-nat<=? (add1 n-1)))))
(define step-nat<=?
  (lambda (n-1 nat<=?_n-1)
    (lambda (j)
      (ind-Nat j
        (lambda (k)
          (Dec (<= (add1 n-1) k)))
        (right (add1-not-<=zero n-1)) ; embeded a (<= (add1 n-1) 0) -> Absurd
        TODO))))

(claim nat<=?
  (Pi ((n Nat)
       (j Nat))
    (Dec (<= n j))))
(define nat<=?
  (lambda (n j)
    ((ind-Nat n
       mot-nat<=?
       zero<=?
       step-nat<=?)
     j)))