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
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:
- First prove that there are no solutions when n is 0.
- Hint: Lookup ltnP, ltn_eqF, leq_add and Search _ "_gt0".
- Now prove the only solution when n is 1.
- 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
- Deduce that if n is greater than 2 and a and b are solutions, then they are even.
- Prove that the solutions for n are the halves of the solutions for n + 2.
- Hint: Search _ odd double and Search _ "eq" "mul".
- Prove there are no solutions for n even
- Hint: Use sol0 and solSS.
- 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!
Exercise 3:
Certify the solutions of this problem.
- Hint: Do not hesitate to take advantage of Coq's capabilities
for brute force case analysis
Exercise 4:
Certify the result of the euclidean division of
$$a b^n - 1\quad\textrm{ by }\quad b ^ {n+1}$$
Exercise 5:
Prove that the natural number interval $$[n!+2\ ,\ n!+n]$$
contains no prime number.
- Hint: Use Search _ prime dvdn, Search _ factorial, ...