exercise2

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 2:

Exercise 3:

Exercise 4:

Exercise 5 :

Exercise 6 :

look up what ==>

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

Exercise 11

Exercise 12

Exercise 13

Exercise 14

*** We define functions that test if 3 natural numbers are in increasing (or decreasing) order