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
Try to prove the following theorems using no
lemma and minimizing the number of applications of
the tactic case
Exercise 1:
Exercise 7 :
Try to prove using the case tactic and alternatively
without using the case tactic
Exercise 8 :
Try to prove using the case tactic and alternatively
without using the case tactic
Exercise 9 :
- what is (+) ?
- prove this using move and rewrite
***
maxn defines the maximum of two numbers
***
We define the maxinum of three number as
folllow
***
Try to prove the following theorem
(you may use properties of maxn)
Exercise 10
***
We define functions that test if 3 natural numbers are
in increasing (or decreasing) order