From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Implicit Type p q r : bool.
Implicit Type m n a b c : nat.

(** *** Exercise 1:

Prove that the equation #$$ 8y = 6x + 1 $$# has no solution.

- Hint 1: take the modulo 2 of the equation.
- Hint 2: [Search _ modn addn] and [Search _ modn muln]
#<br/><div># *)
Lemma ex1 x y : 8 * y != 6 * x + 1.
Proof.
Admitted.

(** #</div>#
*** Exercise 2:

The ultimate Goal of this exercise is to find the solutions of the equation
#$$ 2^n = a^2 + b^2,$$# where n is fixed and a and b unkwown.

We hence study the following predicate:
#<div># *)
Definition sol n a b := [&& a > 0, b > 0 & 2 ^ n == a ^ 2 + b ^ 2].
(** #</div>#
- First prove that there are no solutions when n is 0.

  - Hint: do enough cases on a and b.
#<div># *)
Lemma sol0 a b : ~~ sol 0 a b.
Admitted.
(** #</div>#
- Now prove the only solution when n is 1.

  - Hint: do enough cases on a and b.
#<div># *)
Lemma sol1 a b : sol 1 a b = (a == 1) && (b == 1).
Admitted.
(** #</div>#
- Now prove a little lemma that will guarantee that a and b are even.

  - Hint 1: first prove [(x * 2 + y) ^ 2 = y ^ 2 %[mod 4]].
  - Hint 2: [About divn_eq] and [Search _ modn odd]
#<div># *)
Lemma mod4Dsqr_even a b : (a ^ 2 + b ^ 2) %% 4 = 0 -> (~~ odd a) && (~~ odd b).
Proof.
Admitted.
(** #</div>#
- Deduce that if n is greater than 2 and a and b are solutions, then they are even.
#<div># *)
Lemma sol_are_even n a b : n > 1 -> sol n a b -> (~~ odd a) && (~~ odd b).
Proof.
Admitted.
(** #</div>#
- Prove that the solutions for n are the halves of the solutions for n + 2.

  - Hint: [Search _ odd double] and [Search _ "eq" "mul"].

#<div># *)
Lemma solSS n a b : sol n.+2 a b -> sol n a./2 b./2.
Proof.
Admitted.
(** #</div>#
- Prove there are no solutions for n even

  - Hint: Use [sol0] and [solSS].
#<div># *)
Lemma sol_even a b n : ~~ sol (2 * n) a b.
Proof.
Admitted.
(** #</div>#
- Certify the only solution when n is odd.

  - Hint 1: Use [sol1], [solSS] and [sol_are_even].
  - Hint 2: Really sketch it on paper first!
#<div># *)
Lemma sol_odd a b n : sol (2 * n + 1) a b = (a == 2 ^ n) && (b == 2 ^ n).
Proof.
Admitted.
(** #</div>#
*** Exercise 3:
Certify the solutions of this problem.

- Hint: Do not hesitate to take advantage of Coq's capabilities
  for brute force case analysis
#<div># *)
Lemma ex3 n : (n + 4 %| 3 * n + 32) = (n \in [:: 0; 1; 6; 16]).
Proof.
Admitted.
(** #</div>#
*** Exercise 4:

Certify the result of the euclidean division of
#$$a b^n - 1\quad\textrm{  by  }\quad b ^ {n+1}$$#

#<div># *)
Lemma ex4 a b n : a > 0 -> b > 0 -> n > 0 ->
   edivn (a * b ^ n - 1) (b ^ n.+1) =
   ((a - 1) %/ b, ((a - 1) %% b) * b ^ n + b ^ n - 1).
Proof.
Admitted.
(** #</div>#
*** Exercise 5:

Prove that the natural number interval #$$[n!+2\ ,\ n!+n]$$#
contains no prime number.

- Hint: Use [Search _ prime dvdn], [Search _ factorial], ...

#<div># *)
Lemma ex5 n m : n`! + 2 <= m <= n`! + n -> ~~ prime m.
Proof.
Admitted.
(** #</div># *)