jsCoq – Use Coq in Your Browser

Worksheet on divisibility.

These are specific statements or questions, with their origin and comments both in French and English. Note that provided script prepsheet will replace lines from marker (*Begin solution for the teacher.*) to next marker (included) (*End solution for the teacher.*) by "Admitted.", and will remove lines from marker (*Begin other solution for the teacher.*) to next marker (included) (*End other solution for the teacher.*) That way, both teacher and student versions of the file are compiling, and teachers can verify the validity of the provided solution(s).

From Coq Require Import Lia List.
From Coq Require ZArith.BinInt ZArithRing Znumtheory.
From Teach Require DivPrelude Zmod_div Zprime.
Import ZArith.BinInt ZArithRing DivPrelude ListNotations.

Local Open Scope Z_scope.
(*fr Les premiers exercices proviennent d'une fiche d'exercice faite
   par M. Delabrouille, enseignant au lycée Blaise Pascal à Orsay *)
(*en The first exercises come from a wrksheet done by Mr Delabrouille, 
   teacher at Blaise Pascal's high school, Orsay, France. *)

(*fr Exercice 1 de la fiche d'exercice du lycée Blaise Pascal *)
(*en Exercise 1 from Blaise Pascal's high school worksheet *)

(*fr ** La divisibilité dans Z *)
Print Z.divide.
(*fr On dit qu'un entier y est divisible par un entier x s'il existe un entier
   z tel que y = z * x. Dans ce cas, note (x | y) pour "x divise y".

En Coq, cette relation s'appelle Z.divide et utilise la même notation. *)
Print Z.divide.
About "( x | y )".

(*fr À titre d'exemple, on peut prouver que 9 divise 99. *)
Lemma divide_echauffement : (9 | 99).
Admitted.

Search _.
(*fr Vous pouvez utiliser Coq comme une calculette : *)

Compute 17 / 5.
Compute 123 / 24.

(*fr À vous pour celui-ci : *)
Lemma divide_echauffement' : (17 | 493).
Proof.
Admitted.

(*fr On va maintenant prouver que la divisibilité est réflexive et transitive. *)
(*fr On pourra utiliser Z.mul_1_r ou Z.mul_1_l. *)
Check Z.mul_1_r.
Check Z.mul_1_l.

Lemma divide_refl (x : Z) : (x | x).
Proof.
Admitted.

(*fr Pour le lemme suivant, vous aurez sans doute besoin de l'associtivité et/ou
     de la commutativité de la multiplication : *)
Check Z.mul_assoc.
Check Z.mul_comm.

(*fr Vous devez aussi vous souvenir comment utiliser une propriété du type
   "il existe" : avec un [destruct] (ou bien un intro pattern). *)

Lemma divide_trans (x y z : Z) : (x | y) -> (y | z) -> (x | z).
Proof.
Admitted.

(*fr Toujours sur la divisibilité, on peut prouver que c'est une relation
     compatible avec l'addition.

Vous aurez besoin de factoriser en utilisant l'un des lemmes suivants : *)
Check Z.mul_add_distr_l.
Check Z.mul_add_distr_r.

Lemma divide_add_r (n m p : Z) : (n | m) -> (n | p) -> (n | m + p).
Proof.
Admitted.

(*fr ** Division euclidienne *)

(*fr La division euclidienne d'un entier (positif pour faire
    simple) a par un entier positif b est le couple
    (q, r) tel que :
    a = b * q + r et 0 <= r < b.

On appelle q le quotient de a par b (noté a / b en Coq) et r le reste de a par b (noté a mod b en Coq). *)
Compute (17 / 5).
Compute (17 mod 5).
Compute (5 * 3 + 2).

On va utiliser très souvent le lemme suivant :

En utilisant TODO, prouver le lemme suivant :

Lemma dixsept_mod3 : 17 mod 5 = 2.
Proof.
Admitted.

(*fr ** Division euclidienne et divisibilité *)

Lemma exercise01 (n p : Z) : n mod 7 = 3 -> p mod 7 = 1 -> (7 | 2 * n + p * p).
Proof.
Admitted.

(* End solution for the teacher. *)

(*fr Exercice 1 de la fiche d'exercice du lycée Blaise Pascal, preuve alternative *)
(*en Exercise 1 from Blaise Pascal's high school worksheet, alternative proof *)
Lemma exercise01_with_auto (n p : Z) : n mod 7 = 3 -> p mod 7 = 1 -> (7 | 2 * n + p * p).
Proof.
Admitted.

(* End solution for the teacher *)

(*fr Exercice 5 de la fiche d'exercice du lycée Blaise Pascal *)
(*en Exercise 5 from Blaise Pascal's high school worksheet *)
Lemma exercise02 : (17 | 35 ^ 228 + 84 ^ 501).
Proof.
Admitted.

(*fr Inspiré de l'exercice 5 de la fiche d'exercice du lycée Blaise Pascal,
   mais on augmente les valeurs des exposants afin d'empêcher Coq de calculer
   facilement la preuve *)
(*en Almost the same as exercise 5 from Blaise Pascal's high school worksheet,
   but we increased the values to prevent Coq from computing the result trivially *)
Lemma exercise03 : (17 | 35 ^ 22800 + 84 ^ 500001).
Proof.
Admitted.

Definition abcabc (a b c : Digit) : Z :=
  (Z_of_Digit a) * 100000 +
  (Z_of_Digit b) * 10000 +
  (Z_of_Digit c) * 1000 +
  (Z_of_Digit a) * 100 +
  (Z_of_Digit b) * 10 +
  (Z_of_Digit c).

(*fr Exercice 2.b page 143 du livre Mathématiques Hyperbole option Maths Expertes *)
(*en Exercise 2.b page 143 from Mathématiques Hyperbole option Maths Expertes *)
Lemma exercise04_with_auto (a b c : Digit) : (91 | abcabc a b c).
Proof.
Admitted.

(*fr Preuve alternative de l'exercice 2.b page 143 du livre Mathématiques Hyperbole option Maths Expertes *)
(*en Alternative proof to exercise 2.b page 143 from Mathématiques Hyperbole option Maths Expertes *)
Lemma exercise04 (a b c : Digit) : (91 | abcabc a b c).
Proof.
Admitted.

(*fr Exercice 63 page 154 du livre Mathématique Hyperbole option Maths Expertes *)
(*en Exercise 63 page 154 from  Mathématique Hyperbole option Maths Expertes *)
Lemma exercise05 : findall (fun x => ((78^115372 + 92^23238 + 106^35536) mod 7 = x)).
Proof.
Admitted.

(*fr Énoncé alternatif de l'exercice 63 page 154 du livre Mathématique Hyperbole option Maths Expertes
sans findall *)
(*en Alternative formalization of exercise 63 page 154 from Mathématique Hyperbole option Maths Expertes
without findall *)
Lemma exercise05_alt : (78 ^ 115372 + 92 ^ 23238 + 106 ^ 35536) mod 7 = 3.
Proof.
Admitted.

(*fr Lemme intermédiaire pour l'exercice 10 *)
(*en Intermediate lemma for exercise 10 *)
Lemma exercise06 (n : Digits) : (2 | (Z_of_Digits n)) <-> (2 | (Z_of_Digit (last_digit n))).
Proof.
Admitted.

(*fr Lemme intermédiaire pour l'exercice 8 *)
(*en Intermediate lemma for exercise 8 *)
Lemma exercise07 (n : Digits) : ((Z_of_Digits n) mod 3 = (digits_sum n) mod 3).
Proof.
Admitted.

(*fr Lemme pour l'exercice 10
   Indice: utiliser l'exercice 07 *)
(*en Lemma for exercice 10:
   Hint: use exercise 07 *)
Lemma exercise08 (n : Digits) : (3 | (Z_of_Digits n)) <-> (3 | digits_sum n).
Proof.
Admitted.

(*fr Lemme pour l'exercice 10 *)
(*en Lemma for exercise 10 *)
Lemma exercise09 (n : Z) : (6 | n) <-> (3 | n) /\ (2 | n).
Proof.
Admitted.

(*fr Exercice 119 page 161 du livre Mathématique Hyperbole option Maths Expertes *)
(*en Exercise 119 page 161 from Mathématique Hyperbole option Maths Expertes *)
Lemma exercise10 (n : Digits) :
  (6 | (Z_of_Digits n)) <-> (6 | (4 * ((digits_sum n) - (Z_of_Digit (last_digit n))) + (Z_of_Digit (last_digit n)))).
Proof.
Admitted.

(*fr Preuve alternative de l'exercice 119 page 161 du livre Mathématique Hyperbole option Maths Expertes,
   en raisonnant par équivalence *)
(*en Alternative proof to exercise 119 page 161 from Mathématique Hyperbole option Maths Expertes,
   by reasoning with equivalence *)

(* @TODO (DH) Le renommage a cassé la preuve, je ne sais pas pourquoi *)
Lemma exercise10_alt (n : Digits) :
  (6 | (Z_of_Digits n)) <-> (6 | (4 * ((digits_sum n) - (Z_of_Digit (last_digit n))) + (Z_of_Digit (last_digit n)))).
Proof.
Admitted.

(* End solution for the teacher *)

(*fr Exercice 117 page 160 du livre Mathématique Hyperbole option Maths Expertes *)
(*en Proof to exercise 117 page 160 from Mathématique Hyperbole option Maths Expertes *)
Lemma exercise11 (n k q : Z) (h0n : 0 <= n) (h0k : 0 <= k) (h0q : 0 <= q)
  (hk : n = k * k) (hq : n = q * q * q) : n mod 7 = 0 \/ n mod 7 = 1.
Proof.
Admitted.

(*fr Lemme pour l'exercice 13 *)
(*en Lemma for exercise 13 *)
Lemma exercise12 (x y p : Z) : prime p -> x * y = p -> (0 <= x) ->
    (x = p /\ y = 1) \/ (x = 1 /\ y = p).
Proof.
Admitted.

(*fr Exercice 121 page 161 du livre Mathématique Hyperbole option Maths Expertes
   Indice: utiliser l'exercice 12 *)
(*en Exercise 121 page 161 from Mathématique Hyperbole option Maths Expertes
   Hint: use exercise 12 *)

(* Expérience derive
Require Import Coq.derive.Derive.
Derive M SuchThat (let (x,y) := (fst M, snd M) in
                   (y ^ 2 = x ^ 2 - 13 /\ 0 <= y /\ 0 <= x /\ 13 <= x ^ 2)) As H.
unfold M.
remember (fst _) as x.
remember (snd _) as y.
split.
* assert (x = 7). rewrite Heqx. unfold fst.

Derive M SuchThat (let (x,y) := (fst M, snd M) in
                   (y ^ 2 = x ^ 2 - 13 /\ 0 <= y /\ 0 <= x /\ 13 <= x ^ 2)) As H.
Derive M SuchThat ((snd M) ^ 2 = (fst M) ^ 2 - 13 /\ 0 <= (snd M) /\ 0 <= (fst M) /\ 13 <= (fst M) ^ 2) As H.
 *)

Lemma exercise13 :
  findall (fun (M : Z * Z) =>
    let (x, y) := M in
    y ^ 2 = x ^ 2 - 13 /\ 0 <= y /\ 0 <= x /\ 13 <= x ^ 2
  ).
Proof.
Admitted.
 
(*fr Exercice 28 page 151 du livre Mathématique Hyperbole option Maths Expertes *)
(*en Exercise 28 page 151 from Mathématique Hyperbole option Maths Expertes *)
Lemma exercise14 (k : Z) (hk : 0 <= k) (x : Z) (hx : 0 <= x) :
  (x | 9 * k + 2) -> (x | 12 * k + 1) -> (x = 1) \/ (x = 5).
Proof.
Admitted.

(*fr Exercice 31 page 151 du livre Mathématique Hyperbole option Maths Expertes *)
(*en Exercise 31 page 151 from Mathématique Hyperbole option Maths Expertes *)
Lemma exercise15 : findall (fun n => (0 <= n) /\ (n | n + 8)).
Proof.
Admitted.