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 inside your browser and . Finally, you can 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:

• 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