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

Exercise 9:

• the only tactics allowed are rewrite and by
• use Search to find the relevant lemmas (all are good but for ltn_neqAle) or browse the online doc
• proof sketch:

          m < n = ~~ (n <= m)
                = ~~ (n == m || n < m)
                = n != m && ~~ (n < m)
                = ...
  

Exercise 10:

• there is no need to prove reflect with iffP: here just use rewrite and apply
• check out the definitions and theory of leq and maxn
• proof sketch:

     n <= m = n - m == 0
            = m + n - m == m + 0
            = maxn m n == m