Programs from "The Little Typer"

ackermann.pie

#lang pie

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim repeat
  (→ (→ Nat Nat) Nat
    Nat))
(define repeat
  (λ (f n)
    (iter-Nat
      n
      (f 1)
      (λ (iter) (f iter)))))

(claim ackermann
  (→ Nat Nat
    Nat))
(define ackermann
  (λ (n)
    (iter-Nat
      n
      (+ 1)
      (λ (ack) (repeat ack)))))

contra.pie

#lang pie

(claim =consequence
  (→ Nat Nat
    U))
(define =consequence
  (λ (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)))))))

(claim =consequence-same
  (∏ ((n Nat))
    (=consequence n n)))
(define =consequence-same
  (λ (n)
    (ind-Nat n
      (λ (k) (=consequence k k))
      sole
      (λ (n-1 prf) (same n-1)))))

(claim use-Nat=
  (∏ ((m Nat) (n Nat))
    (→ (= Nat m n)
      (=consequence m n))))
(define use-Nat=
  (λ (m n prf)
    (replace prf
      (λ (k) (=consequence m k))
      (=consequence-same m))))

(claim zero-not-add1
  (∏ ((n Nat))
    (→ (= Nat zero (add1 n))
      Absurd)))
(define zero-not-add1
  (λ (n prf)
    (use-Nat= zero (add1 n) prf)))

(claim donut-absurdity
  (→ (= Nat 0 6)
    (= Atom 'powdered 'glazed)))
(define donut-absurdity
  (λ (prf)
    (ind-Absurd (use-Nat= 0 6 prf)
      (= Atom 'powdered 'glazed))))

(claim sub1=
  (∏ ((m Nat) (n Nat))
    (→ (= Nat (add1 m) (add1 n))
      (= Nat m n))))
(define sub1=
  (λ (m n)
    (use-Nat= (add1 m) (add1 n))))

(claim one-not-six
  (→ (= Nat 1 6) Absurd))
(define one-not-six
  (λ (prf)
    (zero-not-add1 4 (sub1= 0 5 prf))))

(claim front
  (∏ ((A U) (n Nat))
    (→ (Vec A (add1 n))
      A)))
(define front
  (λ (A n xs)
    ((ind-Vec (add1 n) xs
       (λ (k ys)
         (∏ ((j Nat))
           (→ (= Nat k (add1 j))
             A)))
       (λ (k prf)
         (ind-Absurd (zero-not-add1 k prf) A))
       (λ (k y ys f j prf) y))
      n (same (add1 n)))))

(claim pem-not-false
  (∏ ((X U))
    (→ (→ (Either X (→ X Absurd))
         Absurd)
      Absurd)))
(define pem-not-false
  (λ (X contra)
    (contra (right (λ (x) (contra (left x)))))))

dec.pie

#lang pie

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim =consequence
  (→ Nat Nat
    U))
(define =consequence
  (λ (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)))))))

(claim =consequence-same
  (∏ ((n Nat))
    (=consequence n n)))
(define =consequence-same
  (λ (n)
    (ind-Nat n
      (λ (k) (=consequence k k))
      sole
      (λ (n-1 prf) (same n-1)))))

(claim use-Nat=
  (∏ ((m Nat) (n Nat))
    (→ (= Nat m n)
      (=consequence m n))))
(define use-Nat=
  (λ (m n prf)
    (replace prf
      (λ (k) (=consequence m k))
      (=consequence-same m))))

(claim zero-not-add1
  (∏ ((n Nat))
    (→ (= Nat zero (add1 n))
      Absurd)))
(define zero-not-add1
  (λ (n prf)
    (use-Nat= zero (add1 n) prf)))

(claim sub1=
  (∏ ((m Nat) (n Nat))
    (→ (= Nat (add1 m) (add1 n))
      (= Nat m n))))
(define sub1=
  (λ (m n)
    (use-Nat= (add1 m) (add1 n))))

; new stuff starts here

(claim Dec (→ U U))
(define Dec
  (λ (X)
    (Either X (→ X Absurd))))

(claim zero?
  (∏ ((n Nat)) (Dec (= Nat zero n))))
(define zero?
  (λ (n)
    (ind-Nat n
      (λ (k) (Dec (= Nat zero k)))
      (left (same zero))
      (λ (n-1 prf-or-contra)
        (right (zero-not-add1 n-1))))))

        ; my alternate body for (λ (n-1 prf-or-contra))
        ; (ind-Either prf-or-contra
        ;   (λ (e) (Dec (= Nat zero (add1 n-1))))
        ;   (λ (l) (right (λ (contra) (zero-not-add1 n-1 contra))))
        ;   (λ (r) (right (λ (contra) (zero-not-add1 n-1 contra)))))))))

(claim motive-add1-not= (→ Nat U))
(define motive-add1-not=
  (λ (n)
    (→ (= Nat (add1 n) n)
      Absurd)))

(claim step-add1-not=
  (∏ ((n-1 Nat))
    (→ (→ (= Nat (add1 n-1) n-1)
         Absurd)
      (→ (= Nat (add1 (add1 n-1)) (add1 n-1))
        Absurd))))
(define step-add1-not=
  (λ (n-1 contra prf)
    (contra (sub1= (add1 n-1) n-1 prf))))

(claim add1-not=
  (∏ ((n Nat))
    (→ (= Nat (add1 n) n)
      Absurd)))
(define add1-not=
  (λ (n)
    (ind-Nat n
      motive-add1-not=
      (λ (contra) (zero-not-add1 0 (symm contra)))
      step-add1-not=)))

(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 dec-1)
    (ind-Either dec-1
      (λ (e) (Dec (= Nat (add1 n-1) (add1 j-1))))
      (λ (l) (left (cong l (+ 1))))
      (λ (r) (right (λ (prf) (r (sub1= n-1 j-1 prf))))))))

(claim mot-nat=? (→ Nat U))
(define mot-nat=?
  (λ (k)
    (∏ ((j Nat))
      (Dec (= Nat k j)))))

(claim base-nat=?
  (∏ ((j Nat))
    (Dec (= Nat 0 j))))
(define base-nat=? zero?)

(claim step-nat=?
  (∏ ((n-1 Nat))
    (→ (∏ ((j Nat)) (Dec (= Nat n-1 j)))
      (∏ ((j Nat)) (Dec (= Nat (add1 n-1) j))))))

; my first attempt, which proved unworkable on the right branch
; (define step-nat=?
;   (λ (n-1 dec-1 j)
;     (ind-Either (dec-1 j)
;       (λ (e) (Dec (= Nat (add1 n-1) j)))
;       (λ (l)
;         (right (λ (prf)
;                  (add1-not= j
;                    (replace l
;                      (λ (k) (= Nat (add1 k) j))
;                      prf)))))
;       (λ (r)
;         TODO))))

(define step-nat=?
  (λ (n-1 dec-n-1 j)
    (ind-Nat j
      (λ (k) (Dec (= Nat (add1 n-1) k)))
      (right (λ (contra) (zero-not-add1 n-1 (symm contra))))
      (λ (j-1 dec-j-1)
        (dec-add1= n-1 j-1 (dec-n-1 j-1))))))

(claim nat=?
  (∏ ((m Nat) (n Nat))
    (Dec (= Nat m n))))
(define nat=?
  (λ (m n)
    ((ind-Nat m
      mot-nat=?
      base-nat=?
      step-nat=?)
     n)))

dpairs.pie

#lang pie

(claim list-length
  (∏ ((A U))
    (→ (List A) Nat)))
(define list-length
  (λ (A xs)
    (rec-List
      xs
      0
      (λ (y ys n) (add1 n)))))

; my first blind attempt

; for a given list, what type of Vec do we make?
(claim motive-list-to-vec
  (∏ ((A U))
    (→ (List A) U)))
(define motive-list-to-vec
  (λ (A xs)
    (Vec A (list-length A xs))))

(claim list-to-vec
  (∏ ((A U))
    (→ (List A)
      (Σ ((n Nat))
        (Vec A n)))))
(define list-to-vec
  (λ (A xs)
    (cons
      (list-length A xs)
      (ind-List
        xs
        (motive-list-to-vec A)
        vecnil
        (λ (y ys v) (vec:: y v))))))

; the "direct" approach shown in the book

(claim list→vec
  (∏ ((A U))
    (→ (List A)
      (Σ ((n Nat))
        (Vec A n)))))
(define list→vec
  (λ (A xs)
    (rec-List
      xs
      (the (Σ ((n Nat)) (Vec A n)) (cons 0 vecnil))
      (λ (y ys p)
        (cons
          (add1 (car p))
          (vec:: y (cdr p)))))))

; but neither actually ensures correctness...

(claim good-list-to-vec
  (∏ ((A U) (xs (List A)))
    (Vec A (list-length A xs))))
(define good-list-to-vec
  (λ (A xs)
    (ind-List
      xs
      (motive-list-to-vec A)
      vecnil
      (λ (y ys v) (vec:: y v)))))

; now some more stuff for vecs

(claim repeat
  (∏ ((A U) (n Nat))
    (→ A (Vec A n))))
(define repeat
  (λ (A n x)
    (ind-Nat
      n
      (λ (n) (Vec A n))
      vecnil
      (λ (n xs) (vec:: x xs)))))

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim vec-++
  (∏ ((A U) (m Nat) (n Nat))
    (→ (Vec A m) (Vec A n)
      (Vec A (+ m n)))))
(define vec-++
  (λ (A m n xs ys)
    (ind-Vec
      m
      xs
      (λ (k v) (Vec A (+ k n)))
      ys
      (λ (k e es result) (vec:: e result)))))

(claim vec-to-list
  (∏ ((A U) (n Nat))
    (→ (Vec A n) (List A))))
(define vec-to-list
  (λ (A n xs)
    (ind-Vec
      n
      xs
      (λ (k v) (List A))
      nil
      (λ (k e es l) (:: e l)))))

(claim list-vec-roundtrip=
  (∏ ((A U) (xs (List A)))
    (= (List A)
      xs
      (vec-to-list
        A
        (list-length A xs)
        (good-list-to-vec A xs)))))

(define list-vec-roundtrip=
  (λ (A xs)
    (ind-List
      xs
      (λ (xs)
        (= (List A)
          xs
          (vec-to-list A (list-length A xs) (good-list-to-vec A xs))))
      (same nil)
      (λ (e es prf)
        (cong prf 
          (the (→ (List A) (List A)) (λ (ys) (:: e ys))))))))

evens.pie

#lang pie

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

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

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

(claim +two-even
  (∏ ((n Nat))
    (→ (Even n)
      (Even (+ 2 n)))))
(define +two-even
  (λ (n prf)
    (cons
      (add1 (car prf))
      (cong (cdr prf) (+ 2)))))

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

(claim +two-odd
  (∏ ((n Nat))
    (→ (Odd n)
      (Odd (+ 2 n)))))
(define +two-odd
  (λ (n prf)
    (cons
      (add1 (car prf))
      (cong (cdr prf) (+ 2)))))

(claim +one-even-odd
  (∏ ((n Nat))
    (→ (Even n)
      (Odd (add1 n)))))
(define +one-even-odd
  (λ (n prf)
    (cons
      (car prf)
      (cong (cdr prf) (+ 1)))))

(claim +one-odd-even
  (∏ ((n Nat))
    (→ (Odd n)
      (Even (add1 n)))))
(define +one-odd-even
  (λ (n prf)
    (cons
      (add1 (car prf))
      (cong (cdr prf) (+ 1)))))

(claim step-even-or-odd
  (∏ ((n Nat))
    (→ (Either (Even n) (Odd n))
      (Either (Even (add1 n)) (Odd (add1 n))))))
(define step-even-or-odd
  (λ (n prf)
    (ind-Either
      prf
      (λ (prf) (Either (Even (add1 n)) (Odd (add1 n))))
      (λ (prf-even) (right (+one-even-odd n prf-even)))
      (λ (prf-odd) (left (+one-odd-even n prf-odd))))))

(claim even-or-odd
  (Π ((n Nat))
    (Either (Even n) (Odd n))))
(define even-or-odd
  (λ (n)
    (ind-Nat
      n
      (λ (k) (Either (Even k) (Odd k)))
      (left (cons 0 (same 0)))
      step-even-or-odd)))

lists.pie

#lang pie

(claim length
  (∏ ((A U))
    (→ (List A) Nat)))
(define length
  (λ (A xs)
    (rec-List xs
      0
      (λ (x xs len) (add1 len)))))

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim sum
  (→ (List Nat) Nat))
(define sum
  (λ (xs)
    (rec-List xs
      0
      (λ (x xs acc) (+ x acc))))) 

(claim ++
  (∏ ((A U))
    (→ (List A) (List A)
      (List A))))
(define ++
  (λ (A xs ys)
    (rec-List xs
      ys
      (λ (x xs acc) (:: x acc)))))

(claim snoc
  (∏ ((A U))
    (→ A (List A)
      (List A))))
(define snoc
  (λ (A x xs)
    (rec-List xs
      (:: x nil)
      (λ (x xs acc) (:: x acc)))))

(claim reverse
  (∏ ((A U))
    (→ (List A)
      (List A))))
(define reverse
  (λ (A xs)
    (rec-List xs
      (the (List A) nil)
      (λ (x xs acc) (snoc A x acc)))))

maybe.pie

#lang pie

; silly authors, errors go on the Left

(claim Maybe (→ U U))
(define Maybe (λ (A) (Either Trivial A)))

(claim nothing (∏ ((A U)) (Maybe A)))
(define nothing (λ (A) (left sole)))

(claim just (∏ ((A U)) (→ A (Maybe A))))
(define just (λ (A x) (right x)))

(claim safe-head
  (∏ ((A U))
    (→ (List A)
      (Maybe A))))
(define safe-head
  (λ (A xs)
    (rec-List
      xs
      (nothing A)
      (λ (y ys h) (just A y)))))

(claim safe-tail
  (∏ ((A U))
    (→ (List A)
      (Maybe (List A)))))
(define safe-tail
  (λ (A xs)
    (rec-List
      xs
      (nothing (List A))
      (λ (y ys h) (just (List A) ys)))))

(claim safe-ix
  (∏ ((A U))
    (→ Nat (List A)
      (Maybe A))))
(define safe-ix
  (λ (A ix)
    (rec-Nat
      ix
      (safe-head A)
      (λ (n f xs)
        (ind-Either
          (safe-tail A xs)
          (λ (e) (Maybe A))
          (λ (l) (left l))
          (λ (r) (f r)))))))

(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 f)
    (just (Fin n) f)))

(claim vec-ix
  (∏ ((A U) (n Nat))
    (→ (Fin n) (Vec A n)
      A)))
(define vec-ix
  (λ (A n)
    (ind-Nat
      n
      (λ (k) (→ (Fin k) (Vec A k) A))
      (λ (ix xs) (ind-Absurd ix A)) ; can't happen!
      (λ (n f ix xs)
        (ind-Either
          ix
          (λ (e) A)
          (λ (l) (head xs))
          (λ (r) (f r (tail xs))))))))

numbers.pie

; run with EXACTLY racket -l pie -t numbers.pie -i
#lang pie
(claim add2 (→ Nat Nat))
(define add2 (λ (x) (add1 (add1 x))))

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim * (→ Nat Nat Nat))
(define *
  (λ (x y)
    (iter-Nat x
      0
      (λ (acc) (+ acc y)))))

(claim fac-step (→ Nat Nat Nat))
(define fac-step (λ (n-1 acc) (* (add1 n-1) acc)))

(claim fac (→ Nat Nat))
(define fac
  (λ (x)
    (rec-Nat x
      1
      fac-step)))

pears.pie

; run with EXACTLY racket -l pie -t pears.pie -i
#lang pie

(claim Pear U)
(define Pear (Pair Nat Nat))

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim Pear-+ (→ Pear Pear Pear))
(define Pear-+
  (λ (x y)
    (cons (+ (car x) (car y)) (+ (cdr x) (cdr y)))))

(claim Pear-+-Pi (∏ ((x Pear) (y Pear)) Pear))
(define Pear-+-Pi
  (λ (x y)
    (cons (+ (car x) (car y)) (+ (cdr x) (cdr y)))))

pi.pie

#lang pie

(claim rev-pair
  (∏ ((A U) (D U))
    (→ (Pair A D) (Pair D A))))
(define rev-pair
  (λ (A D p)
    (cons (cdr p) (car p))))

(claim elim-Pair
  (∏ ((A U) (D U) (X U))
    (→ (Pair A D) (→ A D X) X)))
(define elim-Pair
  (λ (A D X p f)
    (f (car p) (cdr p))))

(claim rev-pair2
  (∏ ((A U) (D U))
    (→ (Pair A D) (Pair D A))))
(define rev-pair2
  (λ (A D p)
    (elim-Pair A D (Pair D A)
      p
      (λ (a d) (cons d a)))))

proof.pie

#lang pie

(claim + (→ Nat Nat Nat))
(define +
  (λ (x y)
    (iter-Nat x
      y
      (λ (acc) (add1 acc)))))

(claim +1=add1
  (∏ ((n Nat))
    (= Nat (+ 1 n) (add1 n))))
(define +1=add1
  (λ (n)
    (same (add1 n))))

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

(claim step-incr=add1
  (∏ ((n Nat))
    (→ (= Nat (incr n) (add1 n))
      (= Nat (incr (add1 n)) (add1 (add1 n))))))
(define step-incr=add1
  (λ (n prf)
    (cong prf
      (the (→ Nat Nat) (λ (x) (add1 x))))))

(claim incr=add1
  (∏ ((n Nat))
    (= Nat (incr n) (add1 n))))
(define incr=add1
  (λ (n)
    (ind-Nat
      n
      (λ (n) (= Nat (incr n) (add1 n)))
      (same 1)
      step-incr=add1)))

(claim replace-step-incr=add1
  (∏ ((n Nat))
    (→ (= Nat (incr n) (add1 n))
      (= Nat (add1 (incr n)) (add1 (add1 n))))))
(define replace-step-incr=add1
  (λ (n prf)
    (replace prf
      (λ (x) (= Nat (add1 (incr n)) (add1 x)))
      (same (add1 (incr n))))))

(claim replace-incr=add1
  (∏ ((n Nat))
    (= Nat (incr n) (add1 n))))
(define replace-incr=add1
  (λ (n)
    (ind-Nat
      n
      (λ (n) (= Nat (incr n) (add1 n)))
      (same 1)
      step-incr=add1)))

(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
      (λ (n) (= Nat (add1 (+ n m)) (+ n (add1 m))))
      (same (add1 m))
      (λ (n-1 prf)
        (cong prf
          (the (→ Nat Nat) (λ (x) (add1 x))))))))

(claim step-twice=double
  (∏ ((n-1 Nat))
    (→ (= Nat (twice n-1) (double n-1))
      (= Nat (twice (add1 n-1)) (double (add1 n-1))))))
(define step-twice=double
  (λ (n-1 prf)
    (replace
      (add1+=+add1 n-1 n-1)
      (λ (m)
        (= Nat (add1 m) (add1 (add1 (double n-1)))))
      (cong prf (+ 2)))))

(claim twice=double
  (∏ ((n Nat))
    (= Nat (twice n) (double n))))
(define twice=double
  (λ (n)
    (ind-Nat
      n
      (λ (k) (= Nat (twice k) (double k)))
      (same 0)
      step-twice=double)))

(claim double-Vec
  (∏ ((A U) (n Nat))
    (→ (Vec A n) (Vec A (double n)))))
(define double-Vec
  (λ (A n)
    (ind-Nat
      n
      (λ (k) (→ (Vec A k) (Vec A (double k))))
      (λ (xs) vecnil)
      (λ (n f)
        (λ (xs)
          (vec:: (head xs) (vec:: (head xs) (f (tail xs)))))))))

(claim twice-Vec
  (∏ ((A U) (n Nat))
    (→ (Vec A n) (Vec A (twice n)))))
(define twice-Vec
  (λ (A n xs)
    (replace (symm (twice=double n))
      (λ (k) (Vec A k))
      (double-Vec A n xs))))

todo.pie

#lang pie
(claim xyz TODO)
(claim xyzzy (∏ ((n Nat)) TODO))

vecs.pie

#lang pie

(claim first
  (∏ ((A U) (n Nat))
    (→ (Vec A (add1 n))
      A)))
(define first
  (λ (A n xs)
    (head xs)))

(claim rest
  (∏ ((A U) (n Nat))
    (→ (Vec A (add1 n))
      (Vec A n))))
(define rest
  (λ (A n xs)
    (tail xs)))

(claim repeat
  (∏ ((A U) (n Nat))
    (→ A (Vec A n))))
(define repeat
  (λ (A n x)
    (ind-Nat
      n
      (λ (n) (Vec A n))
      vecnil
      (λ (n xs) (vec:: x xs)))))

(claim last
  (∏ ((A U) (n Nat))
    (→ (Vec A (add1 n)) A)))
(define last
  (λ (A n)
    (ind-Nat
      n
      (λ (n) (→ (Vec A (add1 n)) A))
      (λ (xs) (head xs))
      (λ (n f) (λ (xs) (f (tail xs)))))))

(claim drop-last
  (∏ ((A U) (n Nat))
    (→ (Vec A (add1 n))
      (Vec A n))))
(define drop-last
  (λ (A n)
    (ind-Nat
      n
      (λ (n)
        (→ (Vec A (add1 n))
          (Vec A n)))
      (λ (xs) vecnil)
      (λ (n f)
        (λ (xs)
          (vec:: (head xs) (f (tail xs))))))))