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