chapter-15.rkt

chapter-15.rkt

#lang pie

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

(define =consequence
  (lambda (n m)
    (which-Nat n
      (which-Nat m
        Trivial
        (lambda (_) Absurd))
      (lambda (n-1)
        (which-Nat m
          Absurd
          (lambda (m-1)
            (= Nat n-1 m-1)))))))

(claim =consequence-same
  (Π ((n Nat))
     (=consequence n n)))

(define =consequence-same
  (lambda (n)
    (ind-Nat n
      (lambda (k)
        (=consequence k k))
      sole
      (lambda (n-1 _)
        (same n-1)))))

(claim use-Nat
  (Π ((n Nat)
      (m Nat))
     (-> (= Nat n m)
         (=consequence n m))))

(define use-Nat
  (lambda (n m)
    (lambda (n=m)
      (replace n=m
        (lambda (from/to) (=consequence n from/to))
        (=consequence-same n)))))

;; Donut Absurdity

(claim donut-absurdity-claim U)
(define donut-absurdity-claim
  (-> (= Nat 0 6)
      (= Atom 'powdered 'glazed)))

(claim donut-absurdity/direct donut-absurdity-claim)

(define donut-absurdity/direct
  (lambda (0=6)
    (ind-= 0=6
      (lambda (x _)
        (= Atom
          'powdered
          (which-Nat x 'powdered (lambda (_) 'glazed))))
      (same 'powdered))))

(claim donut-absurdity donut-absurdity-claim)

(define donut-absurdity
  (lambda (0=6)
    (ind-Absurd (use-Nat 0 6 0=6)
      (= Atom 'powdered 'glazed))))

;;;

(claim front
  (Π ((E U)
      (n Nat))
     (-> (Vec E (add1 n))
         E)))

(define front
  (lambda (E n es)
    (ind-Vec (add1 n) es
      (lambda (k es)
        (which-Nat k
          Atom
          (lambda (_) E)))
      'impossible
      (lambda (_ e _ _) e))))


;; Principle of Excluded Middle

(claim pem-not-false
  (Π ((X U))
     (-> (-> (Either X
                     (-> X Absurd))
             Absurd)
         Absurd)))

(define pem-not-false
  (lambda (X)
    (lambda (pem-false)
      (pem-false (right (lambda (x)
                          (pem-false (left x))))))))