To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.


Cheat sheet available at https://www-sop.inria.fr/teams/marelle/types18/cheatsheet.pdf


Exercise 1:

  • prove this satement by induction



Exercise 2:

  • look up the definition of iter (note there is an accumulator varying during recursion)
  • prove the following statement by induction



Exercise 3:

Prove the sum of the lists odds n of exercise 1 is n ^ 2.

You can prove the following lemmas in any order, some are way easier than others.

  • Recall from exercise 1.

  • We define a sum operation suml.

  • Any foldl addn can be rexpressed as a sum.

  • Not to break abstraction, prove suml_cons.

  • Show how to sum a add2list.

  • Show the size of a add2list.

  • Show how many elments odds have.

  • Show the final statment.


(hint)
For eq_suml_odds, use sqrnD



Exercise 4:

Prove the sum of the lists odds n is what you think.

You may want to have at least one itermediate lemma to prove oddsE


(hint)
this intermediate lemma would be:




Exercise 5:

Let us prove directly formula $$ \sum_{i=0}^{n-1} (2 i + 1) = n ^ 2 $$ from lesson 1, slightly modified.

Let us first define a custom sum operator:

  • First prove a very useful lemma about summation

  • Now prove the main result
Do NOT use eq_suml_odds above, it would take much more time