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:

- We define binary trees in the following way:

- Define a function
`eq_bintree` such that the lemma `eq_bintreeP` holds,
and prove it.

- We define the depth of a tree as a function of type
`bintree -> nat` as follows:

- We define balanced trees as the following predicate:

- prove that balanced trees of equal depth are in fact equal:

###
Exercise 2:

Let \(a \ge 0\) and \(n \ge 1\) be natural numbers.

- Show that \[a ^ n − 1 = (a - 1) \sum_{i = 0}^{n-1} a^i.\]
- Hint
`Search _ sum in MC`.
- Hint do as many
`have` as needed.

Let \(a , n \ge 2\) be natural numbers.

- Show that if \(a ^ n − 1\) is prime, then \(a = 2\) and \(n\) is prime.
Complete the following proof script

- We write \(M_n = 2 ^ n − 1\) the \(n^{\textrm{th}}\) Mersenne number.
Show that \(M_{100}\) is not prime.
WARNING: do not substitute `n = 100` in an expression where you have `2 ^ n`,
otherwise the computation will take forever

and possibly crash your jscoq
(in which case you will need to Reset worker

or reload the page), hence
you must use the previous lemma.

When you are done, click the Download link at the top of the page
and send us your homework by email: Assia.Mahboubi@inria.fr