ind-List.rkt

ind-List.rkt

#lang pie

;; Exercises on ind-Nat from Chapter 10 of The Little Typer


;; Prelude

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

(claim length
  (Π ((E U))
     (-> (List E) Nat)))
(define length
  (lambda (E es)
    (rec-List es
      0
      (lambda (e es length/es)
        (add1 length/es)))))

(claim append
  (Π ([E U])
     (-> (List E) (List E) (List E))))
(define append
  (lambda (E es end)
    (ind-List es
      (lambda (es) (List E))
      end
      (lambda (e es append/es)
        (:: e append/es)))))

(claim if0
  (Π ((X U))
     (-> Nat X X X)))

(define if0
  (lambda (X)
    (lambda (test then else)
      (which-Nat test
        else
        (lambda (_) then)))))

(claim filter-List
  (Π ((E U))
     (-> (-> E Nat) (List E) (List E))))

(define filter-List
  (lambda (E)
    (lambda (pred es)
      (rec-List es
        (the (List E) nil)
        (lambda (e _ h)
          (if0 (List E) (pred e)
            (:: e h)
            h))))))

;; End Prelude


;; Exercise 10.1
;;
;; Define a function called list-length-append-dist that states and proves that
;; if you append two lists, l1 and l2, and then the length of the result is
;; equal to the sum of the lengths of l1 and l2.

(claim list-length-append-dist
  (Π ([E U]
      [l1 (List E)]
      [l2 (List E)])
     (= Nat
        (length E (append E l1 l2))
        (+ (length E l1) (length E l2)))))

(define list-length-append-dist
  (lambda (E l1 l2)
    (ind-List l1
      (lambda (es) (= Nat
                      (length E (append E es l2))
                      (+ (length E es) (length E l2))))
      (same (length E l2))
      (lambda (e es h=)
        (cong h= (the (-> Nat Nat)
                   (lambda (len) (add1 len))))))))


;; Exercise 10.2
;;
;; In the following exercises we'll use the function called <= that takes two
;; Nat arguments a, b and evaluates to a type representing the proposition
;; that a is less than or equal to b.

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

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

;; Exercise 10.2.1
;;
;; Using <=, state and prove that 1 is less than or equal to 2.

(claim 1<=2
  (<= 1 2))

(define 1<=2
  (cons 1 (same 2)))

;; Exercise 10.2.2
;;
;; Define a funciton called <=-simplify to state and prove that for all
;; Nats a, b, n we have that n+a <= b implies a <= b
;;
;; NB: You may need to use plusAssociative that was proved in Exercise 8.3.

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

(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 <=-simplify
  (Π ([a Nat]
      [b Nat]
      [n Nat])
     (-> (<= (+ n a) b) (<= a b))))

(define <=-simplify
  (lambda (a b n)
    (ind-Nat n
      (lambda (k) (-> (<= (+ k a) b) (<= a b)))
      (lambda (p) p)
      (lambda (n-1 h)
        (lambda (p)
          ;; h : [∃ k, k+(n-1+a)=b] -> [∃ k, k+a=b]
          ;; p : ∃ k, k+(1+(n-1+a))=b
          ;;       to (1+k)+(n-1+a)=b

          ;; (cons (add1 (car p)) (... (cdr p) ...))
          (h (cons (add1 (car p))
                   (replace (nSm=Snm (car p) (+ n-1 a))
                     (lambda (from/to) (= Nat from/to b))
                     (cdr p)))))))))

;; Exercise 10.2.3
;;
;; Define a function called <=-trans that states and proves that <= is
;; transitive.
(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))))))

(claim <=-trans
  (Π ([a Nat]
      [b Nat]
      [c Nat])
     (-> (<= a b)
         (<= b c)
       (<= a c))))

(define <=-trans
  (lambda (a b c)
    (lambda (p q)
      ;; p : ∃ k₀, k₀+a=b
      ;; q : ∃ k₁, k₁+b=c
      ;;        or k₁+(k₀+a)=c (1)
      ;;        or (k₁+k₀)+a=c (2)
      ;; —————————————————————
      ;; ∃ k, k+a=c

      (cons (+ (car q) (car p))
            (replace (plusAssociative (car p) a (car q))      ; (2)
              (lambda (from/to) (= Nat from/to c))
              (replace (symm (cdr p))                         ; (1)
                (lambda (b/k₀+a) (= Nat (+ (car q) b/k₀+a) c))
                (cdr q)))))))

;; Exercise 10.3
;;
;; Define a function called length-filter-List that states and proves that
;; filtering a list (in the sense of filter-List from Exercise 5.3) evaluates
;; to a a list no longer than the original list.

(claim +1<=+1
  (Π ((a Nat)
      (b Nat))
     (-> (<= a b)
         (<= (add1 a) (add1 b)))))

(define +1<=+1
  (lambda (a b p)
    (cons (car p)
          (replace (symm (nSm=Snm (car p) a))
            (lambda (from/to) (= Nat from/to (add1 b)))
            (cong (cdr p) (+ 1))))))

(claim length-filter-List
  (Π ([E U]
      [l (List E)]
      [p (-> E Nat)])
     (<= (length E (filter-List E p l))
         (length E l))))

(claim lemma1
  (Π ((E U)
      (n Nat)
      (e E)
      (es (List E))
      (fes (List E)))
     (-> (<= (length E fes)
             (length E es))
         (<= (length E (if0 (List E) n (:: e fes) fes))
             (length E (:: e es))))))

(define lemma1
  (lambda (E n e es fes h)
    (ind-Nat n
      (lambda (k) (<= (length E (if0 (List E) k (:: e fes) fes))
                      (length E (:: e es))))
      ;; a<=b -> a<=1+b
      (cons (add1 (car h))
            (cong (cdr h) (+ 1)))
      (lambda (n-1 g)
        (+1<=+1 (length E fes) (length E es) h)))))

(define length-filter-List
  (lambda (E l p)
    (ind-List l
      (lambda (es) (<= (length E (filter-List E p es))
                       (length E es)))
      (cons 0 (same 0))
      (lambda (e es h)
        ;; h : ∃ k, k+(length (filter p es))=(length es)
        ;; ———————————————————————————————————————————
        ;; ∃ k, k+(length (filter e::es))=(length e::es)

        (lemma1 E (p e) e es (filter-List E p es) h)))))