Use ALT-(up-arrow) and ALT-(down-arrow) to process this document inside your browser, line-by-line.
Use ALT-(right-arrow) to go to the cursor.
You can
save your edits
inside your browser and
load them back.
Finally, you can
download
your working copy of the file, e.g., for sending it to teachers.

###
Exercise 1:

- Define a function double that takes a natural
number to its double.
- you can use the operations on nat that we defined in class

###
Exercise 2:

- Define a function that takes a natural number and tests
if it is zero. In that case the value of the function is 1,
otherwise it is the double of the given number.
- The skeleton of the function is given, fill in the blanks.

###
Exercise 3:

Define boolean negation. We did peek at it during the lesson,
now try to write it yourself.

###
Exercise 4:

- write the Fibonacci function (growth of a rabbit population).
$$ \phi(n) = \begin{array}{|c}1~\mathrm{if}~n = 0 \\ 1~\mathrm{if}~n = 1\\ \phi(n-1) + \phi(n-2)~\mathrm{otherwise}\end{array} $$

###
Exercise 5:

- Define the option container with constructors None and Some
- Define the
projection

default

###
Exercise 6:

Use the

`iter` function below to define:

- addition over natural numbers.
- multiplication over natural unmbers.

###
Exercise 7:

- prove the following statement by case split

###
Exercise 8:

- look up what
`==>` is and prove the Peirce law

###
Exercise 9:

- what is
`(+)` ?
- Hint:
`->` in the goal stands for implication, use move to name the
assumption
- Hint: use Search to dind useful lemmas and use rewrite to use them