inequality.rkt

inequality.rkt

#lang pie

;; Prelude

(claim +
  (-> Nat Nat Nat))
(define +
  (lambda (n m)
    (rec-Nat n
      m
      (lambda (n-1 +/n-1)
        (add1 +/n-1)))))

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

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

(define <=
  (λ (a b)
    (Σ ([k Nat])
       (= Nat (+ k a) b))))

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

(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))))))

;; End Prelude

;; Credit: Cesar
(claim remove-add1
  (-> Nat Nat))

(define remove-add1
  (lambda (n)
    (which-Nat n
      0
      (lambda (n-1) n-1))))

;; a
(claim n+0=n
  (Π ((n Nat))
     (= Nat (+ n 0) n)))

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

;; 1
(claim n+m=0->n=0
  (Π ((n Nat)
      (m Nat))
     (-> (= Nat (+ n m) 0)
         (= Nat n 0))))

(define n+m=0->n=0
  (lambda (n m)
    (ind-Nat m
      (lambda (k) (-> (= Nat (+ n k) 0) (= Nat n 0)))
      (lambda (n+0=0) (replace (n+0=n n)
                        (lambda (from/to) (= Nat from/to 0))
                        n+0=0))
      (lambda (m-1 h)
        (lambda (p)
          ;; h : (→ (= Nat (+ n       m-1)  0) (= Nat n 0))
          ;; p :    (= Nat (+ n (add1 m-1)) 0)
          (h (cong (replace (nSm=Snm n m-1)
                     (lambda (from/to) (= Nat from/to 0))
                     p)
                   remove-add1)))))))


;; b
(claim n+0=0->n=0
  (Π ((n Nat))
     (-> (= Nat (+ n 0) 0)
         (= Nat n 0))))

(define n+0=0->n=0
  (lambda (n)
    (ind-Nat n
      (lambda (k) (-> (= Nat (+ k 0) 0)
                      (= Nat k 0)))
      (lambda (a) a)
      (lambda (n-1 h)
        (lambda (p)
          ;; h : (→ (= Nat (+ n-1 0) 0) (= Nat n-1 0))
          ;; p : (= Nat (add1 (+ n-1 0)) 0)
          ;; ————————————–————————————–
          ;; (= Nat (add1 n-1) 0)
          (replace (n+0=n n-1)
            (lambda (from/to) (= Nat (add1 from/to) 0))
            p))))))

;; c
(claim 1+n=1->n=0
  (Π ((n Nat))
     (-> (= Nat (add1 n) 1)
         (= Nat n 0))))

(define 1+n=1->n=0
  (lambda (n)
    (ind-Nat n
      (lambda (k) (-> (= Nat (add1 k) 1)
                      (= Nat k 0)))
      (lambda (p) (same 0))
      (lambda (n-1 h)
        (lambda (p)
          ;; h : (→ (= Nat (add1 n-1) 1) (= Nat n-1 0))
          ;; p : (= Nat (add1 (add1 n-1)) 1)
          (cong p remove-add1))))))

;; d
(claim 1+=1+
  (Π ((n Nat)
      (m Nat))
     (-> (= Nat (add1 n) (add1 m))
         (= Nat n m))))

(define 1+=1+
  (lambda (n m)
    (ind-Nat m
      (lambda (k) (-> (= Nat (add1 n) (add1 k))
                      (= Nat n k)))
      (lambda (p) (1+n=1->n=0 n p))
      (lambda (m-1 h)
        (lambda (p)
          (cong p remove-add1))))))

;; 2
(claim n+m=m->n=0
  (Π ((n Nat)
      (m Nat))
     (-> (= Nat (+ n m) m)
         (= Nat n 0))))

(define n+m=m->n=0
  (lambda (n m)
    (ind-Nat m
      (lambda (k) (-> (= Nat (+ n k) k) (= Nat n 0)))
      (lambda (n+0=0)
        (n+0=0->n=0 n n+0=0))
      (lambda (n-1 h)
        (lambda (h=)
          ;; h : (→ (= Nat       (+ n n-1)              n-1) (= Nat n 0))
          ;; h= :   (= Nat       (+ n (add1 n-1)) (add1 n-1))
          ;;     to (= Nat (add1 (+ n n-1))       (add1 n-1)) – (1)
          (h
           (1+=1+
            (+ n n-1) n-1
            (replace (nSm=Snm n n-1)  ; (1)
              (lambda (nSm/Snm) (= Nat nSm/Snm (add1 n-1)))
              h=))))))))

;; 3
(claim 0+n=m->n=m
  (Π ((k Nat)
      (n Nat)
      (m Nat))
     (-> (= Nat (+ k n) m) (= Nat k 0)
       (= Nat n m))))

(define 0+n=m->n=m
  (lambda (k n m k+n=m k=0)
    (replace k=0
      (lambda (k/0) (= Nat (+ k/0 n) m))
      k+n=m)))

(claim a=b
  (Π ((a Nat)
      (b Nat))
     (-> (<= a b) (<= b a)
       (= Nat a b))))

(define a=b
  (lambda (a b)
    (lambda (p q)
      ;; p : ∃ k₀, k₀+a=b
      ;; q : ∃ k₁, k₁+b=a
      ;;        or k₀+(k₁+b)=b (1) – rewrite p with symm q
      ;;        or (k₀+k₁)+b=b (2) – plus associative

      ;; let k₂ = k₀+k₁
      ;; then
      ;; k₂+b=b -> k₂=0
      ;;           k₀+k₁=0 -> k₀=0
      ;;                      0+a=b -> a=b
      (0+n=m->n=m
       (car p) a b (cdr p)
       (n+m=0->n=0
        (car p) (car q)
        (n+m=m->n=0
         (+ (car p) (car q)) b
         (replace (plusAssociative (car q) b (car p))       ; (2)
           (lambda (from/to) (= Nat from/to b))
           (replace (symm (cdr q))                          ; (1)
             (lambda (a/k₁+b) (= Nat (+ (car p) a/k₁+b) b))
             (cdr p)))))))))