chapter-15-Absurd.rkt

chapter-15-Absurd.rkt

#lang pie

;; Exercises on Absurd from Chapter 15 of The Little Typer

(claim +
  (-> Nat Nat
    Nat))

(define +
  (λ (a b)
    (rec-Nat a
      b
      (λ (_ b+a-k)
        (add1 b+a-k)))))

(claim double
  (-> Nat
      Nat))

(define double
  (λ (n)
    (rec-Nat n
      0
      (λ (_ n+n-2)
        (+ 2 n+n-2)))))

(claim Even
  (-> Nat
      U))

(define Even
  (λ (n)
    (Σ ([half Nat])
       (= Nat n (double half)))))

(claim Odd
  (-> Nat
      U))

(define Odd
  (λ (n)
    (Σ ([haf Nat])
       (= Nat n (add1 (double haf))))))

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

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

;; The following is not required for the statement of exercises
;; but will be required in some solutions.

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

(define =consequence
  (λ (n j)
    (which-Nat n
      (which-Nat j
        Trivial
        (λ (j-1)
          Absurd))
      (λ (n-1)
        (which-Nat j
          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 =consequence-n-1)
        (same n-1)))))

(claim use-Nat=
  (Π ([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))))

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

(define add1-not-zero
  (lambda (n p)
    (zero-not-add1 n (symm p))))

;;; Auxilliary

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

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

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

(define nSm=Snm
  (lambda (n m)
    (symm (Snm=nSm n m))))

;; Exercise 15.1
;;
;; State and prove that 3 is not less than 1.

(claim sub1=
  (Π ((n Nat)
      (m Nat))
     (-> (= Nat (add1 n) (add1 m))
         (= Nat n m))))

(define sub1=
  (lambda (n m p)
    (use-Nat= (add1 n) (add1 m) p)))

(claim not-3<=1
  (-> (<= 3 1)
      Absurd))

(claim not-3<=1-aux
  (Π ((k Nat))
     (-> (= Nat (+ k 3) 1)
         Absurd)))

(define not-3<=1-aux
  (lambda (k p)
    ;; p : (= Nat (+ k 3)        1)
    ;;     (= Nat 1        (+ k 3))  [symm]
    ;;     (= Nat 1 (add1 (+ k 2)))  [nSm=Snm]
    ;;     (= Nat 0 (+ k 2))         [sub1=]
    ;;     (= Nat 0 (add1 (+ k 1)))  [nSm=Snm]
    ;;     ...                       [zero-not-add1]
    (zero-not-add1 (+ k 1)
     (replace (nSm=Snm k 1)
       (lambda (from/to) (= Nat 0 from/to))
       (sub1= 0 (+ k 2)
              (replace (nSm=Snm k 2)
                (lambda (from/to) (= Nat 1 from/to))
                (symm p)))))))

(define not-3<=1
  (lambda (3<=1)
    (not-3<=1-aux (car 3<=1) (cdr 3<=1))))

;; Exercise 15.2
;;
;; State and prove that any natural number is not equal to its successor.

(claim n<>Sn
  (Π ([n Nat])
     (-> (= Nat n (add1 n))
         Absurd)))

(define n<>Sn
  (lambda (n)
    (ind-Nat n
      (lambda (k)
        (-> (= Nat k (add1 k)) Absurd))
      (lambda (p) (zero-not-add1 0 p))
      (lambda (n-1 h)
        (lambda (p)
          (h (sub1= n-1 (add1 n-1) p)))))))

;; Exercise 15.3
;;
;; State and prove that for every Nat n, the successor of n is not less
;; than or equal to n.

(claim Sn-not<=-n
  (Π ([n Nat])
     (-> (<= (add1 n) n)
         Absurd)))

(define Sn-not<=-n
  (lambda (n)
    (ind-Nat n
      ;; mot
      (lambda (k)
        (-> (<= (add1 k) k)
            Absurd))
      ;; base
      (lambda (p)
        (zero-not-add1 (+ (car p) 0)
                       (replace (nSm=Snm (car p) 0)
                         (lambda (from/to) (= Nat 0 from/to))
                         (symm (cdr p)))))
      ;; step
      (lambda (n-1 h)
        (lambda (p)
          (h (cons (car p)
                   (sub1=
                    (+ (car p) (add1 n-1))
                    n-1
                    (replace (nSm=Snm (car p) (add1 n-1))
                      (lambda (from/to) (= Nat from/to (add1 n-1)))
                      (cdr p))))))))))

;; Exercise 15.4
;;
;; State and prove that 1 is not Even.

(claim one-not-Even-aux
  (Π ((n Nat))
     (-> (= Nat 1 (double n))
         Absurd)))

(define one-not-Even-aux
  (lambda (n)
    (ind-Nat n
      (lambda (k)
        (-> (= Nat 1 (double k))
            Absurd))
      (lambda (p) (zero-not-add1 0 (symm p)))
      (lambda (n-1 h)
        (lambda (p)
          (zero-not-add1
           (double n-1)
           (sub1= 0 (add1 (double n-1)) p)))))))

(claim one-not-Even
  (-> (Even 1)
      Absurd))

(define one-not-Even
  (lambda (e1)
    (one-not-Even-aux (car e1) (cdr e1))))