#lang pie

;;;;;;;;; '+'
(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-+)))

;;;;;;;;; '*'
(claim step-*
  (-> Nat Nat Nat
    Nat))
(define step-*
  (lambda (j n-1 *n-1)
    (+ j *n-1)))

(claim *
  (-> Nat Nat
      Nat))
(define *
  (lambda (n j)
    (rec-Nat n
      zero
      (step-* j))))

;;;;;;;;; some useful numbers
(claim  one Nat)
(define one (add1 zero))
(claim  two Nat)
(define two (+ one one))
(claim  three Nat)
(define three (+ one two))
(claim  four Nat)
(define four (+ one three))
(claim  five Nat)
(define five (+ one four))

;;;;;;;;; incr
(claim incr
  (-> Nat
      Nat))
(define incr
  (lambda (n)
    (iter-Nat n
      one
      (+ one))))

;;;;;;;;; some misc defintions
(claim vegetables (Pair Atom Atom))
(define vegetables (cons 'celery 'carrot))

(claim sandwich
  (-> Atom
      Atom))
(define sandwich
  (lambda (which-sandwich)
    'delicious))

(claim expectations (List Atom))
(define expectations
  (:: 'cooked
    (:: 'eaten
      (:: 'tried-cleaning
        (:: 'understood
          (:: 'slept nil))))))

(claim more-expectations (Vec Atom 3))
(define more-expectations
  (vec:: 'need-induction
    (vec:: 'understood-induction
      (vec:: 'built-function vecnil))))

(claim rugbrod (List Atom))
(define rugbrod
  (:: 'rye-flour
    (:: 'rye-kernels
      (:: 'water
        (:: 'sourdough
          (:: 'salt nil))))))

(claim toppings (List Atom))
(define toppings
  (:: 'potato
    (:: 'butter nil)))

(claim condiments (List Atom))
(define condiments
  (:: 'chives
    (:: 'mayonnaise nil)))

(claim treats (Vec Atom 3))
(define treats
  (vec:: 'kanelbullar
    (vec:: 'plattar
      (vec:: 'prinsesstarta vecnil))))

(claim drinks (List Atom))
(define drinks
  (:: 'coffee
    (:: 'cocoa nil)))

(claim menu (Vec Atom 4))
(define menu
  (vec:: 'ratatouille
    (vec:: 'kartoffelmad
      (vec:: (sandwich 'hero)
        (vec:: 'prinsesstarta vecnil)))))

;;;;;;;;; predecessor of a Nat
(claim pred
  (-> Nat
      Nat))
(define pred
  (lambda (n)
    (which-Nat n
      0
      (lambda (n-1)
        n-1))))

;;;;;;;;; pear maker and eliminator
(claim Pear U)
(define Pear (Pair Nat Nat))

(claim Pear-maker
  (Pi ((X U))
    U))
(define Pear-maker
  (lambda (X)
    (-> Nat Nat
        X)))

(claim elim-Pear
  (Pi ((X U))
    (-> Pear (Pear-maker X)
      X)))
(define elim-Pear
  (lambda (X pear maker)
    (maker (car pear) (cdr pear))))

;;;;;;;;; pearwise+
(claim pearwise+
  (-> Pear Pear
      Pear))
(define pearwise+
  (lambda (anjou bosc)
    (elim-Pear Pear anjou
      (lambda (a1 d1)
        (elim-Pear Pear bosc
          (lambda (a2 d2)
            (cons (+ a1 a2) (+ d1 d2))))))))

;;;;;;;;; gauss
(claim step-gauss
  (-> Nat Nat
      Nat))
(define step-gauss
  (lambda (n-1 gauss_n-1)
    (+ (add1 n-1) gauss_n-1)))

(claim gauss
  (-> Nat
      Nat))
(define gauss
  (lambda (n)
    (rec-Nat n
      0
      step-gauss)))

;;;;;;;;; define 'factorial'
(claim step-factorial
  (-> Nat Nat
      Nat))
(define step-factorial
  (lambda (n-1 factorial_n-1)
    (* (add1 n-1) factorial_n-1)))

(claim factorial
  (-> Nat
      Nat))
(define factorial
  (lambda (n)
    (rec-Nat n
      one
      step-factorial)))

;;;;;;;;; elim-Pair
(claim elim-Pair
  (Pi ((A U)
       (D U)
       (X U))
    (-> (Pair A D)
        (-> A D
            X)
        X)))
(define elim-Pair
  (lambda (A D X p f)
    (f (car p) (cdr p))))

;;;;;;;;; swap + flip
(claim swap
  (-> (Pair Nat Atom)
      (Pair Atom Nat)))
(define swap
  (lambda (p)
    (elim-Pair
      Nat Atom
      (Pair Atom Nat)
      p
      (lambda (a d)
        (cons d a)))))

(claim flip
  (Pi ((A U)
       (D U))
    (-> (Pair A D)
        (Pair D A))))
(define flip
  (lambda (A D p)
    (cons (cdr p) (car p))))

;;;;;;;;; kar + kdr
(claim kar
  (-> (Pair Nat Nat)
      Nat))
(define kar
  (lambda (p)
    (elim-Pair
      Nat Nat
      Nat
      p
      (lambda (a d)
        a))))

(claim kdr
  (-> (Pair Nat Nat)
      Nat))
(define kdr
  (lambda (p)
    (elim-Pair
      Nat Nat
      Nat
      p
      (lambda (a d)
        d))))

;;;;;;;;; twin
(claim twin
  (Pi ((Y U))
    (-> Y
      (Pair Y Y))))
(define twin
  (lambda (Y x)
    (cons x x)))

;;;;;;;;; List/length
(claim step-length
  (Pi ((E U))
    (-> E (List E) Nat
        Nat)))
(define step-length
  (lambda (E)
    (lambda (e es length_es)
      (add1 length_es))))

(claim length
  (Pi ((E U))
    (-> (List E)
        Nat)))
(define length
  (lambda (E es)
    (rec-List es
      0
      (step-length E))))

;;;;;;;;; List/append
(claim step-append
  (Pi ((E U))
    (-> E (List E) (List E)
        (List E))))
(define step-append
  (lambda (E)
    (lambda (e es append_es)
      (:: e append_es))))

(claim append
  (Pi ((E U))
    (-> (List E) (List E)
        (List E))))
(define append
  (lambda (E start end)
    (rec-List start
      end
      (step-append E))))

;;;;;;;;; List/snoc
(claim snoc
  (Pi ((E U))
    (-> (List E) E
        (List E))))
(define snoc
  (lambda (E es e)
    (append E es (:: e nil))))

;;;;;;;;; List/reverse
(claim step-reverse
  (Pi ((E U))
    (-> E (List E) (List E)
      (List E))))
(define step-reverse
  (lambda (E)
    (lambda (e es reverse_es)
      (snoc E reverse_es e))))

(claim reverse
  (Pi ((E U))
    (-> (List E)
        (List E))))
(define reverse
  (lambda (E es)
    (rec-List es
      (the (List E) nil)
      (step-reverse E))))

;;;;;;;;; laekkert
(claim kartoffelmad (List Atom))
(define kartoffelmad
  (append Atom
    (append Atom
      condiments toppings)
    (reverse Atom
      (:: 'plate
        (:: 'rye-bread nil)))))

;;;;;;;;; Vec/first-of-one/two
(claim first-of-one
  (Pi ((E U))
    (-> (Vec E 1)
        E)))
(define first-of-one
  (lambda (E es)
    (head es)))

(claim first-of-two
  (Pi ((E U))
    (-> (Vec E 2)
        E)))
(define first-of-two
  (lambda (E es)
    (head es)))

;;;;;;;;; Vec/first & Vec/rest
(claim first
  (Pi ((E U)
       (l Nat))
    (-> (Vec E (add1 l))
        E)))
(define first
  (lambda (E l es)
    (head es)))

(claim rest
  (Pi ((E U)
       (l Nat))
    (-> (Vec E (add1 l))
        (Vec E l))))
(define rest
  (lambda (E l es)
    (tail es)))

;;;;;;;;; Vec/last
(claim mot-last
  (-> U Nat
      U))
(define mot-last
  (lambda (E k)
    (-> (Vec E (add1 k))
        E)))

(claim base-last
  (Pi ((E U))
    (mot-last E zero)))
(define base-last
  (lambda (E es)
    (head es)))

(claim step-last
  (Pi ((E U)
       (l-1 Nat))
    (-> (mot-last E l-1)
        (mot-last E (add1 l-1)))))
(define step-last
  (lambda (E)
    (lambda (l-1 last_l-1)
      (lambda (es)
        (last_l-1 (tail es))))))

(claim last
  (Pi ((E U)
       (l Nat))
    (mot-last E l)))
(define last
  (lambda (E l)
    (ind-Nat l
      (mot-last E)
      (base-last E)
      (step-last E))))


;;;;;;;;; peas
(claim mot-peas (-> Nat U))
(define mot-peas
  (lambda (k)
    (Vec Atom k)))

(claim step-peas
  (Pi ((l-1 Nat))
    (-> (mot-peas l-1)
        (mot-peas (add1 l-1)))))
(define step-peas
  (lambda (l-1 peas_l-1)
    (vec:: 'pea peas_l-1)))

(claim peas
  (Pi ((how-many-peas Nat))
    (Vec Atom how-many-peas)))
(define peas
  (lambda (how-many-peas)
    (ind-Nat how-many-peas
      mot-peas
      vecnil
      step-peas)))

;;;;;;;;; also-rec-Nat
(claim also-rec-Nat
  (Pi ((X U))
    (-> Nat
        X
        (-> Nat X
            X)
        X)))
(define also-rec-Nat
  (lambda (X)
    (lambda (target base step)
      (ind-Nat target
        (lambda (k) X)
        base
        step))))

;;;;;;;;; Vec/drop-last
(claim mot-drop-last
  (-> U Nat
      U))
(define mot-drop-last
  (lambda (E k)
    (-> (Vec E (add1 k))
        (Vec E k))))

(claim base-drop-last
  (Pi ((E U))
    (mot-drop-last E zero)))
(define base-drop-last
  (lambda (E es)
    vecnil))

(claim step-drop-last
  (Pi ((E U)
       (l-1 Nat))
    (-> (mot-drop-last E l-1)
        (mot-drop-last E (add1 l-1)))))
(define step-drop-last
  (lambda (E l-1 drop-last_l-1)
    (lambda (es)
      (vec::
        (head es)
        (drop-last_l-1 (tail es))))))

(claim drop-last
  (Pi ((E U)
       (l Nat))
    (mot-drop-last E l)))
(define drop-last
  (lambda (E l)
    (ind-Nat l
      (mot-drop-last E)
      (base-drop-last E)
      (step-drop-last E))))

;;;;;;;;; proof for (+ 1 n) = (add1 n)
(claim +1=add1
  (Pi ((n Nat))
    (= Nat (+ 1 n) (add1 n))))
(define +1=add1
  (lambda (n)
    (same (add1 n))))

;;;;;;;;; proof for (+ incr n) = (add1 n)
(claim mot-incr=add1
  (-> Nat
      U))
(define mot-incr=add1
  (lambda (k)
    (= Nat (incr k) (add1 k))))

(claim base-incr=add1
  (= Nat (incr zero) (add1 zero)))
(define base-incr=add1
  (same (add1 zero)))

; for every Nat n
; if (incr n) equals (add1 n)
; then (incr (add1 n)) equals (add1 (add1 n))
(claim step-incr=add1
  (Pi ((n-1 Nat))
    (-> (= Nat
          (incr n-1)
          (add1 n-1))
        (= Nat
          (add1
            (incr n-1))
          (add1
            (add1 n-1))))))
(define step-incr=add1
  (lambda (n-1)
    (lambda (incr=add1_n-1)
      (cong incr=add1_n-1 (+ 1)))))

; using replace instead of cong
(claim step-incr=add1_replace_version
  (Pi ((n-1 Nat))
    (-> (= Nat           ; target
          (incr n-1)     ;   from
          (add1 n-1))    ;   to
      (= Nat             ; replace expressions's type
        (add1
          (incr n-1))
        (add1
          (add1 n-1))))))
(define step-incr=add1_replace_version
  (lambda (n-1 incr=add1_n-1)
    (replace incr=add1_n-1         ; given evidence
      (lambda (k)
        (= Nat
          (add1
            (incr n-1))
          (add1
            k)))                   ; mot
      (same (add1 (incr n-1))))))  ; base has type (mot from)

(claim incr=add1
  (Pi ((n Nat))
    (= Nat (incr n) (add1 n))))
(define incr=add1
  (lambda (n)
    (ind-Nat n
      mot-incr=add1
      base-incr=add1
      step-incr=add1)))

; using replace step's version
(claim incr=add1_replace_version
  (Pi ((n Nat))
    (= Nat (incr n) (add1 n))))
(define incr=add1_replace_version
  (lambda (n)
    (ind-Nat n
      mot-incr=add1
      base-incr=add1
      step-incr=add1_replace_version)))

;;;;;;;;; proof that (twice n) equals (double n)
(claim double
  (-> Nat
      Nat))
(define double
  (lambda (n)
    (iter-Nat n
      0
      (+ 2))))

(claim twice
  (-> Nat
      Nat))
(define twice
  (lambda (n)
    (+ n n)))

; begin lemma showing:
;   (+ n (add j)) equals (add1 (+ n j))
(claim mot-add1+=+add1
  (-> Nat Nat
      U))
(define mot-add1+=+add1
  (lambda (j k)
    (= Nat
      (add1 (+ k j))
      (+ k (add1 j)))))

(claim step-add1+=+add1
  (Pi ((j Nat)
       (n-1 Nat))
    (-> (mot-add1+=+add1 j n-1)
        (mot-add1+=+add1 j (add1 n-1)))))
(define step-add1+=+add1
  (lambda (j n-1 evidence_n-1)
    (cong evidence_n-1 (+ 1))))

(claim add1+=+add1
  (Pi ((n Nat)
       (j Nat))
    (mot-add1+=+add1 j n)))
(define add1+=+add1
  (lambda (n j)
    (ind-Nat n
      (mot-add1+=+add1 j)
      (same (add1 j))
      (step-add1+=+add1 j))))
; end lemma

(claim mot-twice=double
  (-> Nat
      U))
(define mot-twice=double
  (lambda (k)
    (= Nat
      (twice k)
      (double k))))

(claim step-twice=double
  (Pi ((n-1 Nat))
    (-> (mot-twice=double n-1)
        (mot-twice=double (add1 n-1)))))
(define step-twice=double
  (lambda (n-1 evidence_n-1)
    (replace (add1+=+add1 n-1 n-1)
      (lambda (k)
        (= Nat
          (add1 k)
          (add1
            (add1 (double n-1)))))
      (cong evidence_n-1 (+ 2)))))

(claim twice=double
  (Pi ((n Nat))
    (= Nat
       (twice n)
       (double n))))
(define twice=double
  (lambda (n)
    (ind-Nat n
      mot-twice=double
      (same zero)
      step-twice=double)))

;;;;;;;;; double-Vec & twice-Vec
(claim twice-Vec
  (Pi ((E U)
       (l Nat))
    (-> (Vec E l)
        (Vec E (twice l)))))

(claim mot-double-Vec
  (-> U Nat
      U))
(define mot-double-Vec
  (lambda (E k)
    (-> (Vec E k)
        (Vec E (double k)))))

(claim step-double-Vec
  (Pi ((E U)
       (l-1 Nat))
    (-> (mot-double-Vec E l-1)
        (mot-double-Vec E (add1 l-1)))))
(define step-double-Vec
  (lambda (E l-1 double-Vec_l-1)
    (lambda (es)
      (vec:: (head es)
        (vec:: (head es)
          (double-Vec_l-1 (tail es)))))))

(claim double-Vec
  (Pi ((E U)
       (l Nat))
    (mot-double-Vec E l)))
(define double-Vec
  (lambda (E l)
    (ind-Nat l
      (mot-double-Vec E)
      (lambda (es)
        vecnil)
      (step-double-Vec E))))

(define twice-Vec
  (lambda (E l)
    (lambda (es)
      (replace (symm (twice=double l))
        (lambda (k)
          (Vec E k))
        (double-Vec E l es)))))

;;;;;;;;; Sigma as 'there exist'
(claim grape-same
  (Sigma ((es (List Atom)))
    (= (List Atom)
       (snoc Atom es 'grape)
       (:: 'grape es))))
(define grape-same
  (cons nil
    (same (:: 'grape nil))))

;;;;;;;;; replicate
(claim mot-replicate
  (-> U Nat
      U))
(define mot-replicate
  (lambda (E k)
    (Vec E k)))

(claim step-replicate
  (Pi ((E U)
       (e E)
       (l-1 Nat))
    (-> (mot-replicate E l-1)
        (mot-replicate E (add1 l-1)))))
(define step-replicate
  (lambda (E e l-1 replicate_l-1)
    (vec:: e replicate_l-1)))

(claim replicate
  (Pi ((E U)
       (l Nat))
    (-> E
      (Vec E l))))
(define replicate
  (lambda (E l)
    (lambda (e)
      (ind-Nat l
        (mot-replicate E)
        vecnil
        (step-replicate E e)))))

;;;;;;;;; vec->list
(claim mot-vec->list
  (Pi ((E U)
       (k Nat))
    (-> (Vec E k)
      U)))
(define mot-vec->list
  (lambda (E k es)
    (List E)))

(claim step-vec->list
  (Pi ((E U)
       (l-1 Nat)
       (h E)
       (t (Vec E l-1)))
    (-> (mot-vec->list E l-1 t)
        (mot-vec->list E (add1 l-1) (vec:: h t)))))
(define step-vec->list
  (lambda (E l-1 h t vec->list_t)
    (:: h vec->list_t)))

(claim vec->list
  (Pi ((E U)
       (l Nat))
    (-> (Vec E l)
        (List E))))
(define vec->list
  (lambda (E l)
    (lambda (es)
      (ind-Vec l es
        (mot-vec->list E)
        nil
        (step-vec->list E)))))

;;;;;;;;; list->vec
(claim mot-list->vec
  (Pi ((E U))
    (-> (List E)
        U)))
(define mot-list->vec
  (lambda (E es)
    (Vec E (length E es))))

(claim step-list->vec
  (Pi ((E U)
       (e E)
       (es (List E)))
    (-> (mot-list->vec E es)
        (mot-list->vec E (:: e es)))))
(define step-list->vec
  (lambda (E e es list->vec_es)
    (vec:: e list->vec_es)))

(claim step-list->vec_foolish
  (Pi ((E U)
       (e E)
       (es (List E)))
    (-> (mot-list->vec E es)
        (mot-list->vec E (:: e es)))))
(define step-list->vec_foolish
  (lambda (E e es list->vec_es)
    (replicate E (length E (:: e es)) e)))

(claim list->vec
  (Pi ((E U)
       (es (List E)))
    (mot-list->vec E es)))
(define list->vec
  (lambda (E es)
    (ind-List es
      (mot-list->vec E)
      vecnil
      ;(step-list->vec_foolish E))))
      (step-list->vec E))))

;;;;;;;;; Vec/append
(claim mot-vec-append
  (Pi ((E U)
       (j Nat)
       (k Nat))
    (-> (Vec E k)
        U)))
(define mot-vec-append
  (lambda (E j k)
    (lambda (es)
      (Vec E (+ k j)))))

(claim step-vec-append
  (Pi ((E U)
       (j Nat)
       (l-1 Nat)
       (h E)
       (t (Vec E l-1)))
    (-> (mot-vec-append E j l-1 t)
        (mot-vec-append E j (add1 l-1) (vec:: h t)))))
(define step-vec-append
  (lambda (E j l-1 h t)
    (lambda (vec-append_l-1)
      (vec:: h vec-append_l-1))))

(claim vec-append
  (Pi ((E U)
       (l Nat)
       (j Nat))
    (-> (Vec E l) (Vec E j)
        (Vec E (+ l j)))))
(define vec-append
  (lambda (E l j)
    (lambda (es end)
      (ind-Vec l es
        (mot-vec-append E j)
        end
        (step-vec-append E j)))))

;;;;;;;;; fika
(claim fika (Vec Atom 5))
(define fika
  (vec-append Atom 3 2
    treats
    (list->vec Atom drinks)))

;;;;;;;;; list->vec->list=
; aside, treat statement
(claim Treat-Statement U)
(define Treat-Statement
  (Pi ((some-treats (List Atom))
       (more-treats (List Atom)))
    (-> (= (List Atom)
          some-treats
          more-treats)
        (= (List Atom)
          (:: 'plattar some-treats)
          (:: 'plattar more-treats)))))

(claim ::-plattar
  (-> (List Atom)
      (List Atom)))
(define ::-plattar
  (lambda (tasty-treats)
    (:: 'plattar tasty-treats)))

(claim treat-proof Treat-Statement)
(define treat-proof
  (lambda (some-treats more-treats treats=)
    (cong treats= ::-plattar)))

(claim length-treats=
  (Pi ((some-treats (List Atom))
       (more-treats (List Atom)))
    (-> (= (List Atom)
          some-treats
          more-treats)
        (= Nat
          (length Atom some-treats)
          (length Atom more-treats)))))
(define length-treats=
  (lambda (some-treats more-treats treats=)
    (cong treats= (length Atom))))
; end aside, treat statement

; helper
(claim ::-fun
  (Pi ((E U))
    (-> E (List E)
        (List E))))
(define ::-fun
  (lambda (E)
    (lambda (e es)
      (:: e es))))
; end helper

(claim mot-list->vec->list=
  (Pi ((E U))
    (-> (List E)
        U)))
(define mot-list->vec->list=
  (lambda (E es)
    (= (List E)
      es
      (vec->list E
        (length E es)
        (list->vec E es)))))

(claim step-list->vec->list=
  (Pi ((E U)
       (e E)
       (es (List E)))
    (-> (mot-list->vec->list= E es)
        (mot-list->vec->list= E (:: e es)))))
(define step-list->vec->list=
  (lambda (E e es)
    (lambda (list->vec->list=_es)
      (cong list->vec->list=_es
        (::-fun E e)))))

(claim list->vec->list=
  (Pi ((E U)
       (es (List E)))
    (= (List E)
       es
       (vec->list E
         (length E es)
         (list->vec E es)))))
(define list->vec->list=
  (lambda (E es)
    (ind-List es
      (mot-list->vec->list= E)
      (same nil)
      (step-list->vec->list= E))))

;;;;;;;;; Even
(claim Even
  (-> Nat
      U))
(define Even
  (lambda (n)
    (Sigma ((half Nat))
      (= Nat n (double half)))))

(claim zero-is-even (Even zero))
(define zero-is-even
  (cons zero (same zero)))

(claim +two=even
  (Pi ((n Nat))
    (-> (Even n)
        (Even (+ 2 n)))))
(define +two=even
  (lambda (n e_n)
    (cons (add1 (car e_n))
      (cong (cdr e_n) (+ 2)))))

(claim two-is-even (Even 2))
(define two-is-even
  (+two=even zero zero-is-even))

;;;;;;;;; Odd
(claim Odd
  (-> Nat
      U))
(define Odd
  (lambda (n)
    (Sigma ((haf Nat))
      (= Nat n (add1 (double haf))))))

(claim one-is-odd (Odd one))
(define one-is-odd
  (cons zero (same one)))

(claim thirteen-is-odd (Odd 13))
(define thirteen-is-odd
  (cons 6 (same 13)))

;;;;;;;;; add1 even or odd 
(claim add1-even->odd
  (Pi ((n Nat))
    (-> (Even n)
        (Odd (add1 n)))))
(define add1-even->odd
  (lambda (n e_n)
    (cons (car e_n)
      (cong (cdr e_n) (+ 1)))))

(claim add1-odd->even
  (Pi ((n Nat))
    (-> (Odd n)
        (Even (add1 n)))))
(define add1-odd->even
  (lambda (n o_n)
    (cons (add1 (car o_n))
      (cong (cdr o_n) (+ 1)))))

;;;;;;;;; even-or-odd
(claim mot-even-or-odd
  (-> Nat
      U))
(define mot-even-or-odd
  (lambda (k)
    (Either (Even k) (Odd k))))

(claim step-even-or-odd
  (Pi ((n-1 Nat))
    (-> (mot-even-or-odd n-1)
        (mot-even-or-odd (add1 n-1)))))
(define step-even-or-odd
  (lambda (n-1 e-or-o_n-1)
    (ind-Either e-or-o_n-1
      (lambda (e-or-o)
        (mot-even-or-odd (add1 n-1)))
      (lambda (e_n-1)
        (right
          (add1-even->odd n-1 e_n-1)))
      (lambda (o_n-1)
        (left
          (add1-odd->even n-1 o_n-1))))))

(claim even-or-odd
  (Pi ((n Nat))
    (Either (Even n) (Odd n))))
(define even-or-odd
  (lambda (n)
    (ind-Nat n
      mot-even-or-odd
      (left zero-is-even)
      step-even-or-odd)))

;;;;;;;;; Maybe
(claim Maybe
  (-> U
      U))
(define Maybe
  (lambda (X)
    (Either X Trivial)))

(claim nothing
  (Pi ((E U))
    (Maybe E)))
(define nothing
  (lambda (E)
    (right sole)))

(claim just
  (Pi ((E U))
    (-> E
        (Maybe E))))
(define just
  (lambda (E e)
    (left e)))

;;;;;;;;; maybe-head, maybe-tail
(claim maybe-head
  (Pi ((E U))
    (-> (List E)
        (Maybe E))))
(define maybe-head
  (lambda (E es)
    (rec-List es
      (nothing E)
      (lambda (hd tl tail_tl)
        (just E hd)))))

(claim maybe-tail
  (Pi ((E U))
    (-> (List E)
        (Maybe (List E)))))
(define maybe-tail
  (lambda (E es)
    (rec-List es
      (nothing (List E))
      (lambda (hd tl tail_tl)
        (just (List E) tl)))))

;;;;;;;;; list-ref
(claim step-list-ref
  (Pi ((E U))
    (-> Nat
        (-> (List E)
            (Maybe E))
        (-> (List E)
            (Maybe E)))))
(define step-list-ref
  (lambda (E n-1 list-ref_n-1)
    (lambda (es)
      (ind-Either (maybe-tail E es)
        (lambda (maybe_tl)
          (Maybe E))
        (lambda (tl)
          (list-ref_n-1 tl))
        (lambda (empty)
          (nothing E))))))

(claim list-ref
  (Pi ((E U))
    (-> Nat (List E)
        (Maybe E))))
(define list-ref
  (lambda (E n)
    (rec-Nat n
      (maybe-head E)
      (step-list-ref E))))

;;;;;;;;; similarly-absurd
(claim similarly-absurd
  (-> Absurd
      Absurd))
(define similarly-absurd
  (lambda (x)
    x))

;;;;;;;;; fin for finite, fzero, fadd
(claim Fin
  (-> Nat
      U))
(define Fin
  (lambda (n)
    (iter-Nat n
      Absurd
      Maybe)))

; (fzero n) points at the head of a (Vec X (add1 n))
(claim fzero
  (Pi ((n Nat))
    (Fin (add1 n)))) ; (Maybe (Fin n))
(define fzero
  (lambda (n)
    (nothing (Fin n))))

; fadd1 points somewhere in its tail
(claim fadd1
  (Pi ((n Nat))
    (-> (Fin n)
        (Fin (add1 n)))))
(define fadd1
  (lambda (n)
    (lambda (i-1)
      (just (Fin n) i-1))))

;;;;;;;;; vec-ref
(claim base-vec-ref
  (Pi ((E U))
    (-> (Fin zero) (Vec E zero)
        E)))
(define base-vec-ref
  (lambda (E no-value-ever es)
    (ind-Absurd no-value-ever
      E)))

(claim step-vec-ref
  (Pi ((E U)
       (l-1 Nat))
    (-> (-> (Fin l-1) (Vec E l-1)
            E)
        (-> (Fin (add1 l-1)) (Vec E (add1 l-1))
            E))))
(define step-vec-ref
  (lambda (E l-1)
    (lambda (vec-ref_l-1)
      (lambda (i es)
        (ind-Either i
          (lambda (i) E)
          (lambda (i-1)
            (vec-ref_l-1 i-1 (tail es)))
          (lambda (triv)
            (head es)))))))

(claim vec-ref
  (Pi ((E U)
       (l Nat))
    (-> (Fin l) (Vec E l)
        E)))
(define vec-ref
  (lambda (E l)
    (ind-Nat l
      (lambda (k)
        (-> (Fin k) (Vec E k)
            E))
      (base-vec-ref E)
      (step-vec-ref E))))

;;;;;;;;; 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)))))))

(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)))))

(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)))))

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

(claim sub1=
  (Pi ((n Nat)
       (j Nat))
    (-> (= Nat (add1 n) (add1 j))
        (= Nat n j))))
(define sub1=
  (lambda (n j)
    (use-Nat= (add1 n) (add1 j))))

;;;;;;;;; donut absurdity
(claim donut-absurdity
  (-> (= Nat 0 6)
      (= Atom 'powdered 'glazed)))
(define donut-absurdity
  (lambda (zero=six)
    (ind-Absurd
      (zero-not-add1 5 zero=six)
      (= Atom 'powdered 'glazed))))

;;;;;;;;; one-not-six
(claim one-not-six
  (-> (= Nat 1 6)
      Absurd))
(define one-not-six
  (lambda (one=six)
    (zero-not-add1 4
      (sub1= 0 5 one=six))))

;;;;;;;;; front
(claim mot-front
  (Pi ((E U)
       (k Nat))
    (-> (Vec E k)
        U)))
(define mot-front
  (lambda (E k es)
    (Pi ((j Nat))
      (-> (= Nat k (add1 j))
          E))))

(claim step-front
  (Pi ((E U)
       (l Nat)
       (e E)
       (es (Vec E l)))
    (-> (mot-front E l es)
        (mot-front E (add1 l) (vec:: e es)))))
(define step-front
  (lambda (E l e es)
    (lambda (front_es)
      (lambda (j eq)
        e))))

(claim front
  (Pi ((E U)
       (n Nat))
    (-> (Vec E (add1 n))
        E)))
(define front
  (lambda (E l es)
    ((ind-Vec (add1 l) es
       (mot-front E)
       (lambda (j eq)
         (ind-Absurd
           (zero-not-add1 j eq)
           E))
       (step-front E))
      l (same (add1 l)))))

;;;;;;;;; pem & Dec
(claim pem
  (Pi ((X U))
    (Either X (-> X Absurd))))

(claim pem-not-false
  (Pi ((X U))
    (-> (-> (Either X (-> X Absurd))
            Absurd)
        Absurd)))
(define pem-not-false
  (lambda (X)
    (lambda (pem-false)
      (pem-false
        (right
          (lambda (x)
            (pem-false
              (left x))))))))

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

;;;;;;;;; zero?
(claim zero?
  (Pi ((j Nat))
    (Dec (= Nat zero j))))
(define zero?
  (lambda (j)
    (ind-Nat j
      (lambda (k)
        (Dec (= Nat zero k)))
      (left
        (same zero))
      (lambda (j-1 zero?n_1)
        (right
          (zero-not-add1 j-1))))))

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

;;;;;;;;; dec-add1=
(claim dec-add1=
  (Pi ((n-1 Nat)
       (j-1 Nat))
    (-> (Dec (= Nat n-1 j-1))
        (Dec (= Nat (add1 n-1) (add1 j-1))))))
(define dec-add1=
  (lambda (n-1 j-1 eq-or-not)
    (ind-Either eq-or-not
      (lambda (target)
        (Dec (= Nat (add1 n-1) (add1 j-1))))
      (lambda (yes)
        (left
          (cong yes (+ 1))))
      (lambda (no)
        (right
          (lambda (n=j)
            (no
              (sub1= n-1 j-1 n=j))))))))

;;;;;;;;; nat=?
(claim mot-nat=?
  (-> Nat
      U))
(define mot-nat=?
  (lambda (k)
    (Pi ((j Nat))
      (Dec (= Nat k 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 j)
    (ind-Nat j
      (lambda (k)
        (Dec (= Nat (add1 n-1) k)))
      (right
        (add1-not-zero n-1))
      (lambda (j-1 nat=?_j-1)
        (dec-add1= n-1 j-1
          (nat=?_n-1 j-1))))))
        

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