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 to next marker (included) 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).

Vous pouvez utiliser Coq comme une calculette :

Compute 17 / 5.
Compute 123 / 24.

(* À vous pour celui-ci : *)
Lemma divide_echauffement' : (17 | 493).
Proof.
  unfold Z.divide.
  exists 29.
  simpl.
  reflexivity.
Qed.

(* On va maintenant prouver que la divisibilité est réflexive et transitive. *)
(* 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.
  unfold Z.divide.
  exists 1.
  rewrite Z.mul_1_l.
  reflexivity.
Qed.

(* 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.

(* 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.
  intros Hxy Hyz.
  destruct Hxy as [k Hk].
  destruct Hyz as [k' Hk'].
  exists (k' * k).
  rewrite Hk', Hk, Z.mul_assoc.
  reflexivity.
Qed.

(* 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.
  intros Hxy Hyz.
  destruct Hxy as [k Hk].
  destruct Hyz as [k' Hk'].
  exists (k + k').
  rewrite Hk', Hk.
  rewrite <-Z.mul_add_distr_r.
  reflexivity.
Qed.

(* ** Division euclidienne *)

(* 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.

(* ** Division euclidienne et divisibilité *)

Lemma exercise01 (n p : Z) : n mod 7 = 3 -> p mod 7 = 1 -> (7 | 2 * n + p * p).
Proof.
  intros hn hp.
  destruct (Z.mod_decomp p 7 1) as [k hk]; try easy.
  destruct (Z.mod_decomp n 7 3) as [k' hk']; try easy.
  subst n p.
  replace
     (2 * (7 * k' + 3) + (7 * k + 1) * (7 * k + 1)) with
     (7 * (7 * k * k + 2 * k + 2 * k' + 1)) by lia.
  apply Z.divide_factor_l.
Qed.

(* Exercice 1 de la fiche d'exercice du lycée Blaise Pascal, preuve alternative *)

Lemma exercise01_with_auto (n p : Z) : n mod 7 = 3 -> p mod 7 = 1 -> (7 | 2 * n + p * p).
Proof.
  intros Hn Hp; apply Z.mod_divide.
  rewrite Z.add_mod, (Z.mul_mod 2), (Z.mul_mod p), Hn, Hp, Z.mul_1_r.
  reflexivity.
Qed.
(* End solution for the teacher *)

(* Exercice 5 de la fiche d'exercice du lycée Blaise Pascal *)

Lemma exercise02 : (17 | 35 ^ 228 + 84 ^ 501).
Proof.
  apply Z.mod_divide; easy.
Qed.

(* 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 *)
Lemma exercise03 : (17 | 35 ^ 22800 + 84 ^ 500001).
Proof.
  apply Z.mod_divide.
  rewrite Z.add_mod, (Z.pow_mod 35), (Z.pow_mod 84).
  replace (35 mod 17) with 1 by reflexivity.
  (* We don't really work on Z/nZ so can't replace 16 with -1 *)
  replace (84 mod 17) with (17 + - 1) by reflexivity.
  rewrite (Z.pow_mod (17 + -1)).
  replace ((17 + -1) mod 17) with (-1 mod 17) by reflexivity.
  rewrite <-(Z.pow_mod _ 500001).
  rewrite Z.pow_m1_l_odd;
    [| exact (Pos2Z.is_nonneg _) | exists 250000; reflexivity].
  rewrite Z.pow_1_l by (exact (Pos2Z.is_nonneg _)). (* <- bad pow *)
  rewrite <-(Z.add_mod), Z.add_opp_diag_r, Z.mod_0_l.
  reflexivity.
Qed.

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).

(* Exercice 2.b page 143 du livre Mathématiques Hyperbole option Maths Expertes *)

Lemma exercise04_with_auto (a b c : Digit) : (91 | abcabc a b c).
Proof.
(* Begin solution for the teacher *)  
  apply (Z.divide_trans _ 1001).
  - exists 11; reflexivity.
  - replace
      (abcabc a b c) with
      (((Z_of_Digit a) * 100 + (Z_of_Digit b) * 10 + (Z_of_Digit c)) * 1001).
    + exact (Z.divide_factor_r _ _).
    + unfold abcabc. lia.
Qed.
(* End solution for the teacher *)

(* Preuve alternative de l'exercice 2.b page 143 du livre Mathématiques Hyperbole option Maths Expertes *)

Lemma exercise04 (a b c : Digit) : (91 | abcabc a b c).
Proof.
(* Begin solution for the teacher *)
  exists (11 * ((Z_of_Digit a) * 100 + (Z_of_Digit b) * 10 + (Z_of_Digit c))).
  unfold abcabc. (* lia now solves it *)
  assert ((Z_of_Digit a) * 100000 = ((Z_of_Digit a) * 100) * 1000) as ->. {
    rewrite <-Z.mul_assoc; reflexivity.
  }
  assert ((Z_of_Digit b) * 10000 = ((Z_of_Digit b) * 10) * 1000) as ->. {
    rewrite <-Z.mul_assoc; reflexivity.
  }
  rewrite <-2(Z.mul_add_distr_r _ _ 1000).
  rewrite <-!Z.add_assoc.
  rewrite <-Z.mul_succ_r, <-Z.add_1_r.
  replace (1000 + 1) with (91 * 11) by reflexivity.
  rewrite <-Z.mul_assoc, (Z.mul_comm 11), !Z.mul_assoc.
  reflexivity.
Qed.
(* End solution for the teacher *)

(* Exercice 63 page 154 du livre Mathématique Hyperbole option Maths Expertes *)

Lemma exercise05 : findall (fun x => ((78^115372 + 92^23238 + 106^35536) mod 7 = x)).
Proof.
(* Begin solution for the teacher *)  
  specialize (Z.pow_mod 78 115372 7) as h1.
  remember (78 ^ 115372) as b1.
  replace (78 mod 7) with 1 in h1; [|reflexivity].
  rewrite Z.pow_1_l in h1; [|cbv; intro h; inversion h].

specialize (Z.pow_mod 92 23238 7) as h2.
  remember (92 ^ 23238) as b2.
  replace (92 mod 7) with 1 in h2; [|reflexivity].
  rewrite Z.pow_1_l in h2; [|cbv; intro h; inversion h].

specialize (Z.pow_mod 106 35536 7) as h3.
  remember (106 ^ 35536) as b3.
  replace (106 mod 7) with 1 in h3; [|reflexivity].
  rewrite Z.pow_1_l in h3; [|cbv; intro h; inversion h].

assert (HG: (b1 + b2 + b3) mod 7 = 3).
  * rewrite (Z.add_mod (b1+b2) b3 7).
    rewrite (Z.add_mod b1 b2 7).
    rewrite h1. rewrite h2. rewrite h3. reflexivity.
  * simpl. exists [3]. split.
    + apply Forall_forall.
      intros x hx.
      apply in_inv in hx.
      destruct hx; [|contradiction]. now subst x.
    + intros x hx.
      constructor.
      symmetry.
      now rewrite <- hx.
Qed.
(* End solution for the teacher *)

(* Énoncé alternatif de l'exercice 63 page 154 du livre Mathématique Hyperbole option Maths Expertes
sans findall *)
Lemma exercise05_alt : (78 ^ 115372 + 92 ^ 23238 + 106 ^ 35536) mod 7 = 3.
Proof.
(* Begin solution for the teacher *)
  (* We need to hide the explicit constants to block reduction. *)
  remember 115372 as a eqn:def_a.
  remember 23238 as b eqn:def_b.
  remember 35536 as c eqn:def_c.
  rewrite Z.add_mod, (Z.add_mod (78 ^ a)).
  rewrite (Z.pow_mod 78), (Z.pow_mod 92), (Z.pow_mod 106).
  replace (78 mod 7) with 1 by (reflexivity).
  replace (92 mod 7) with 1 by (reflexivity).
  replace (106 mod 7) with 1 by (reflexivity).
  rewrite 3!Z.pow_1_l by (subst; exact (Pos2Z.is_nonneg _)).
  reflexivity.
Qed.
(* End solution for the teacher *)

(* Lemme intermédiaire pour l'exercice 10 *)

Lemma exercise06 (n : Digits) : (2 | (Z_of_Digits n)) <-> (2 | (Z_of_Digit (last_digit n))).
Proof.
(* Begin solution for the teacher *)
  assert (forall k, (2 | 10 * k)) as key. {
    intros k; apply Z.divide_mul_l; exists 5; reflexivity.
  }
  rewrite (Z.decimal_decomposition n); split; intros H.
  - apply Z.divide_add_cancel_l with (2 := H); exact (key _).
  - apply Z.divide_add_r; [exact (key _) | exact H].
Qed.
(* End solution for the teacher *)

(* Lemme intermédiaire pour l'exercice 8 *)

Lemma exercise07 (n : Digits) : ((Z_of_Digits n) mod 3 = (digits_sum n) mod 3).
Proof.
(* Begin solution for the teacher *)
  induction n as [d | h t IH]; [reflexivity |].
  rewrite Z.digits_sum_digits, Z.Z_of_Digits_dcons, Z.add_mod.
  rewrite Z.mul_mod, Z.pow_mod.
  replace (10 mod 3) with 1 by (reflexivity).
  rewrite Z.pow_1_l; [| exact (Z.digits_len_nneg _)]. (* <- ugly *)
  rewrite <-(Z.mul_mod), Z.mul_1_r, (Z.add_mod (Z_of_Digit h)), IH; reflexivity.
Qed.
(* End solution for the teacher *)

(* Lemme pour l'exercice 10
   Indice: utiliser l'exercice 07 *)
Lemma exercise08 (n : Digits) : (3 | (Z_of_Digits n)) <-> (3 | digits_sum n).
Proof.
(* Begin solution for the teacher *)
  setoid_rewrite <-Z.mod_divide.
  rewrite exercise07; reflexivity.
Qed.
(* End solution for the teacher *)

(* Lemme pour l'exercice 10 *)

Lemma exercise09 (n : Z) : (6 | n) <-> (3 | n) /\ (2 | n).
Proof.
(* Begin solution for the teacher *)
  split.
  - intros [k ->]; split; apply Z.divide_mul_r, Z.mod_divide; reflexivity.
  - intros [[q Hq] H]; rewrite Hq in H |- *.
    assert (2 | q) as [q' ->]. {
      apply (Z.gauss _ 3 q); [rewrite Z.mul_comm; exact H | reflexivity].
    }
    rewrite <-Z.mul_assoc; replace (2 * 3) with 6 by (reflexivity).
    exact (Z.divide_factor_r _ _).
Qed.

(* Exercice 119 page 161 du livre 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.
(* Begin solution for the teacher *)
  apply iff_trans with (1:=exercise09 (Z_of_Digits n)).
  rewrite and_iff_compat_r with (1 := exercise08 n).
  rewrite and_iff_compat_l with (1 := exercise06 n).
  split.
  - intros [H3 H2]; apply exercise09; split.
    + replace (4 * (digits_sum n - (Z_of_Digit (last_digit n))) + (Z_of_Digit (last_digit n))) with
        (4 * digits_sum n + 3 * (- (Z_of_Digit (last_digit n)))) by ring.
      apply Z.divide_add_r.
      * apply Z.divide_mul_r; exact H3.
      * exact (Z.divide_factor_l _ _).
    + apply Z.divide_add_r; [| exact H2].
      apply Z.divide_mul_l; exists 2; reflexivity.
  - intros [H3 H2]%exercise09; split.
    + replace (4 * (digits_sum n - (Z_of_Digit (last_digit n))) + (Z_of_Digit (last_digit n))) with
        (3 * ((digits_sum n) - (Z_of_Digit (last_digit n))) + (digits_sum n)) in H3 by ring.
      apply Z.divide_add_cancel_l with (2 := H3); exact (Z.divide_factor_l _ _).
    + apply Z.divide_add_cancel_l with (2 := H2).
      apply Z.divide_mul_l; exists 2; reflexivity.
Qed.
(* End solution for the teacher *)

(* Preuve alternative de l'exercice 119 page 161 du livre Mathématique Hyperbole option Maths Expertes,
   en raisonnant par équivalence *)

(* @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.
(* Begin solution for the teacher *)
  setoid_rewrite exercise09; setoid_rewrite exercise08;
  setoid_rewrite exercise06.
  generalize (digits_sum n) as a, (Z_of_Digit (last_digit n)) as b; intros a b.
  assert ((3 | a) <-> (3 | 4 * (a - b) + b)) as part1. {
    replace (4 * (a - b) + b) with (4 * a + 3 * (- b)) by ring.
    pose proof (Z.divide_factor_l 3 (- b)) as Hd.
    setoid_rewrite (Z.divide_add_cancel_r _ _ _ Hd).
    assert (Z.gcd 3 4 = 1) as E by reflexivity.
    setoid_rewrite (Z.divide_mul_cancel_l _ _ _ E).
    reflexivity.
  }
  setoid_rewrite <-part1; setoid_rewrite (Z.divide_add_cancel_l 2);
    [| apply Z.divide_mul_l; exists 2; reflexivity].
  reflexivity.
Qed.

(* End solution for the teacher *)

(* Exercice 117 page 160 du livre 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.
(* Begin solution for the teacher *)
  assert (n mod 7 = 0 \/ n mod 7 = 1 \/ n mod 7 = 2 \/ n mod 7 = 4) as h1.
  - rewrite !hk, Z.mul_mod.
    study (k mod 7) between 0 and 6 as h2.
    8: pose proof (Z.mod_pos_bound k 7) as bounds; lia.
    all: rewrite <-h2; tauto.
  - assert (n mod 7 = 0 \/ n mod 7 = 1 \/ n mod 7 = 6) as h2.
    + rewrite !hq, (Z.mul_mod (q * q)), (Z.mul_mod q q).
      study (q mod 7) between 0 and 6 as h2.
      8: pose proof (Z.mod_pos_bound q 7) as bounds; lia.
      all: rewrite <-h2; tauto.
    + lia.
Qed.
(* End solution for the teacher *)

(* Lemme pour l'exercice 13 *)

Lemma exercise12 (x y p : Z) : prime p -> x * y = p -> (0 <= x) ->
    (x = p /\ y = 1) \/ (x = 1 /\ y = p).
Proof.
(* Begin solution for the teacher *)
  intros Hp H Hx.
  assert (x | p) as Hxdp by (exists y; symmetry; rewrite Z.mul_comm; exact H).
  pose proof (Z.prime_divisors p Hp x Hxdp) as [H' | [H' | [H' | H']]].
  - exfalso; lia.
  - right; split; [exact H' | rewrite H', Z.mul_1_l in H; exact H].
  - left; split; [exact H' |]; apply (Z.mul_reg_l _ _ x). {
      intros C; rewrite C in H'; apply Z.not_prime_0; rewrite H'; exact Hp.
    }
    rewrite Z.mul_1_r; rewrite H' at 2; exact H.
  - exfalso; pose proof (Z.prime_ge_2 p Hp) as pge2; lia.
Qed.
(* End solution for the teacher *)

(* Exercice 121 page 161 du livre Mathématique Hyperbole option Maths Expertes
   Indice: utiliser l'exercice 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.
(* Begin solution for the teacher *)
  exists (cons (7,6) nil); split.
  - (* not good, only Coq things *)
    apply Forall_forall; intros x [H1 | []].
    rewrite <- H1; lia.
  - intros [x y] [H1 [H2 [H3 H0]]]; constructor.
    assert ((x + y) * (x - y) = 13) as key by lia.
    assert (prime 13) as p13 by (apply Z.primeb_correct; reflexivity).
    assert (0 <= x + y) as sum_nneg by (lia).
    pose proof (exercise12 _ _ _ p13 key sum_nneg)
      as [[xeq yeq] | [xeq yeq]]; [| exfalso; lia].
    apply pair_equal_spec; lia.
Qed.
(* End solution for the teacher *)

(* Exercice 28 page 151 du livre 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.
(* Begin solution for the teacher *)
  intros h1 h2.
  assert (prime 5) as p5 by (apply Z.primeb_correct; reflexivity).
  enough (x | 5) as xd5. {
    pose proof (Z.prime_divisors 5 p5 _ xd5); lia.
  }
  apply (Z.divide_mul_r x 4 (9 * k + 2)) in h1.
  apply (Z.divide_mul_r x (-3) (12 * k + 1)) in h2.
  replace 5 with (4 * (9 * k + 2) + -3 * (12 * k + 1)).
  + now apply Z.divide_add_r.
  + lia.
Qed.
(* End solution for the teacher *)

(* Exercice 31 page 151 du livre Mathématique Hyperbole option Maths Expertes *)

Lemma exercise15 : findall (fun n => (0 <= n) /\ (n | n + 8)).
Proof.
(* Begin solution for the teacher *)
  exists [1; 2; 4; 8].
  split.
  - apply Forall_forall. intros x hx.
  atomize hx. 5: inversion hx.
  all: split; [lia | subst x; apply Z.mod_divide; easy].
  - intros x [hx1 hx2].
  assert (h2 : (x | 8)). {
    apply (Z.divide_add_r x (x + 8) (-x)) in hx2 as h3.
    - replace (x + 8 + -x) with 8 in h3; try easy; lia.
    - apply Z.divide_opp_r. apply Z.divide_refl.
  }
  study x between 0 and 8 as h3.
  10: apply Z.divide_pos_le in h2; lia.
  all: subst x.
  1: now apply Z.divide_0_l in h2.
  1, 2, 4, 8: now repeat constructor.
  all: apply Z.mod_divide in h2; cbn in h2; lia.
Qed.
(* End solution for the teacher *)