equality-Nat.rkt

equality-Nat.rkt

#lang pie

;; Exercises on Nat equality from Chapter 8 and 9 of The Little Typer

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (n m)
    (rec-Nat n
      m
      (λ (_ +/n-1)
        (add1 +/n-1)))))

;; Exercise 8.1
;; Define a function called zero+n=n that states and proves that
;; 0+n = n for all Nat n.

(claim zero+n=n
  (Pi ((n Nat))
      (= Nat (+ 0 n) n)))

(define zero+n=n
  (lambda (n)
    (same n)))

;; Exercise 8.2
;;
;; Define a function called a=b->a+n=b+n that states and proves that
;; a = b implies a+n = b+n for all Nats a, b, n.

(claim a=b->a+n=b+n
  (Pi ((a Nat)
       (b Nat)
       (n Nat))
      (-> (= Nat a b)
          (= Nat (+ a n) (+ b n)))))

;; Using cong
#;
(define a=b->a+n=b+n
  (lambda (a b n h)
    (cong h (the (-> Nat Nat)
              (lambda (m)
                (+ m n))))))

;; Using replace
(define a=b->a+n=b+n
  (lambda (a b n a=b)
    (replace a=b
      (lambda (from/to) (= Nat (+ a n) (+ from/to n)))
      (same (+ a n)))))

;; Exercise 8.3
;;
;; Define a function called plusAssociative that states and proves that
;; + is associative.

(claim plusAssociative
  (Π ([n Nat]
      [m Nat]
      [k Nat])
     (= Nat (+ k (+ n m)) (+ (+ k n) m))))

(define plusAssociative
  (lambda (n m k)
    (ind-Nat k
      (lambda (k) (= Nat (+ k (+ n m)) (+ (+ k n) m)))
      (same (+ n m))
      (lambda (k-1 plusAssociative/k-1)
        (cong plusAssociative/k-1 (+ 1))))))

;; Exercise 9.1
;;
;; Define a function called same-cons that states and proves that
;; if you cons the same value to the front of two equal Lists then
;; the resulting Lists are also equal.

(claim same-cons
  (Π ([E U]
      [l1 (List E)]
      [l2 (List E)]
      [e E])
     (-> (= (List E) l1 l2)
         (= (List E) (:: e l1) (:: e l2)))))

;; Using cong
#;
(define same-cons
  (lambda (E l1 l2 e h)
    (cong h (the (-> (List E) (List E))
              (lambda (xs) (:: e xs))))))

;; Using replace
(define same-cons
  (lambda (E l1 l2 e l1=l2)
    (replace l1=l2
      (lambda (from/to) (= (List E) (:: e l1) (:: e from/to)))
      (same (:: e l1)))))

;; Exercise 9.2
;;
;; Define a function called same-lists that states and proves that
;; if two values, e1 and e2, are equal and two lists, l1 and l2 are
;; equal then the two lists, (:: e1 l1) and (:: e2 l2) are also equal.

(claim same-lists
  (Pi ((E U)
       (l1 (List E))
       (l2 (List E))
       (e1 E)
       (e2 E))
      (-> (= E e1 e2)
          (= (List E) l1 l2)
        (= (List E) (:: e1 l1) (:: e2 l2)))))

;; Using same-cons
#;
(define same-lists
  (lambda (E l1 l2 e1 e2 h1 h2)
    (replace h1
      (lambda (e) (= (List E) (:: e1 l1) (:: e l2)))
      (same-cons E l1 l2 e1 h2))))

;; Using replace twice
(define same-lists
  (lambda (E l1 l2 e1 e2 e1=e2 l1=l2)
    (replace e1=e2
      (lambda (from/to) (= (List E) (:: e1 l1) (:: from/to l2)))
      (replace l1=l2
        (lambda (from/to) (= (List E) (:: e1 l1) (:: e1 from/to)))
        (same (:: e1 l1))))))

;; Exercise 9.3 (was previously called Exercise 8.4)
;;
;; Define a function called plusCommutative that states and proves that
;; + is commutative
;;
;; Bonus: Write the solution using the trans elimiator instead of
;; the replace elimiator.
;; https://docs.racket-lang.org/pie/index.html#%28def._%28%28lib._pie%2Fmain..rkt%29._trans%29%29

(claim m=m+0
  (Pi ((m Nat))
      (= Nat m (+ m 0))))

(define m=m+0
  (lambda (m)
    (ind-Nat m
      (lambda (k) (= Nat k (+ k 0)))
      (same 0)
      (lambda (n-1 n-1=n-1+0)
        (cong n-1=n-1+0 (+ 1))))))

(claim Snm=nSm
  (Pi ((n Nat)
       (m Nat))
      (= Nat (add1 (+ m n)) (+ m (add1 n)))))

(define Snm=nSm
  (lambda (n m)
    (ind-Nat m
      (lambda (k) (= Nat (add1 (+ k n)) (+ k (add1 n))))
      (same (add1 n))
      (lambda (m-1 h)
        (cong h (+ 1))))))

(claim plusCommutative
  (Π ([n Nat]
      [m Nat])
     (= Nat (+ n m) (+ m n))))

;; Using replace
#;
(define plusCommutative
  (lambda (n m)
    (ind-Nat n
      (lambda (k) (= Nat (+ k m) (+ m k)))
      (m=m+0 m)
      (lambda (n-1 n-1+m=m+n-1)
        (replace (Snm=nSm n-1 m)
          (lambda (from/to) (= Nat (add1 (+ n-1 m)) from/to))
          (cong n-1+m=m+n-1 (+ 1)))))))

;; Using trans
(define plusCommutative
  (lambda (n m)
    (ind-Nat n
      (lambda (k) (= Nat (+ k m) (+ m k)))
      (m=m+0 m)
      (lambda (n-1 n-1+m=m+n-1)
        (trans (cong n-1+m=m+n-1 (+ 1)) (Snm=nSm n-1 m))))))