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