Playing with The Little Typer's Pie lang https://github.com/the-little-typer/pie

pie.rkt

#lang pie

;; General

(claim Not
  (-> U U))
(define Not
  (λ (T)
    (-> T Absurd)))

;;; Nats

(claim one
  Nat)
(define one
  (add1 zero))

(claim two
  Nat)
(define two
  (add1 one))

(claim three
  Nat)
(define three
  (add1 two))

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

(claim four
  Nat)
(define four
  (+ two two))

(claim *
  (-> Nat Nat
    Nat))
(define *
  (λ (a b)
    (iter-Nat b
      zero
      (+ a))))

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

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

(claim incr=add1
  (Pi ((n Nat))
    (= Nat (incr n) (add1 n))))
(claim step-incr=add1
  (Pi ((n Nat))
    (-> (= Nat (incr n) (add1 n))
      (= Nat (add1 (incr n)) (add1 (add1 n))))))
(define step-incr=add1
  (λ (n-1 almost)
    (cong almost (+ 1))))
(define incr=add1
  (λ (n)
    (ind-Nat n
      (λ (x)
        (= Nat (incr x) (add1 x)))
      (same 1)
      step-incr=add1)))

(claim add1+=+add1
  (Pi ((i Nat)
       (j Nat))
    (= Nat
       (add1 (+ i j))
       (+ i (add1 j)))))
(define add1+=+add1
  (λ (i j)
    (ind-Nat i
      (λ (k)
        (= Nat
          (add1 (+ k j))
          (+ k (add1 j))))
      (same (add1 j))
      (λ (k-1 almost)
        (cong almost (+ 1))))))

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

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

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

(define twice=double
  (λ (n)
    (ind-Nat n
      (λ (x)
        (= Nat (twice x) (double x)))
      (same zero)
      (λ (n-1 almost)
        ; almost   :: (= Nat              (twice n-1)               (double n-1))
        ;          :: (= Nat              (+ n-1 n-1)               (double n-1))
        ; (cong almost (+ 2))
        ;          :: (= Nat  (add1 (add1 (+ n-1 n-1))) (add1 (add1 (double n-1))))
        ; (replace (add1+=+add1 n-1 n-1) ... (cong almost (+ 2)))
        ;          :: (= Nat  (add1 (+ n-1 (add1 n-1))) (add1 (add1 (double n-1))))
        ; goal     :: (= Nat        (twice (add1 n-1))        (double (add1 n-1)))
        ;          :: (= Nat (+ (add1 n-1) (add1 n-1))  (add1 (add1 (double n-1))))
        ;          :: (= Nat  (add1 (+ n-1 (add1 n-1))) (add1 (add1 (double n-1))))
        (replace (add1+=+add1 n-1 n-1)
          (λ (add1+)
            (= Nat (add1 add1+) (add1 (add1 (double n-1)))))
          (cong almost (+ 2)))))))

(claim Even
  (-> Nat U))
(define Even
  (λ (x)
    (Sigma ((half Nat))
      (= Nat x (double half)))))

(claim Odd
  (-> Nat U))
(define Odd
  (λ (x)
    (Sigma ((haf Nat))
      (= Nat x (add1 (double haf))))))

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

(claim +2-even
  (Pi ((x Nat))
    (-> (Even x)
      (Even (+ 2 x)))))
(define +2-even
  (λ (x x-even)
    (cons (add1 (car x-even)) (cong (cdr x-even) (+ 2)))))

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

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

(claim  nats-are-even-or-odd
  (Pi ((x Nat))
    (Either (Even x) (Odd x))))
(define nats-are-even-or-odd
  (λ (n)
    (ind-Nat n
      (λ (x)
        (Either (Even x) (Odd x)))
      (left zero-is-even)
      (λ (n-1 almost)
        (ind-Either almost
          (λ (almost)
            (Either (Even (add1 n-1)) (Odd (add1 n-1))))
          (λ (n-1-is-even) (right (add1-even->odd n-1 n-1-is-even)))
          (λ (n-1-is-odd) (left (add1-odd->even n-1 n-1-is-odd))))))))

(claim non-even->odd
  (Pi ((x Nat))
    (-> (-> (Even x) Absurd)
      (Odd x))))
(define non-even->odd
  (λ (x x-not-even)
    (ind-Either (nats-are-even-or-odd x)
      (λ (_) (Odd x))
      (λ (x-even)
        (ind-Absurd (x-not-even x-even)
          (Odd x)))
      (λ (x-odd) x-odd))))

(claim =consequence
  (-> Nat Nat U))
(define =consequence
  (λ (i j)
    (which-Nat i
      (which-Nat j
        Trivial
        (λ (_) Absurd))
      (λ (i-1)
        (which-Nat j
          Absurd
          (λ (j-1)
            (= Nat i-1 j-1)))))))

(claim =consequence-same
  (Pi ((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=
  (Pi ((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
  (Pi ((n Nat))
    (-> (= Nat 0 (add1 n)) Absurd)))
(define zero-not-add1
  (λ (n)
    (use-Nat= 0 (add1 n))))

(claim Dec
  (-> U U))
(define Dec
  (λ (T)
    (Either T (-> T Absurd))))

(claim zero?
  (Pi ((n Nat))
    (Dec (= Nat zero n))))
(define zero?
  (λ (n)
    (ind-Nat n
      (λ (k)
        (Dec (= Nat zero k)))
      (left (same zero))
      (λ (n-1 almost-zero?)
        (right (zero-not-add1 n-1))))))

(claim Pos
  (-> Nat U))
(define Pos
  (λ (n)
    (Sigma ((pred Nat))
      (= Nat (add1 pred) n))))

(claim zero-or-pos
  (Pi ((n Nat))
    (Either (= Nat zero n)
            (Pos n))))
(define zero-or-pos
  (λ (n)
    (ind-Nat n
      (λ (k)
        (Either (= Nat zero k)
          (Pos k)))
      (left (same zero))
      (λ (n-1 zero-or-pos-n-1)
        (right (cons n-1 (same (add1 n-1))))))))

(claim n=n+0
  (Pi ((n Nat))
    (= Nat n (+ n 0))))
(define n=n+0
  (λ (n)
    (ind-Nat n
      (λ (k)
        (= Nat k (+ k 0)))
      (same zero)
      (λ (k-1 k-1=n-1+0)
        (cong k-1=n-1+0 (+ 1))))))

(claim n+m=m+n
  (Pi ((n Nat)
       (m Nat))
    (= Nat (+ n m) (+ m n))))
(define n+m=m+n
  (λ (n m)
    (ind-Nat n
      (λ (k)
        (= Nat (+ k m) (+ m k)))
      (n=n+0 m)
      (λ (k-1 k-1+m=m+k-1)
        (replace (add1+=+add1 m k-1)
          (λ (x)
            (= Nat (add1 (+ k-1 m)) x))
          (cong k-1+m=m+k-1 (+ 1)))))))

(claim n!=add1-n
  (Pi ((n Nat))
    (-> (= Nat n (add1 n))
      Absurd)))
(define n!=add1-n
  (λ (n)
    (ind-Nat n
      (λ (k)
        (-> (= Nat k (add1 k)) Absurd))
      (zero-not-add1 0)
      (λ (n-1 n-1!=n n=n+1)
        (n-1!=n
          (use-Nat= (add1 n-1) (add1 (add1 n-1)) n=n+1))))))

(claim =?
  (Pi ((n Nat)
       (m Nat))
    (Dec (= Nat n m))))
(define =?
  (λ (n)
    ; first we induce over n
    ; we satrt we zero?, which is a "decider if zero is equal to some Nat"
    ; and we step by
    ;   given a "decider if k-1 is equal to some Nat",
    ;   build a "decider if k is equal to some Nat",
    (ind-Nat n
      (λ (k)
        (Pi ((m Nat))
          (Dec (= Nat k m))))
      zero?
      (λ (k-1 k-1=? m)
        ; here, k-1=? is a "decider if k-1 is equal to some Nat"
        ; now we do case analysis on m:
        (ind-Nat m
          (λ (l)
            (Dec (= Nat (add1 k-1) l)))
          ; if m is zero, we know k!=m, because k = (add1 k-1) and zero-not-add1
          (right (λ (1+k-1=zero)
                   (zero-not-add1 k-1
                     (symm 1+k-1=zero))))
          ; if m is (add1 m-1)
          ; we can use (k-1=? m-1) to find (Dec (= Nat k-1 m-1))
          ; and then we uset han to get a (Dec (= Nat k m))
          (λ (m-1 _almost)
            (ind-Either (k-1=? m-1)
              (λ (_)
                (Dec (= Nat (add1 k-1) (add1 m-1))))
              (λ (k-1=m-1)
                ; (= Nat k-1 m-1) -> (= Nat k m) via cong
                (left (cong k-1=m-1 (+ 1))))
              (λ (k-1!=m-1)
                ; (Not (= Nat k-1 m-1)) -> (Not (= Nat k m)) requires a little more work
                ; to prove it, we need (= Nat k m) -> (= Nat k-1 m-1)
                ; which we can find with use-Nat
                (right (λ (1+n-1=1+j-1)
                         (k-1!=m-1 (use-Nat= (add1 k-1) (add1 m-1) 1+n-1=1+j-1))))))))))))

(claim LessThan
  (-> Nat Nat U))
(define LessThan
  (λ (lower upper)
    (Sigma ((dif Nat))
      (= Nat (add1 (+ lower dif)) upper))))

(claim LessThanEq
  (-> Nat Nat U))
(define LessThanEq
  (λ (i j)
    (Either
      (LessThan i j)
      (= Nat i j))))

(claim zero-is-less-than-add1
  (Pi ((n Nat))
    (LessThan 0 (add1 n))))
(define zero-is-less-than-add1
  (λ (n)
    (cons n (same (add1 n)))))

(claim nothing<zero
  (Pi ((n Nat))
    (-> (LessThan n 0) Absurd)))
(define nothing<zero
  (λ (n n<zero)
    (zero-not-add1 (+ n (car n<zero)) (symm (cdr n<zero)))))

(claim <add1
  (Pi ((n Nat)
       (j Nat))
    (-> (LessThan n j)
      (LessThan n (add1 j)))))
(define <add1
  (λ (n j n<j)
    (cons (add1 (car n<j))
      (replace (add1+=+add1 n (car n<j))
        (λ (k)
          (= Nat (add1 k) (add1 j)))
        (cong (cdr n<j) (+ 1))))))

(claim <?
  (Pi ((lower Nat)
       (upper Nat))
    (Dec (LessThan lower upper))))
(define <?
  (λ (lower upper)
    (ind-Nat upper
      (λ (k)
        (Dec (LessThan lower k)))
      ; when upper = 0, < is false
      (right (nothing<zero lower))
      (λ (n-1 lower<?n-1)
        (ind-Either lower<?n-1
          (λ (_)
            (Dec (LessThan lower (add1 n-1))))
          (λ (lower<n-1)
            ; when lower < n-1, lower < n
            (left (<add1 lower n-1 lower<n-1)))
          (λ (not-lower<n-1)
            ; if lower is not < n-1, we check if lower = n-1
            (ind-Either (=? lower n-1)
              (λ (_)
                (Dec (LessThan lower (add1 n-1))))
              (λ (lower=n-1)
                ; if lower = n-1, then lower < n
                (left (cons 0
                        (replace lower=n-1
                          (λ (x)
                            (= Nat
                              (add1 (+ lower 0))
                              (add1 x)))
                          (cong (symm (n=n+0 lower)) (+ 1))))))
              (λ (lower!=n-1)
                ; otherwise, lower > n-1, we need to keep working
                (right (λ (lower<n)
                         (ind-Either (zero-or-pos (car lower<n))
                           (λ (_) Absurd)
                           (λ (zero=dif)
                             (lower!=n-1
                               (replace (symm (n=n+0 lower))
                                 (λ (x)
                                   (= Nat x n-1))
                                 (replace (symm zero=dif)
                                   (λ (x)
                                     (= Nat (+ lower x) n-1))
                                   (use-Nat= (add1 (+ lower (car lower<n))) (add1 n-1) (cdr lower<n))))))
                           (λ (zero!=dif)
                             (not-lower<n-1
                               (cons (car zero!=dif)
                                 ; lower<n means (= (add1 (+ lower (car lower<n))) (add1 n-1))
                                 ; and (car lower<n) = (add1 (car zero!=dif))
                                 ; thus (= (add1 (+ lower (add1 (car zero!=dif)))) (add1 n-1))
                                 ; thus (= (add1 (add1 (+ lower (car zero!=dif)))) (add1 n-1))
                                 ; thus (= (add1 (+ lower (car zero!=dif))) n-1)
                                 ; which is exactly what we need to build a fake proof that lower<n-1
                                 (use-Nat= (add1 (add1 (+ lower (car zero!=dif)))) (add1 n-1)
                                   (replace (symm (add1+=+add1 lower (car zero!=dif)))
                                     (λ (x)
                                       (= Nat (add1 x) (add1 n-1)))
                                     (replace (symm (cdr zero!=dif))
                                       (λ (x)
                                         (= Nat (add1 (+ lower x)) (add1 n-1)))
                                       (cdr lower<n))))))))))))))))))

(claim <=?
  (Pi ((n Nat)
       (m Nat))
    (Dec (LessThanEq n m))))
(define <=?
  (λ (n m)
    (ind-Either (<? n m)
      (λ (_) (Dec (LessThanEq n m)))
      (λ (n<m) (left (left n<m)))
      (λ (n!<m)
        (ind-Either (=? n m)
          (λ (_) (Dec (LessThanEq n m)))
          (λ (n=m) (left (right n=m)))
          (λ (n!=m)
            (right
              (λ (n<=m)
                (ind-Either n<=m
                  (λ (_) Absurd)
                  n!<m
                  n!=m)))))))))

(claim assoc-+
  (Pi ((m Nat)
       (n Nat)
       (o Nat))
    (= Nat (+ (+ m n) o) (+ m (+ n o)))))
(define assoc-+
  (λ (m n o)
    (ind-Nat m
      (λ (k)
        (= Nat (+ (+ k n) o) (+ k (+ n o))))
      (same (+ n o))
      (λ (k-1 k-1+n+o=k-1+n+o)
        (cong k-1+n+o=k-1+n+o (+ 1))))))

(claim trans-<=
  (Pi ((m Nat)
       (n Nat)
       (o Nat))
    (-> (LessThanEq m n)
        (LessThanEq n o)
        (LessThanEq m o))))
(define trans-<=
  (λ (m n o m<=n n<=o)
    (ind-Either m<=n
      (λ (_) (LessThanEq m o))
      (λ (m<n)
        (ind-Either n<=o
          (λ (_) (LessThanEq m o))
          (λ (n<o)
            (left
              (cons (add1 (+ (car m<n) (car n<o)))
                ; (cdr m<n) ~ (= Nat (add1 (+ m (car m<n))) n)
                ; (cdr n<o) ~ (= Nat (add1 (+ n (car n<o))) o)
                ; o
                ; (add1 (+ n (car n<o)))                      [replace (symm (cdr n<o))]
                ; (add1 (+ (add1 (+ m (car m<n))) (car n<o))) [replace (symm (cdr m<n))]
                ; (add1 (add1 (+ (+ m (car m<n)) (car n<o)))) (eval +)
                ; (add1 (add1 (+ m (+ (car m<n)) (car n<o)))) [replace assoc-+] TODO
                ; (add1 (+ m (add1 (+ (car m<n) (car n<o))))) [replace add1+=+add1]
                ; (add1 (+ m (add1 (+ (car m<n) (car n<o))))) [goal]
                (replace (add1+=+add1 m (+ (car m<n) (car n<o)))
                  (λ (x)
                    (= Nat (add1 x) o))
                  (replace (assoc-+ m (car m<n) (car n<o))
                    (λ (x)
                      (= Nat (add1 (add1 x)) o))
                    (replace (symm (cdr m<n))
                      (λ (x)
                        (= Nat (add1 (+ x (car n<o))) o))
                      (replace (symm (cdr n<o))
                        (λ (x) (= Nat x o))
                        (same o))))))))
          (λ (n=o)
            (replace n=o
              (λ (x)
                (LessThanEq m x))
              m<=n))))
      (λ (m=n)
        (replace (symm m=n)
          (λ (x)
            (LessThanEq x o))
          n<=o)))))

;;; Lists

(claim length
  (Pi ((E U))
    (-> (List E) Nat)))
(define length
  (λ (E list)
    (rec-List list
      0
      (λ (x xs) (+ 1)))))

(claim snoc
  (Pi ((E U))
    (-> (List E) E (List E))))
(define snoc
  (λ (E list new)
    (rec-List list
      (:: new nil)
      (λ (e _ es) (:: e es)))))

(claim reverse
  (Pi ((E U))
    (-> (List E) (List E))))
(define reverse
  (λ (E list)
    (rec-List list
      (the (List E) nil)
      (λ (x xs reversed-xs)
        (snoc E reversed-xs x)))))

(claim replicate
  (Pi ((E U))
    (-> Nat E
      (List E))))
(define replicate
  (λ (E n e)
    (iter-Nat n
      (the (List E) nil)
      (λ (es) (:: e es)))))

(claim ::-add1-length
  (Pi ((E U)
       (list (List E))
       (n Nat)
       (_ (= Nat (length E list) n))
       (e E))
    (= Nat (length E (:: e list)) (add1 n))))
(define ::-add1-length
  (λ (E list)
    (ind-List list
      (λ (l)
        (Pi ((n Nat)
             (_ (= Nat (length E l) n))
             (e E))
          (= Nat (length E (:: e l)) (add1 n))))
      (λ (n tail-has-length-n _e)
        (cong tail-has-length-n (+ 1)))
      (λ (_e _es almost n tail-has-length-n _e)
        (cong tail-has-length-n (+ 1))))))

(claim replicate-length-matches-argument
  (Pi ((n Nat)
       (E U)
       (e E))
    (= Nat (length E (replicate E n e)) n)))
(define replicate-length-matches-argument
  (λ (n E e)
    (ind-Nat n
      (λ (k)
        (= Nat (length E (replicate E k e)) k))
      (same zero)
      (λ (n-1 almost)
        (::-add1-length
          E
          (replicate E n-1 e)
          n-1
          almost
          e)))))

(claim LessThanEqAll
  (-> Nat (List Nat) U))
(define LessThanEqAll
  (λ (lower uppers)
    (rec-List uppers
      Trivial
      (λ (e _es almost)
        (Pair (LessThanEq lower e)
          almost)))))

(claim <=all?
  (Pi ((n Nat)
       (others (List Nat)))
    (Dec (LessThanEqAll n others))))
(define <=all?
  (λ (n list)
    (ind-List list
      (λ (xs)
        (Dec (LessThanEqAll n xs)))
      ; if the list is empty, n is trivially <= than all
      (left sole)
      (λ (e rest n<=rest?)
        (ind-Either n<=rest?
          (λ (_)
            (Dec (LessThanEqAll n (:: e rest))))
          (λ (n<=rest)
            ; if n <= rest, we check to see if it's <= to e
            (ind-Either (<=? n e)
              (λ (_)
                (Dec (LessThanEqAll n (:: e rest))))
              (λ (n<=e)
                (left (cons n<=e n<=rest)))
              (λ (n!<=e)
                (right (λ (n<=e::rest)
                         (n!<=e (car n<=e::rest)))))))
          (λ (n!<=rest)
            ; if n is not <= to the rest, it obviously isn't <= to e::rest
            (right (λ (n<=e::rest)
                     (n!<=rest (cdr n<=e::rest))))))))))

(claim Sorted
  (-> (List Nat) U))
(define Sorted
  (λ (list)
    (rec-List list
      Trivial
      (λ (e es almost)
        (Pair (LessThanEqAll e es) almost)))))

(claim unsorted-list
  (List Nat))
(define unsorted-list
  (:: 1 (:: 0 nil)))

(claim unsorted-list-is-not-sorted
  (-> (Sorted unsorted-list) Absurd))
(define unsorted-list-is-not-sorted
  (λ (unsorted-list-is-sorted)
    (ind-Either (car (car unsorted-list-is-sorted))
      (λ (_) Absurd)
      (λ (one<zero)
        (nothing<zero 1 one<zero))
      (λ (one=zero)
        (zero-not-add1 0 (symm one=zero))))))

(claim sorted-list
  (List Nat))
(define sorted-list
  (:: 0 (:: 2 (:: 2 (:: 3 nil)))))

(claim sorted-list-is-sorted
  (Sorted sorted-list))
(define sorted-list-is-sorted
  (cons
    (cons ; 0 <=all [2, 2, 3]
      (left (cons 1
              (same 2)))
      (cons
        (left (cons 1
                (same 2)))
        (cons
          (left (cons 2
                  (same 3)))
          sole)))
    (cons
      (cons ; 2 <=all [2, 3]
        (right (same 2))
        (cons
          (left (cons 0 (same 3)))
          sole))
      (cons ; 2 <=all [3]
        (cons
          (left (cons 0 (same 3)))
          sole)
        (cons ; 3 <=all []
          sole
          sole)))))

(claim sorted?
  (Pi ((list (List Nat)))
    (Dec (Sorted list))))
(define sorted?
  (λ (list)
    (ind-List list
      (λ (list)
        (Dec (Sorted list)))
      (left sole)
      (λ (e rest rest-sorted?)
        (ind-Either rest-sorted?
          (λ (_)
            (Dec (Sorted (:: e rest))))
          (λ (rest-sorted)
            (ind-Either (<=all? e rest)
              (λ (_)
                (Dec (Sorted (:: e rest))))
              (λ (e<=rest)
                (left (cons e<=rest rest-sorted)))
              (λ (e!<=rest)
                (right (λ (e::rest-sorted)
                         (e!<=rest (car e::rest-sorted)))))))
          (λ (rest-unsorted)
            (right (λ (e::rest-sorted)
                     (rest-unsorted (cdr e::rest-sorted))))))))))

(check-same (Dec (Sorted sorted-list))
  (sorted? sorted-list)
  (left sorted-list-is-sorted))