To play this document inside your browser use ALT-N and ALT-P.

You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.


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: do enough cases on a and b.

  • Now prove the only solution when n is 1.

    • Hint: do enough cases on a and b.

  • 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, ...