The little typer code

the-little-typer.rkt

#lang pie

;3-24
(claim + (-> Nat Nat Nat))
(define +
	(λ(a b)
		(iter-Nat a
			b
			(λ(almost)
				(add1 almost)
			)
		)
	)
)

;2-50
(claim gauss (-> Nat Nat))
(define gauss
	(λ(n)
		(rec-Nat n
			0
			(λ(n-1 almost)
				(+ n-1 almost)
			)
		)
	)
)

;????
(claim zerop (-> Nat Atom))
(define zerop
	(λ(n)
		(ind-Nat n
			(λ(k) Atom)
			't
			(λ(n-1 almost) 'nil)
		)
	)
)

;5-35
(claim length (Π ((E U)) (-> (List E) Nat)))
(define length
	(λ(E xs)
		(rec-List xs
			0
			(λ(e es almost)
			(add1 almost)
			)
		)
	)
)

;5-45
(claim append (Π ((E U)) (-> (List E) (List E) (List E))))
(define append
	(λ(E xs ys)
		(rec-List xs
			ys
			(λ(e es result)
			(:: e result)
			)
		)
	)
)

;5-60
(claim snoc (Π ((E U)) (-> (List E) E (List E))))
(define snoc
	(λ(E xs e)
		(rec-List xs
			(:: e nil)
			(λ(e es result)
				(:: e result)
			)
		)
	)
)

;5-62
(claim reverse (Π ((E U)) (-> (List E) (List E))))
(define reverse
	(λ(E xs)
		(rec-List xs
			(the (List E) nil)
			(λ(x xs almost)
				(snoc E almost x)
			)
		)
	)
)

;7-38
(claim first (Π ((E U) (l Nat)) (-> (Vec E (+ 1 l)) E)))
(define first
	(λ(E l xs)
		(head xs)
	)
)

;(first Nat 0 (the (Vec Nat 1) (vec:: 1 vecnil)))

;7-43
(claim rest (Π ((E U) (l Nat)) (-> (Vec E (+ 1 l)) (Vec E l))))
(define rest
	(λ(E l xs) (tail xs))
)

;8-28
(claim last (Π ((E U) (l Nat)) (-> (Vec E (+ 1 l)) E)))
(define last
	(λ(E l)
		(ind-Nat l
			(λ(k) (-> (Vec E (+ 1 k)) E))
			(λ(xs) (head xs))
			(λ(k-1 last_k-1 ys)
				(last_k-1 (tail ys))
			)
		)
	)
)
;(last Nat 1 (the (Vec Nat 2) (vec:: 2 (vec:: 1 vecnil))))

;8-60
(claim drop-last (Π ((E U) (l Nat)) (-> (Vec E (+ 1 l)) (Vec E l))))
(define drop-last
	(λ(E l)
		(ind-Nat l
			(λ(k) (-> (Vec E (+ 1 k)) (Vec E k)))
			(λ(whatever) vecnil)
			(λ(k-1 last_k-1 ys)
				(vec:: (head ys) (last_k-1 (tail ys)))
			)
		)
	)
)
;(drop-last Nat 1 (the (Vec Nat 2) (vec:: 2 (vec:: 1 vecnil))))

;9-41
(claim +1=add1 (Π ((n Nat)) (= Nat (+ 1 n) (add1 n))))
(define +1=add1
	(λ(n)
		(same (add1 n))
	)
)

;10-21
(claim double (-> Nat Nat))
(claim twice (-> Nat Nat))
(define double
	(λ(n)
		(iter-Nat n
			0
			(+ 2)
		)
	)
)
(define twice (λ(n) (+ n n)))

(claim succ (-> Nat Nat))
(define succ (λ(x) (add1 x)))

(claim a+succ_b=succ_a+b (Π ((a Nat)(b Nat)) (= Nat (+ a (succ b)) (succ (+ a b)))))
(define a+succ_b=succ_a+b
	(λ(a b)
		(ind-Nat a
			(λ(k) (= Nat (+ k (succ b)) (succ (+ k b))))
			(same (succ b))
			(λ(k-1 proof_k-1)
				(cong proof_k-1 succ)
			)
		)
	)
)

;9
(claim double=twice (Π ((n Nat)) (= Nat (double n) (twice n))))
(define double=twice
	(λ(n)
		(symm
			(ind-Nat n
				(λ(k) (= Nat (twice k) (double k)))
				(same 0)
				(λ(k-1 proof_k-1)
					(replace proof_k-1
						(λ(x) (= Nat (succ (+ k-1 (+ 1 k-1))) (+ 2 x)))
						(cong (a+succ_b=succ_a+b k-1 k-1) succ)
					)
				)
			)
		)
	)
)
;(double=twice 10)

;9-56
(claim twice-Vec (Π ((E U)(l Nat)) (-> (Vec E l) (Vec E (twice l)))))
(define twice-Vec
	(λ(E l)
		(ind-Nat l
			(λ(l) (-> (Vec E l) (Vec E (twice l))))
			(λ(xs) vecnil)
			(λ(k-1 almost xs)
				(replace (double=twice (succ k-1))
					(λ(x) (Vec E x))
					(vec:: (head xs)
						(vec:: (head xs)
							(replace (symm (double=twice k-1))
								(λ(x) (Vec E x))
								(almost (tail xs))
							)
						)
					)
				)
			)
		)
	)
)
;(twice-Vec Nat 2 (vec:: 2 (vec:: 1 vecnil)))

;10-54
(claim list->vec (Π ((E U) (xs (List E))) (Vec E (length E xs))))
(define list->vec
	(λ(E xs)
		(ind-List xs
			(λ(ys) (Vec E (length E ys)))
			vecnil
			(λ(x rem vec_rem)
				(vec:: x vec_rem)
			)
		)
	)
)
;(list->vec Nat (:: 1 (:: 2 nil)))

;10-45
(claim replicate (Π ((E U)(l Nat)) (-> E (Vec E l))))
(define replicate
	(λ(E l e)
		(ind-Nat l
			(λ(k) (Vec E k))
			vecnil
			(λ(k-1 xs)
				(vec:: e xs)
			)
		)
	)
)
;(replicate Atom 10 'peas)


;11-5
(claim vec-append (Π ((E U) (m Nat) (n Nat)) (-> (Vec E m) (Vec E n) (Vec E (+ m n)))))
(define vec-append
	(λ(E m n)
		(ind-Nat m
			(λ(k) (-> (Vec E k) (Vec E n) (Vec E (+ k n))))
			(λ(xs ys) ys)
			(λ(k-1 append_m-1 xs ys)
				(vec:: (head xs) (append_m-1 (tail xs) ys))
			)
		)
	)
)
;(vec-append Nat 1 1 (vec:: 1 vecnil) (vec:: 2 vecnil))

;11-32
(claim vec->list (Π ((E U) (l Nat)) (-> (Vec E l) (List E))))
(define vec->list
	(λ(E l)
		(ind-Nat l
			(λ(k) (-> (Vec E k) (List E)))
			(λ(xs) nil)
			(λ(k almost xs)
				(:: (head xs) (almost (tail xs)))
			)
		)
	)
)

;11-34
(claim list->vec->list= (Π ((E U) (xs (List E))) (= (List E) xs (vec->list E (length E xs) (list->vec E xs)))))
(define list->vec->list=
	(λ(E xs)
		(ind-List xs
			(λ(ys) (= (List E) ys (vec->list E (length E ys) (list->vec E ys))))
			(same nil)
			(λ(y ys proof_ys)
				(cong proof_ys (the (-> (List E) (List E)) (λ(t) (:: y t))))
			)
		)
	)
)

;12-5
(claim Even (-> Nat U))
(define Even
	(λ(n) (Σ ((half Nat)) (= Nat (double half) n)))
)

;12-13
(claim +2-even (Π ((n Nat)) (-> (Even n) (Even (+ 2 n)))))
(define +2-even
	(λ(n n-is-even)
		(cons
			(succ (car n-is-even))
			(cong (cdr n-is-even) (+ 2))
		)
	)
)
;(+2-even 4 (cons 2 (same 4)))




;12-32
(claim Odd (-> Nat U))
(define Odd
	(λ(n) (Σ ((haf Nat)) (= Nat (succ (double haf)) n)))
)

;12-49
(claim succ_odd_is_even (Π ((a Nat)) (-> (Odd a) (Even (succ a)))))
(define succ_odd_is_even
	(λ(a a_is_odd)
		(cons
			(succ (car a_is_odd))
			(cong (cdr a_is_odd) (+ 1))
		)
	)
)

;12-53
(claim succ_even_is_odd (Π ((a Nat)) (-> (Even a) (Odd (succ a)))))
(define succ_even_is_odd
	(λ(a a_is_even)
		(cons
			(car a_is_even)
			(cong (cdr a_is_even) (+ 1))
		)
	)
)

;13-15
(claim either-even-or-odd (Π ((a Nat)) (Either (Even a)	(Odd a))))
(define either-even-or-odd
	(λ(a)
		(ind-Nat a
			(λ(k) (Either (Even k) (Odd k)))
			(left (cons 0 (same 0)))
			(λ(k-1 proof_k-1)
				(ind-Either proof_k-1
					(λ(whatever) (Either (Even (succ k-1)) (Odd (succ k-1))))
					(λ(k-1-is-even) (right (succ_even_is_odd k-1 k-1-is-even)))
					(λ(k-1-is-odd) (left (succ_odd_is_even k-1 k-1-is-odd)))
				)
			)
		)
	)
)
;(either-even-or-odd 4)
;(either-even-or-odd 5)

;14-7
(claim Maybe (-> U U))
(define Maybe
	(λ(inner)
		(Either inner Trivial)
	)
)

;14-9
(claim nothing (Π ((E U)) (Maybe E)))
(define nothing
	(λ(E)
		(right sole)
	)
)

;14-10
(claim just (Π((E U)) (-> E (Maybe E))))
(define just
	(λ(E e)
		(left e)
	)
)

;14-11
(claim maybe-head (Π((E U)) (-> (List E) (Maybe E))))
(define maybe-head
	(λ(E xs)
		(rec-List xs
			(nothing E)
			(λ(x xs almost) (just E x))
		)
	)
)
;(maybe-head Nat nil)
;(maybe-head Nat (:: 1 nil))

;14-12
(claim maybe-tail (Π((E U)) (-> (List E) (Maybe (List E)))))
(define maybe-tail
	(λ(E xs)
		(rec-List xs
			(nothing (List E))
			(λ(x xs almost) (just (List E) xs))
		)
	)
)
;(maybe-head Nat nil)
;(maybe-head Nat (:: 1 nil))

;14-23
(claim list-ref (Π ((E U)) (-> Nat (List E) (Maybe E))))
(define list-ref
	(λ(E k)
		(rec-Nat k
			(maybe-head E)
			(λ(k-1 almost xs)
				(ind-Either (maybe-tail E xs)
					(λ(whatever) (Maybe E))
					(λ(some)	(almost some))
					(λ(empty) (nothing E))
				)
			)
		)
	)
)
;(list-ref Nat 2 (:: 1 (:: 2 (:: 3 nil))))
;(list-ref Nat 4 (:: 1 (:: 2 (:: 3 nil))))

;14-50
(claim Fin (Π ((n Nat)) U))
(define Fin
	(λ(n)
		(iter-Nat n
			Absurd
			Maybe	;; ==> (λ(almost) (Maybe almost))
		)
	)
)

;14-53
(claim fzero (Π ((n Nat)) (Fin (add1 n))))
(define fzero
	(λ(n) (nothing (Fin n)))
)
;(fzero 5)

;14-58
(claim fadd1 (Π ((n Nat)) (-> (Fin n) (Fin (add1 n)))))
(define fadd1
	(λ(n k)
		(just (Fin n) k)
	)
)
;(fadd1 5 (fzero 4))

;14-61
(claim vec-ref (Π ((E U) (l Nat)) (-> (Fin l) (Vec E l) E)))
(define vec-ref
	(λ(E l)
		(ind-Nat l
			(λ(k) (-> (Fin k) (Vec E k) E))
			(λ(zero-fin empty-vec) 
				(ind-Absurd zero-fin E)
			)
			(λ(l-1 vec-ref_l-1 k xs)
				(ind-Either k
					(λ(whatever) E)
					(λ(k-1) (vec-ref_l-1 k-1 (tail xs)))
					(λ(zero-idx) (head xs))
				)
			)
		)
	)
)
;(vec-ref Nat 2 (fadd1 1 (fzero 0)) (vec:: 1 (vec:: 2 vecnil)))

;15-21
(claim =conseq (Π ((m Nat) (n Nat)) U))
(define =conseq 
	(λ(m n)
		(which-Nat m
			(which-Nat n
				Trivial
				(λ(n-1) Absurd)
			)
			(λ(m-1)
				(which-Nat n
					Absurd
					(λ(n-1) (= Nat m-1 n-1))
				)
			)
		)
	)
)
;(=conseq 2 3)
;(=conseq 1 0)
;(=conseq 0 1)
;(=conseq 0 0)

;15-23
(claim =conseq-same (Π ((n Nat)) (=conseq n n)))
(define =conseq-same
	(λ(n)
		(ind-Nat n
			(λ(k) (=conseq k k))
			sole
			(λ(k-1 proof_k-1)
				(same k-1)
			)
		)
	)
)

;15-35 ****
(claim use-Nat= (Π ((m Nat) (n Nat)) (-> (= Nat m n) (=conseq m n))))
(define use-Nat=
	(λ(m n proof_m=n)
		(replace proof_m=n
			(λ(x) (=conseq m x))
			(=conseq-same m)
		)
	)
)

;15-44
(claim add1-not-zero (Π ((n Nat)) (-> (= Nat (add1 n) 0) Absurd)))
(define add1-not-zero
	(λ(n proof_succ-n=0)
		((use-Nat= (add1 n) 0) proof_succ-n=0)
	)
)

;15-50 because the conseq= of (m+1) and (n+1) is m=n so use-Nat preduces the proof of the following
(claim pred= (Π ((m Nat) (n Nat)) (-> (= Nat (succ m) (succ n)) (= Nat m n))))
(define pred=
	(λ(m n proof_succ-m=succ-n)
		(use-Nat= (add1 m) (add1 n) proof_succ-m=succ-n)
	)
)

;15-51
(claim one-not-six (-> (= Nat 1 6) Absurd))
(define one-not-six
	(λ(one-equals-six)
		(use-Nat= 0 5 (use-Nat= 1 6 one-equals-six))
	)
)

;15-53
(claim front (Π ((E U) (l-1 Nat)) (-> (Vec E (succ l-1)) E)))
(define front
	(λ(E l-1 xs)
		(
			(ind-Vec (succ l-1) xs
				(λ(k whatever) (-> (= Nat (succ l-1) k) E))
				; Although it's accepted using (head xs) ....
				; here we actually needs to prove the following line is not reachable
				(λ(eq)
				(ind-Absurd ((add1-not-zero l-1) eq) E))
				(λ(k-1 y ys almost eq) y)
			)
			(same (add1 l-1))
		)
	)
)

;15-90 This proof is actually like this:
; Assume PEM is wrong, there must be a theorem that is both correct and wrong
; And then we can proof Absurd
(claim pem-not-false (Π ((X U)) (-> (-> (Either X (-> X Absurd)) Absurd) Absurd)))
(define pem-not-false
	(λ(X pem-false)
		(pem-false (right (λ(X-proof) (pem-false (left X-proof))) ))
	)
)

;15-107
(claim Dec (Π((X U)) U))
(define Dec (λ(X) (Either X (-> X Absurd))))


;16-4
(claim zero? (Π ((n Nat)) (Dec (= Nat n 0))))
(define zero?
	(λ(n)
		(ind-Nat n
			(λ(k) (Dec (= Nat k 0)))
			(left (same 0))
			(λ(k-1 proof_k-1)
				(right (add1-not-zero k-1))
			)
		)
	)
)

;16-17
(claim n-not-succ-n (Π ((n Nat)) (-> (= Nat (+ 1 n) n) Absurd)))
(define n-not-succ-n
	(λ(n)
		(ind-Nat n
			(λ(k) (-> (= Nat (+ 1 k) k) Absurd))
			(use-Nat= 1 0)
			(λ(k-1 proof_k-1 k=k-1)
				(proof_k-1 (pred= (succ k-1) k-1 k=k-1))
			)
		)
	)
)

(claim pred (-> Nat Nat))
(define pred
	(λ(n)
		(which-Nat n
			0
			(λ(n-1) n-1)
		)
	)
)


(claim nat=?-rev (Π ((m Nat) (n Nat)) (Dec (= Nat n m))))
(define nat=?-rev
	; note: don't intro n this time, because	once we done that
	; the induction will limited to the given (k n) 
	; which makes us unable to do further induction
	(λ(m)
		(ind-Nat m
			(λ(k) (Π ((n Nat)) (Dec (= Nat n k))))
			; base: for every n, n=0 is decidable
			(λ(n)
				(ind-Nat n
					(λ(j) (Dec (= Nat j 0)))
					(left (same 0))
					(λ(j-1 proof_j-1=0?) (right (use-Nat= (succ j-1) 0)))
				)
			)
			; step: for every n, if n=k-1 is decidable, n=k is decidable
			(λ(k-1 proof_k-1 n)
				(ind-Nat n
					(λ(j) (Dec (= Nat j (succ k-1))))
					; base: 0=k is decidable, because k-1 exists, so this must be false
					(right (λ(k=0) ((add1-not-zero k-1) (symm k=0))))
					; step: if j-1=k is decidable then j=k is decidable
					(λ(j-1 proof_k=j-1?)
						; here's the trick, it's impossible for us to proof j=k? from k=j-1?
						; however, it's possible to prove it with j-1=k-1?
						; So we actually apply the outer induction assumption at this time
						; rather than use the inner assumption.
						(ind-Either (proof_k-1 j-1)
							(λ(whatever) (Dec (= Nat (succ j-1) (succ k-1))))
							(λ(j-1=k-1) (left (cong j-1=k-1 succ)))
							(λ(j-1!=k-1)(right (λ(j-1=k-1) (j-1!=k-1 (cong j-1=k-1 pred)))))
						)
					)
				)
			)
		)
	)
)

(claim nat=? (Π ((m Nat) (n Nat)) (Dec (= Nat m n))))
(define nat=? (λ(m n) (nat=?-rev n m)))

;(nat=? 1 1)
;(nat=? 1 2)

(claim neg (Pi ((X U)) U))
(define neg (λ(X) (-> X Absurd)))


(claim <=> (Pi ((X U) (Y U)) U))
(define <=> (λ(X Y) (Pair (-> X Y) (-> Y X))))

(claim equ-symm (Pi ((X U) (Y U)) (-> (<=> X Y) (<=> Y X))))
(define equ-symm
	(λ(X Y X-equ-Y)
		(cons (cdr X-equ-Y) (car X-equ-Y))
	)
)

(claim equ-proof (Pi ((X U) (Y U)) (-> (<=> X Y) X Y)))
(define equ-proof
	(λ(X Y X-equ-Y X-proof)
		((car X-equ-Y) X-proof)
	)
)

(claim contraposition-equ (Pi ((X U) (Y U)) (-> (Dec X) (Dec Y)(<=> (-> X Y) (-> (neg Y) (neg X))))))
(define contraposition-equ
	(λ(X Y dec-X dec-Y)
		(cons
			(λ(X-implies-Y Y-false X-proof) (Y-false (X-implies-Y X-proof)))
			(λ(Y-false-implies-X-false X-proof)
				(ind-Either dec-Y
					(λ(whatever) Y)
					(λ(Y-proof) Y-proof)
					(λ(Y-false) (ind-Absurd ((Y-false-implies-X-false Y-false) X-proof) Y))
				)
			)
		)
	)
)

(claim dual-neg-equ (Pi ((X U)) (-> (Dec X) (<=> X (neg (neg X))))))
(define dual-neg-equ
	(λ(X dec-X)
		(cons
			(λ(X-proof X-false) (X-false X-proof))
			(λ(X-false-false)
				(ind-Either dec-X
					(λ(whatever) X)
					(λ(X-proof) X-proof)
					(λ(X-false) (ind-Absurd (X-false-false X-false) X))
				)
			)
		)
	)
)


;Proof of Proof-by-absurdity
(claim proof-by-absurdity (Pi ((X U)) (-> (Dec X) (neg (neg X)) X)))
(define proof-by-absurdity
	(λ(X dec-X X-false-false)
		(ind-Either dec-X
			(λ(whatever) X)
			(λ(X-proof) X-proof)
			(λ(X-false) (ind-Absurd (X-false-false X-false) X))
		)
	)
)