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.
- 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.
(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