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.

Exercise 0:

• Define not. In type theory negation is defined in terms of False.

Exercise 1:

• Prove the negation of the excluded middle.

Exercise 2:

• Declare iff (the constructor being called iff_intro).
• Define iff1 of the given type

Exercise 3:

• Declare xor: two constructors, both have two arguments
• Prove the following lemmas

Exercise 4:

• Declare exists2
• Prove a lemma ex1 -> ex2 T

Exercise 5:

• Write the induction principle for lists

Exercise 6:

• remeber => /view to prove the following lemma
• the two relevant views are prime_gt1 and dvdn_leq
• Note: => /view combines well with -> (lesson 3)
• Hint: the proof can be a one liner by move=> ....
• Recall: the notation "_ < _ <= _" hides a conjunction

Exercise 7:

• Define the indexed data type of Cherry tree: + the index is a bool and must be truee iff the tree is completely flourished + leaves can be either Flower or Bud + the third constructor is called Node and has two sub trees