Machine-Checked Mathematics

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

Lemma subX1_prime (a n : nat) : 2 <= a -> 2 <= n ->
  prime (a ^ n - 1) -> (a == 2) && prime n.
Proof.
move=> a_ge2 n_ge2 /primeP [_ mP].
have n_gt0 : S 0 <= n by rewrite (leq_trans _ n_ge2).
have a_gt0 : S 0 <= a by rewrite (leq_trans _ a_ge2).
have dvdam : a - 1 %| a ^ n - 1 by rewrite subX1_factor// dvdn_mulr.
have neq_m : a - 1 != a ^ n - 1.
  rewrite -(eqn_add2r 1) !subnK// ?expn_gt0 ?a_gt0//.
  by rewrite -{1}[a]expn1 ltn_eqF// ltn_exp2l//.
have a_eq2: a = 2.
  have := mP _ dvdam.
  by rewrite -(eqn_add2r 1) subnK// (negPf neq_m) orbF => /eqP.
move: mP; rewrite a_eq2 /= => mP.
apply/primeP; split => // d /dvdnP[k eq_n].
case d_neq1 : (d == 1) => //=.
have d_gt0 : d > 0.
   by move: n_gt0; rewrite eq_n !lt0n; apply: contra_neq => ->; rewrite muln0.
have k_gt0 : k > 0.
   by move: n_gt0; rewrite eq_n !lt0n; apply: contra_neq => ->; rewrite mul0n.
have d_gt1 : d > 1 by rewrite ltn_neqAle eq_sym d_neq1/=.
have dvddm : 2 ^ d - 1 %| 2 ^ n - 1.
  by rewrite eq_n mulnC expnM (subX1_factor (_ ^ _))// dvdn_mulr.
have := mP _ dvddm; rewrite gtn_eqF/=; last first.
  by rewrite ltn_subRL; have: 2 ^ 1 < 2 ^ d by rewrite ltn_exp2l.
by rewrite -(eqn_add2r 1) !subnK// ?expn_gt0// eqn_exp2l.
Qed.

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