(** This file is part of the coq-teach library Copyright (C) Boldo, Clément, Hamelin, Mayero, Rousselin This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *) (** * 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. Import ZArith.BinInt ListNotations ZArithRing Znumtheory. From Teach Require Import DivPrelude Zmod_div Zprime. 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 *) Lemma exercise01 (n p : Z) : n mod 7 = 3 -> p mod 7 = 1 -> (7 | 2 * n + p * p). Proof. Admitted. (*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. (*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 := a * 100000 + b * 10000 + c * 1000 + a * 100 + b * 10 + 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 | n) <-> (2 | last_digit n). Proof. Admitted. (*fr Lemme intermédiaire pour l'exercice 8 *) (*en Intermediate lemma for exercise 8 *) Lemma exercise07 (n : 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 | 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 | n) <-> (6 | (4 * ((digits_sum n) - (last_digit n)) + 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 *) Lemma exercise10_alt (n : Digits) : (6 | n) <-> (6 | (4 * ((digits_sum n) - (last_digit n)) + last_digit n)). Proof. Admitted. (*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 *) 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.