The Little Typer

little-typer.pie

;; -*- scheme-*-
#lang pie

;;
;; Boolean
;;
(claim Boolean U)
(define Boolean Atom)

;;
;; Arithmetic
;;
(claim step-+ (-> Nat Nat))
(define step-+
  (λ (n) (add1 n)))

(claim + (-> Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      step-+)))

(claim make-step-* (-> Nat Nat Nat))
(define make-step-*
  (λ (x y) (+ x y)))

(claim * (-> Nat Nat Nat))
(define *
  (λ (x y)
    (iter-Nat x
      0
      (make-step-* y))))

(claim zerop (-> Nat Boolean))
(define zerop
  (λ (n)
    (which-Nat n
      't
      (λ (n-1) 'nil))))

;;
;; Pair accessor
;;
(claim elim-Pair
  (Π ((A U)
       (D U)
       (R U))
    (-> (Pair A D)
        (-> A D R)
        R)))
(define elim-Pair
  (λ (A D R)
    (λ (p f)
      (f (car p) (cdr p)))))

(claim kar
  (Π ((A U)
       (D U))
    (-> (Pair A D) A)))
(define kar
  (λ (A D)
    (λ (p)
      (elim-Pair A D A p (λ (x y) x)))))

;;
;; PI Type
;;
(claim flip
  (Π ((A U)
       (D U))
    (-> (Pair A D)
        (Pair D A))))
(define flip
  (λ (A D)
    (λ (p)
      (cons (cdr p) (car p)))))

(claim id
  (Π ((A U))
     (-> A A)))
(define id
  (λ (_u x)
    x))

;;
;; Lists
;;
(claim l (List Nat))
(define l (:: 1 (:: 2 (:: 3 nil))))

(claim length
  (Π ((A U))
    (-> (List A) Nat)))
(define length
  (λ (A)
    (λ (l)
      (rec-List l
        0
        (λ (x ll n)
          (add1 n))))))

(claim append-step
  (Π ((A U))
    (-> A (List A) (List A) (List A))))
(define append-step
  (λ (A)
    (λ (x _xs acc)
      (:: x acc))))

(claim append
  (Π ((A U))
    (-> (List A) (List A) (List A))))
(define append
  (λ (A)
    (λ (lst1 lst2)
      (rec-List lst1
        lst2
        (append-step A)))))

(claim snoc
  (Π ((A U))
    (-> (List A) A (List A))))
(define snoc
  (λ (A)
    (λ (xs x)
      (rec-List xs
        (:: x nil)
        (append-step A)))))

;; I struggled to get the ordering of the list right,
;; but it turned out to be a mistake in the book
;; http://thelittletyper.com/errata.html
(claim concat-step
  (Π ((A U))
    (-> A (List A) (List A) (List A))))
(define concat-step
  (λ (A)
    (λ (x xs acc)
      (snoc A acc x))))

(claim concat
  (Π ((A U))
    (-> (List A) (List A) (List A))))
(define concat
  (λ (A)
    (λ (l1 l2)
      (rec-List l2
        l1
        (concat-step A)))))

(claim reverse-step
  (Π ((A U))
    (-> A (List A) (List A) (List A))))
(define reverse-step
  (λ (A)
    (λ (x xs acc)
      (snoc A acc x))))

(claim reverse
  (Π ((A U))
    (-> (List A) (List A))))
(define reverse
  (λ (A)
    (λ (list)
      (rec-List list
        (the (List A) nil)
        (reverse-step A)))))


;;
;; Danish recipes
;;
(claim rugbrød
  (List Atom))
(define rugbrød
  (:: '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 kartoffelmad
  (List Atom))
(define kartoffelmad
  (append Atom
    (append Atom toppings condiments)
    (reverse Atom (:: 'plate
                    (:: 'rye-bread nil)))))

;;
;; Vectors
;;

(claim v (Vec Nat 3))
(define v
  (vec:: 1
    (vec:: 2
      (vec:: 3 vecnil))))

(claim first
  (Π ((A U)
       (l Nat))
    (-> (Vec A (add1 l)) A)))
(define first
  (λ (A l)
    (λ (v)
      (head v))))

(claim rest
  (Π ((A U)
       (l Nat))
    (-> (Vec A (add1 l)) (Vec A l))))
(define rest
  (λ (A l)
    (λ (v) (tail v))))


;;
;; Induction
;;

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

(claim peas-step
  (Π ((k-1 Nat))
    (-> (peas-mot k-1)
        (peas-mot (add1 k-1)))))
(define peas-step
  (λ (k-1 acc)
    (vec:: 'pea acc)))

(claim peas
  (Π ((k Nat))
    (Vec Atom k)))
(define peas
  (λ (k)
    (ind-Nat k
      peas-mot
      vecnil
      peas-step)))


;; last

(claim last-mot
  (-> U Nat U))
(define last-mot
  (λ (A k)
    (-> (Vec A (add1 k))
        A)))

(claim last-base
  (Π ((A U))
    (last-mot A 0)))
(define last-base
  (λ (A)
    (first A 0)))

(claim last-step
  (Π ((A U)
       (k Nat))
    (-> (last-mot A k) (last-mot A (add1 k)))))
(define last-step
  (λ (A k-1 almost)
    (λ (v)
      (almost (rest A (add1 k-1) v)))))

(claim last
  (Π ((A U)
       (k Nat))
    (-> (Vec A (add1 k)) A)))
(define last
  (λ (A k)
    (ind-Nat k
      (last-mot A)
      (last-base A)
      (last-step A))))


;; drop-last

(claim drop-last-mot
  (Π ((A U))
    (-> Nat U)))
(define drop-last-mot
  (λ (A k)
    (-> (Vec A (add1 k)) (Vec A k))))

(claim drop-last-base
  (Π ((A U))
    (drop-last-mot A zero)))
(define drop-last-base
  (λ (_A)
    (λ (v) vecnil)))

(claim drop-last-step
  (Π ((A U)
       (k Nat))
    (-> (drop-last-mot A k)
        (drop-last-mot A (add1 k)))))
(define drop-last-step
  (λ (A k acc)
    (λ (v)
      (vec:: (first A (add1 k) v)
             (acc (rest A (add1 k) v))))))

(claim drop-last
  (Π ((A U)
       (k Nat))
    (-> (Vec A (add1 k)) (Vec A k))))
(define drop-last
  (λ (A k)
    (ind-Nat k
      (drop-last-mot A)
      (drop-last-base A)
      (drop-last-step A))))


;;
;; Equality & proofs
;;
(claim add1=1+
  (Π ((n Nat))
    (= Nat (add1 n) (+ 1 n))))
(define add1=1+
  (λ (n)
    (same (add1 n))))

(claim incr
  (-> Nat Nat))
(define incr
  (λ (n)
    (iter-Nat n
      1
      (+ 1))))

;; add1 = inc

(claim add1=incr-mot
  (-> Nat U))
(define add1=incr-mot
  (λ (n)
    (= Nat (incr n) (add1 n))))

(claim add1=incr-base
  (= Nat (incr 0) (add1 0)))
(define add1=incr-base
  (same 1))

(claim add1=incr-step
  (Π ((k-1 Nat))
    (-> (= Nat (incr k-1) (add1 k-1))
        (= Nat (add1 (incr k-1)) (add1 (add1 k-1))))))
(define add1=incr-step
  (λ (k-1)
    (λ (eq)
      (cong eq (+ 1)))))

(claim add1=incr
  (Π ((n Nat))
    (= Nat (incr n) (add1 n))))
(define add1=incr
  (λ (n)
    (ind-Nat n
      add1=incr-mot
      add1=incr-base
      add1=incr-step)))


;;
;; double === twice
;;

(claim double (-> Nat Nat))
(define double
  (λ (n)
    (iter-Nat n
      0
      (+ 2))))

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


(claim add1+=+add1
  (Π ((n Nat)
       (m Nat))
    (= Nat
       (add1 (+ n m))
       (+ n (add1 m)))))
(define add1+=+add1
  (λ (n m)
    (ind-Nat n
      (λ (i)
        (= Nat
          (add1 (+ i m))
          (+ i (add1 m))))
      (same (add1 m))
      (λ (k eq) (cong eq (+ 1))))))


(claim twice=double-mot
  (-> Nat U))
(define twice=double-mot
  (λ (n)
    (= Nat (twice n) (double n))))

(claim twice=double-base
  (= Nat (twice 0) (double 0)))
(define twice=double-base
  (same 0))

(claim twice=double-step
  (Π ((n Nat))
    (-> (= Nat (twice n) (double n))
        (= Nat (twice (add1 n)) (double (add1 n))))))
(define twice=double-step
  (λ (n-1)
    (λ (eq)
      (replace (add1+=+add1 n-1 n-1)
        (λ (k)
          (= Nat
            (add1 k)
            (add1
              (add1 (double n-1)))))
        (cong eq (+ 2))))))


(claim twice=double
  (Π ((n Nat))
    (= Nat (twice n) (double n))))

(define twice=double
  (λ (n)
    (ind-Nat n
      twice=double-mot
      twice=double-base
      twice=double-step)))


;; twice-Vec

(claim double-Vec-base
  (Π ((E U))
    (-> (Vec E 0) (Vec E 0))))
(define double-Vec-base
  (λ (E v)
    vecnil))

(claim double-Vec
  (Π ((E U)
       (n Nat))
    (-> (Vec E n) (Vec E (double n)))))
(define double-Vec
  (λ (E n)
    (ind-Nat n
      (λ (k) (-> (Vec E k) (Vec E (double k))))
      (double-Vec-base E)
      (λ (k acc)
        (λ (v)
          ;; This would not work with twice because v, as
          ;; described by the type would have size `twice n`,
          ;; which has normal form
          ;; (iter-Nat k ....)
          ;; and Pie can't determine/prove that it
          ;; is not empty  (it should start with add1).
          (vec:: (head v)
            (vec:: (head v)
              (acc (tail v)))))))))

(claim twice-Vec
  (Π ((E U)
       (n Nat))
    (-> (Vec E n) (Vec E (twice n)))))
(define twice-Vec
  (λ (E n)
    (λ (es)
      (replace (symm (twice=double n))
        (λ (k)
          (Vec E k))
        (double-Vec E n es)))))


;;
;; replicate
;;

(claim replicate
  (Π ((E U)
      (l Nat))
    (-> E (Vec E l))))
(define replicate
  (λ (E l)
    (λ (e)
      (ind-Nat l
        (λ (k) (Vec E k))
        vecnil
        (λ (k v)
          (vec:: e v))))))

;; list->vec
;;
;; This version has a type which accepts
;; buggy definitions of list->vec.

(claim list->vec-mot
  (Π ((E U))
    (-> (List E) U)))
(define list->vec-mot
  (λ (E es)
    (Vec E (length E es))))

(claim list->vec-step
  (Π ((E U)
      (e E)
      (es (List E)))
    (-> (Vec E (length E es))
        (Vec E (add1 (length E es))))))
(define list->vec-step
  (λ (E e es)
    (λ (v)
      (vec:: e v))))

(claim list->vec
  (Π ((E U)
      (es (List E)))
    (Vec E (length E es))))
(define list->vec
  (λ (E es)
    (ind-List es
      (list->vec-mot E)
      vecnil
      (list->vec-step E))))


;; vec-append

(claim vec-append-mot
  (Π ((E U)
      (j Nat)
      (k Nat))
    (-> (Vec E k) U)))
(define vec-append-mot
  (λ (E j k)
    (λ (v)
      (Vec E (+ k j)))))

(claim vec-append-step
  (Π ((E U)
      (j Nat)
      (k Nat)
      (e E)
      (es (Vec E k)))
    (-> (vec-append-mot E j
          k es)
      (vec-append-mot E j
        (add1 k) (vec:: e es)))))
(define vec-append-step
  (λ (E j k e es)
    (λ (almost-answer)
      (vec:: e almost-answer))))

(claim vec-append
  (Π ((E U)
      (l Nat)
      (j Nat))
    (-> (Vec E l) (Vec E j)
      (Vec E (+ l j)))))
(define vec-append
  (λ (E l j)
    (λ (v1 v2)
      (ind-Vec l v1
        (vec-append-mot E j)
        v2
        (vec-append-step E j)))))

;; define vec->list now, and we'll use it to prove
;; that converting a list to a vector and then back
;; into a list will give the same list. Ruling out
;; some foolish list->vec definitions.

(claim vec->list-mot
  (Π ((E U)
      (k Nat))
    (-> (Vec E k) U)))
(define vec->list-mot
  (λ (E k)
    (λ (v) (List E))))

(claim vec->list-step
  (Π ((E U)
      (l-1 Nat)
      (e E)
      (es (Vec E l-1)))
    (-> (vec->list-mot E l-1 es)
        (vec->list-mot E (add1 l-1) (vec:: e es)))))
(define vec->list-step
  (λ (E l-1 e es)
    (λ (vec->list-es)
      (:: e vec->list-es))))


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


;; ensure list->vec  vec->list  gives the original list back

(claim list->vec->list=-mot
  (Π ((E U))
    (-> (List E) U)))

(define list->vec->list=-mot
  (λ (E es)
    (= (List E)
      es
      (vec->list E
        (length E es)
        (list->vec E es)))))


(claim list->vec->list=-step
  (Π ((E U)
      (e E)
      (es (List E)))
    (-> (list->vec->list=-mot E es)
        (list->vec->list=-mot E (:: e es)))))

;(define list->vec->list=-step
;  (λ (E e es)
;    (λ (eq)
;      TODO)))
;
;(claim list->vec->list=
;  (Π ((E U)
;      (es (List E)))
;    (= (List E)
;       es
;       (vec->list E
;         (length E es)
;         (list->vec E es)))))
;(define list->vec->list=
;  (λ (E es)
;    (ind-List es
;      (list->vec->list=-mot E)
;      (same nil)
;      (list->vec->list=-step E))))


;;
;; 12. Even numbers can be odd
;;

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

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

(claim +two-even
  (Π ((n Nat))
    (-> (Even n) (Even (+ 2 n)))))
(define +two-even
  (λ (n eq)
    (cons (add1 (car eq))
      (cong (cdr eq) (+ 2)))))

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


(claim Odd
  (-> Nat U))
(define Odd
  (λ (n)
    (Σ ((haf Nat))
      (= Nat n (add1 (double haf))))))

(claim one-is-odd
  (Odd 1))
(define one-is-odd
  (cons 0 (same 1)))

(claim add1-even->odd
  (Π ((n Nat))
    (-> (Even n) (Odd (add1 n)))))
(define add1-even->odd
  (λ (n even)
    (cons (car even)
      (cong (cdr even) (+ 1)))))

(claim add1-odd->even
  (Π ((n Nat))
    (-> (Odd n) (Even (add1 n)))))
(define add1-odd->even
  (λ (n odd)
    (cons (add1 (car odd))
      (cong (cdr odd) (+ 1)))))


;;
;; Every number is either odd or even
;;

(claim even-or-odd
  (Π ((n Nat))
    (Either (Even n) (Odd n))))

(claim even-or-odd-step
  (Π ((k-1 Nat))
    (-> (Either (Even k-1) (Odd k-1))
        (Either (Even (add1 k-1)) (Odd (add1 k-1))))))

(define even-or-odd-step
  (λ (k-1)
    (λ (proof-k-1)
      (ind-Either proof-k-1
        (λ (_) (Either (Even (add1 k-1)) (Odd (add1 k-1))))
        (λ (proof-even)
          (right (add1-even->odd k-1 proof-even)))
        (λ (proof-odd)
          (left (add1-odd->even k-1 proof-odd)))))))

(define even-or-odd
  (λ (n)
    (ind-Nat n
      (λ (k) (Either (Even k) (Odd k)))
      (left zero-is-even)
      even-or-odd-step)))

;;
;; 14. There is safety in numbers
;;

(claim Maybe
  (-> U U))
(define Maybe
  (λ (X) (Either X Trivial)))

(claim nothing
  (Π ((E U)) (Maybe E)))
(define nothing
  (λ (E)
    (right sole)))

(claim just
  (Π ((E U)) (-> E (Maybe E))))
(define just
  (λ (E x) (left x)))

(claim maybe-head
  (Π ((E U))
    (-> (List E) (Maybe E))))
(define maybe-head
  (λ (E)
    (λ (lst)
      (rec-List lst
        (nothing E)
        (λ (hd tl acc)
          (just E hd))))))

(claim maybe-tail
  (Π ((E U))
    (-> (List E) (Maybe (List E)))))
(define maybe-tail
  (λ (E)
    (λ (lst)
      (rec-List lst
        (nothing (List E))
        (λ (hd tl acc)
          (just (List E) tl))))))

(claim list-ref
  (Π ((E U))
    (-> Nat (List E) (Maybe E))))
(define list-ref
  (λ (E)
    (λ (k)
      (rec-Nat k
        (maybe-head E)
        (λ (k-1 acc)
          (λ (es)
            (ind-Either (maybe-tail E es)
              (λ (_) (Maybe E))
              (λ (tl) (acc tl))
              (λ (_) (nothing E)))))))))

;; 
;; (Fin N)
;; 
(claim Fin
  (-> Nat U))
(define Fin
  (λ (n)
    (iter-Nat n
      Absurd
      Maybe)))

(claim fzero
  (Π ((n Nat))
    (Fin (add1 n))))

(define fzero
  (λ (n)
    (nothing (Fin n))))

(claim fadd1
  (Π ((n Nat))
    (-> (Fin n) (Fin (add1 n)))))

(define fadd1
  (λ (n)
    (λ (i-1)
      (just (Fin n) i-1))))

(claim vec-ref
  (Π ((E U)
      (l Nat))
    (-> (Fin l) (Vec E l) E)))

(claim vec-ref-base
  (Π ((E U))
    (-> (Fin zero) (Vec E zero)
        E)))
(define vec-ref-base
  (λ (E)
    (λ (no-value es)
      (ind-Absurd no-value
        E))))

(claim vec-ref-step
  (Π ((E U)
      (l-1 Nat))
    (-> (-> (Fin l-1)
            (Vec E l-1)
            E)
        (-> (Fin (add1 l-1))
            (Vec E (add1 l-1))
            E))))

(define vec-ref-step
  (λ (E l-1)
    (λ (vec-ref-l-1)
      (λ (i es)
        (ind-Either i
          (λ (i) E)
          (λ (i-1) (vec-ref-l-1 i-1 (tail es)))
          (λ (triv) (head es)))))))
    
(define vec-ref
  (λ (E l)
    (ind-Nat l
      (λ (k)
        (-> (Fin k) (Vec E k) E))
      (vec-ref-base E)
      (vec-ref-step E))))
        

;;
;;

(claim =consequence
  (-> Nat Nat U))

(define =consequence
  (λ (n j)
    (which-Nat n
      ;; n=0
      (which-Nat j
        ;; j=0
        Trivial
        (λ (j-1) Absurd))
      ;; n!=0
      (λ (n-1)
        (which-Nat j
          ;; j=0
          Absurd
          (λ (j-1)
            (= Nat n-1 j-1)))))))

(claim =consequence-same
  (Π ((n Nat))
    (=consequence n n)))

(define =consequence-same
  (λ (n)
    (ind-Nat n
      (λ (k)
        (=consequence k k))
      sole
      (λ (n-1 almost)
        (same n-1)))))


(claim use-Nat=
  ;; for every n and j Nats, if they are
  ;; equal, then consequence of they being
  ;; equal follows.
  (Π ((n Nat)
      (j Nat))
    (-> (= Nat n j)
        (=consequence n j))))
      
(define use-Nat=
  (λ (n j)
    (λ (n=j)
      (replace n=j
        (λ (k) (=consequence n k))
        (=consequence-same n)))))

(claim zero-not-add1
  (Π ((n Nat))
    (-> (= Nat zero (add1 n))
        Absurd)))
(define zero-not-add1
  (λ (n)
    (use-Nat= zero (add1 n))))
  
;;
;; pem, middle excluded...
;;

;; Every statement is either true or false
;(claim pem
;  (-> X (Either X (-> X Abusrd))))

(claim pem-not-false
  (Π ((X U))
    (-> (-> (Either X (-> X Absurd))
            Absurd)
        Absurd)))

(define pem-not-false
  (λ (X)
    (λ (pem-false)
      (pem-false
        (right
          (λ (x)
            (pem-false (left x))))))))

(claim Dec
  (-> U U))

(define Dec
  (λ (X)
    (Either X (-> X Absurd))))

(claim zero?
  (Π ((j Nat))
    (Dec (= Nat zero j))))

(define zero?
  (λ (j)
    (ind-Nat j
      (λ (k) (Dec (= Nat zero k)))
      (left (same 0))
      (λ (j-1 zero?n-1)
        (right (zero-not-add1 j-1))))))

(claim add1-not-zero
  (Π ((n Nat))
    (-> (= Nat (add1 n) zero)
      Absurd)))
(define add1-not-zero
  (λ (n) (use-Nat= (add1 n) zero)))
      

(claim mot-nat=?
  (-> Nat U))
(define mot-nat=?
  (λ (k)
    (Π ((j Nat))
      (Dec (= Nat k j)))))

(claim sub1=
  (Π ((n Nat)
      (j Nat))
    (-> (= Nat (add1 n) (add1 j))
        (= Nat n j))))
(define sub1=
  (λ (n j)
    (use-Nat= (add1 n) (add1 j))))

(claim dec-add1=
  (Π ((n-1 Nat)
      (j-1 Nat))
    (-> (Dec (= Nat n-1 j-1))
        (Dec (= Nat (add1 n-1) (add1 j-1))))))
(define dec-add1=
  (λ (n-1 j-1 eq-or-not)
    (ind-Either eq-or-not
      (λ (_target)
        (Dec (= Nat (add1 n-1) (add1 j-1))))
      (λ (yes)
        (left (cong yes (+ 1))))
      (λ (no)
        (right (λ (n=j)
                 (no (sub1= n-1 j-1 n=j))))))))

(claim nat=-step
  (Π ((n-1 Nat))
    (-> (mot-nat=? n-1)
        (mot-nat=? (add1 n-1)))))
(define nat=-step
  (λ (n-1 nat=?n-1 j)
    (ind-Nat j
      (λ (k) (Dec (= Nat (add1 n-1) k)))
      (right (add1-not-zero n-1))
      (λ (j-1 _)
        (dec-add1= n-1 j-1
          (nat=?n-1 j-1))))))
    

(claim nat=?
  (Π ((n Nat)
      (j Nat))
    (Dec (= Nat n j))))

(define nat=?
  (λ (n j)
    ((ind-Nat n
       mot-nat=?
       zero?
       nat=-step)
    j)))