To play this document inside your browser use ALT-N and ALT-P.
If you get stack overflow
errors, try to use
Google Chrome
or Chromium
with the command line option --js-flags="--harmony-tailcalls".
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.
Exercise 1:
- use no lemma to prove the following statement
Exercise 2:
- look up what ==> is check if there are relevant views
- prove that as you like
Exercise 3:
- look for lemmas supporting contrapositive reasoning
Exercise 4:
- what is (+) ?
- find the right view to prove this statement
- now find another proof without the view
Exercise 5:
- it helps to find out what is behind ./2 and .*2 in order to Search
- any proof would do, but there is one not using implyP
Exercise 6:
- prove that using case:
- then prove that without using case:
Exercise 7:
- look up the definition of iter
- prove this satement by induction
Exercise 8:
- look up the definition of iter (note there is an accumulator varying
during recursion)
- prove the following statement by induction