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