Chapter9.md

Chapter 9 Exercises

Exercise 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, using replace, because this can also be done with cong, but we are trying to practice chapter 9's replace.

(claim same-cons
  (Pi ((t U) (x t) (as (List t)) (bs (List t)))
    (-> (= (List t) as bs)
        (= (List t) (:: x as) (:: x bs)))))

Answer

Exercise 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 ((t U) (e1 t) (e2 t) (l1 (List t)) (l2 (List t)))
    (-> (= (List t) l1 l2) (= t e1 e2)
        (= (List t) (:: e1 l1) (:: e2 l2)))))

Answer

Exercise 3

Define a function called plus-comm that states and proves that + is commutative

(claim plus-comm
 (Pi ((n Nat) (m Nat))
   (= Nat (+ n m) (+ m n))))

Bonus: Write the solution using the trans elimiator instead of the replace eliminator.

Answer