Newer
Older
(* Importation de bibliothèques pour les nombres
relatifs et la logique classique. *)
From Coq Require Import Arith_base ZArith Lia.
(* Dans ce fichier, les nombres sont par défaut
des relatifs. *)
Local Open Scope Z_scope.
Section SophieGermain.
(* On va avoir besoin de la notion de puissance.
On pourrait l’importer depuis une bibliothèque,
mais cela peut être plus intéressant de
l’axiomatiser. *)
(* On suppose donc une opération puissance.
Elle prend en argument un nombre relatif et un
entier naturel. *)
Hypothesis power : Z * nat -> Z.
(* Ajout d’une notation pour rendre le fichier
plus lisible. *)
Notation "a ^ b" := (power (a, b%nat)) : Z_scope.
(* On peut maintenant utiliser cette fonction dans
le fichier… mais on ne sait rien sur ce qu’elle renvoit !
On va donc ajouter des hypothèses sur son comportement : *)
Hypothesis power_0 : forall a, a ^ 0 = 1.
Hypothesis power_succ : forall a b, a ^ (b + 1) = a * (a ^ b).
(* ****************************************************** *)
(* Définitions utiles, mais qui n’ont pas besoin d’être
comprises pour le reste. *)
Lemma power_succ_nat : forall a (b : nat), a ^ (S b) = a * (a ^ b).
Proof.
intros. rewrite <- (power_succ a b). repeat f_equal. lia.
Qed.
Lemma power_succ_nat_r : forall a (b : nat), a ^ (S b) = (a ^ b) * a.
Proof.
intros. rewrite power_succ_nat. lia.
Qed.
(* Exemple de lemme : a² = a*a. *)
Lemma power_2 : forall a, a ^ 2 = a * a.
intro a.
repeat rewrite power_succ_nat.
rewrite power_0.
lia.
Qed.
Lemma fold_power_2 : forall a, a * (a * 1) = a ^ 2.
Proof.
intros. rewrite power_2. lia.
Qed.
Ltac unfold_power :=
repeat first [
rewrite power_2 in *
| rewrite power_0 in *
| rewrite power_succ_nat in * ].
Ltac fold_power :=
unfold_power;
repeat first [
rewrite fold_power_2 in *
| rewrite <- power_2 in *
| rewrite <- power_succ_nat in *
| rewrite <- power_succ_nat_r in * ].
Ltac refold_power :=
unfold_power;
repeat rewrite Z.mul_assoc in *;
fold_power.
Ltac liap :=
intros;
unfold_power;
lia.
Tactic Notation "replace" constr(a) "by" constr(b) :=
let E := fresh "E" in
assert (E : a = b);
[ liap
| repeat rewrite E; clear E ].
Tactic Notation "replace" constr(a) "by" constr(b) "in" hyp(H) :=
let E := fresh "E" in
assert (E : a = b);
[ liap
| repeat rewrite E in H; clear E ].
Tactic Notation "automatically" "prove" ident(N) ":" constr(P) :=
assert (N : P); [ liap |].
Ltac ttransitivity n :=
transitivity n; [ liap |].
repeat lazymatch goal with
| |- context [Zpos ?a * Zpos ?b] =>
let c := eval compute in (Zpos a * Zpos b) in
let E := fresh "E" in
assert (E : Zpos a * Zpos b = c); [ reflexivity | rewrite E in *; clear E ]
| |- context [?a * Zpos ?b * ?c] =>
| |- context [?a * Zpos ?b] =>
| |- _ => rewrite Z.mul_assoc
end.
Ltac sort_mul :=
unfold_power;
repeat rewrite Z.mul_assoc; repeat rewrite Z.add_assoc; repeat rewrite Z.add_sub_assoc;
repeat rewrite <- Z.mul_assoc; fold_power; repeat rewrite Z.mul_assoc.
Ltac get_power t :=
lazymatch t with
| _ ^ ?n => constr:(n)
| - _ ^ ?n => constr:(n)
| _ * _ ^ ?n => constr:(n)
| - (_ * _ ^ ?n) => constr:(n)
| _ * _ => constr:(1%nat)
| - (_ * _) => constr:(1%nat)
| _ => constr:(0%nat)
end.
Ltac sort_terms_add_in t :=
let sort_terms a b cont :=
let an := get_power a in
let bn := get_power b in
let d := eval compute in (bn <=? an)%nat in
lazymatch d with
| true => cont a b
| false =>
rewrite (Z.add_comm a b);
cont b a
| _ => cont a b
end in
lazymatch t with
| Zpos ?a + Zpos ?b =>
let c := eval compute in (Zpos a + Zpos b) in
let E := fresh "E" in
assert (E : Zpos a + Zpos b = c); [ reflexivity | rewrite E in *; clear E ]
| (Zpos ?a + Zpos ?b) + ?c =>
let d := eval compute in (Zpos a + Zpos b) in
let E := fresh "E" in
assert (E : Zpos a + Zpos b = d); [ reflexivity | rewrite E in *; clear E ];
sort_terms_add_in (d + c)
| (?a + Zpos ?b) + Zpos ?c =>
let d := eval compute in (Zpos b + Zpos c) in
rewrite <- (Z.add_assoc a (Zpos b) (Zpos c));
let E := fresh "E" in
assert (E : Zpos b + Zpos c = d); [ reflexivity | rewrite E in *; clear E ];
sort_terms_add_in (a + d)
| (?a + ?b) + ?c =>
rewrite <- (Z.add_assoc a b c);
sort_terms b c ltac:(fun b c =>
rewrite (Z.add_assoc a b c);
sort_terms_add_in (a + b))
| ?a + ?b =>
sort_terms a b ltac:(fun _ _ => idtac)
end.
Ltac sort_terms_add :=
lazymatch goal with
| |- ?a = ?b =>
sort_terms_add_in a;
sort_terms_add_in b
end.
Ltac sort_add :=
repeat rewrite <- Z.add_opp_r;
sort_terms_add;
repeat rewrite Z.add_opp_r.
Ltac sort_terms :=
sort_mul; sort_add.
Ltac apply_fact fact :=
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
let rec aux t :=
lazymatch t with
| (?a + ?b * ?bf) + ?c * ?cf =>
lazymatch bf with
| cf =>
rewrite <- (Z.add_assoc a (b * bf) (c * cf)) ;
fact b c cf ltac:(fun _ => rewrite (Z.add_0_r a); aux a) ltac:(fun bc => aux (a + bc))
| _ => aux (a + b * bf)
end
| ?b * ?bf + ?c * ?cf =>
lazymatch bf with
| cf =>
rewrite <- (Z.mul_add_distr_r b c cf) ;
fact b c cf ltac:(fun _ => repeat rewrite Z.add_0_l) ltac:(fun _ => idtac)
| _ => idtac
end
| ?a + _ => aux a
| _ => idtac
end in
repeat rewrite <- Z.add_opp_r;
repeat rewrite <- Z.mul_opp_l;
lazymatch goal with
| |- ?a = ?b =>
aux a;
aux b
end;
repeat rewrite Z.add_opp_r.
Ltac fact_powers :=
sort_terms;
apply_fact ltac:(fun b c cf contz cont =>
rewrite <- (Z.mul_add_distr_r b c cf) ;
cont ((b + c) * cf));
repeat rewrite Z.add_opp_l;
repeat rewrite Z.add_assoc;
repeat rewrite Z.add_sub_assoc.
Ltac cancel_terms :=
apply_fact ltac:(fun b c cf contz cont =>
rewrite <- (Z.mul_add_distr_r b c cf) ;
let bc := eval compute in (b + c) in
replace (b + c) by bc ;
lazymatch bc with
| 0 =>
rewrite (Z.mul_0_l cf);
contz tt
| _ => cont (bc * cf)
end).
Lemma Zmul_sub_add : forall a b,
(a - b) * (a + b) = a^2 - b^2.
Proof.
liap.
Qed.
Lemma contrapositive : forall P Q,
(~ Q -> ~ P) <-> (P -> Q).
Proof.
intros P Q.
destruct (classic Q) as [nq|q]; tauto.
Qed.
Ltac contrapositive_with P :=
generalize P; clear P;
apply contrapositive;
let nP := fresh "N" in
intro nP.
Lemma power_eq_0 : forall a n,
a^n = 0 -> a = 0.
Proof.
intros a n. induction n.
- rewrite power_0. inversion 1.
- replace (S n) by (n + 1)%nat. rewrite power_succ.
intro E.
destruct (Zmult_integral _ _ E); auto.
Qed.
Lemma power_2_pos : forall a,
a^2 >= 0.
Proof.
intro a.
rewrite power_2.
apply sqr_pos.
Qed.
Lemma Zeq_not : forall n m,
n < m \/ m < n -> n <> m.
Proof.
intros n m [I|I]; lia.
Qed.
Lemma square_add : forall a b,
(a + b)^2 = a^2 + 2 * a * b + b^2.
Proof.
intros a b. repeat rewrite power_2. lia.
Qed.
Lemma square_sub : forall a b,
(a - b)^2 = a^2 - 2 * a * b + b^2.
Proof.
intros a b. repeat rewrite power_2. lia.
Qed.
Ltac simplify :=
repeat rewrite <- Z.add_assoc;
repeat rewrite <- Z.add_sub_assoc;
simpl;
repeat rewrite Z.add_assoc;
repeat rewrite Z.add_sub_assoc;
simpl;
repeat rewrite Z.sub_add;
repeat rewrite Z.add_0_l;
repeat rewrite Z.add_0_r.
Ltac simplify_in E :=
repeat rewrite <- Z.add_assoc in E;
repeat rewrite <- Z.add_sub_assoc in E;
simpl in E;
repeat rewrite Z.add_assoc in E;
repeat rewrite Z.add_sub_assoc in E;
simpl in E;
repeat rewrite Z.sub_add in E;
repeat rewrite Z.add_0_l in E;
repeat rewrite Z.add_0_r in E.
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
Lemma cancel_inf_eq : forall n m, n >= 0 -> m <= n + m.
Proof. lia. Qed.
(* ****************************************************** *)
Section Pair.
(* Cas pair. *)
(* On considère un a tel que a = 2*n. *)
Variables a n : Z.
Hypothesis definition_a : a = 2*n.
Lemma a4p4_pair : exists m, a^4 + 4 = 2*m.
Proof.
exists (8*n^4 + 2).
(* On déroule la définition de a. *)
rewrite definition_a.
(* On peut rechercher des lemmes pour traiter
la distributivité. *)
Search (_ * (_ + _)).
(* On obtient beaucoup de lemmes, mais parmis eux :
Z.mul_add_distr_l: forall n m p : Z,
n * (m + p) = n * m + n * p *)
rewrite Z.mul_add_distr_l.
(* On réarange les multiplications. *)
sort_mul.
(* On se retrouve avec une égalité triviale. *)
reflexivity.
Qed.
Lemma a4p4_pas_2 : a^4 + 4 <> 2.
Proof.
(* On va même montrer que a^4 + 4 est strictement
plus grand. *)
apply Zeq_not.
right.
(* On traite la transivité. *)
apply Z.lt_le_trans with (m := 4); [lia|].
(* On annule les 4. *)
apply cancel_inf_eq.
(* Faisons apparaitre le carré. *)
replace (a^4) by ((a^2)^2).
(* Un carré est toujours positif. *)
apply power_2_pos.
Qed.
End Pair.
(* ****************************************************** *)
Section Chiffres.
(* Quelques propriétés sur les derniers chiffres. *)
Lemma égalité_remarquable_1 : forall a n,
a = 10*n + 1 ->
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
Proof.
intros a n definition_a.
rewrite definition_a.
unfold_power.
repeat rewrite Z.mul_add_distr_l.
repeat rewrite Z.mul_add_distr_r.
sort_mul.
exists (10*n^2 + 2*n).
rewrite Z.mul_add_distr_l.
sort_mul.
fact_powers.
reflexivity.
Qed.
(* Cela nous conduit à montrer que si a finit par 1,
alors a^4 + 4 n’est pas premier (sauf dans le cas 1). *)
Lemma divisibilité_1 : forall a n,
a = 10*n + 1 ->
exists m, a^4 + 4 = 5*m.
Proof.
intros a n definition_a.
destruct (égalité_remarquable_1 a n definition_a) as (x&definition_x).
destruct (égalité_remarquable_1 (a^2) x definition_x) as (y&definition_y).
exists (2*y + 1).
refold_power.
rewrite definition_y.
repeat rewrite Z.mul_add_distr_l.
sort_mul.
sort_add.
reflexivity.
Qed.
Lemma égalité_remarquable_9 : forall a n,
a = 10*n + 9 ->
exists m, a^2 = 10*m + 1.
Proof.
intros a n definition_a.
exists (10*n^2 + 18*n + 8).
liap.
Qed.
Lemma divisibilité_9 : forall a n,
a = 10*n + 9 ->
exists m, a^4 + 4 = 5*m.
Proof.
intros a n definition_a.
destruct (égalité_remarquable_9 a n definition_a) as (x&definition_x).
destruct (égalité_remarquable_1 (a^2) x definition_x) as (y&definition_y).
exists (2*y + 1).
liap.
Qed.
Lemma égalité_remarquable_3 : forall a n,
a = 10*n + 3 ->
exists m, a^2 = 10*m + 9.
Proof.
intros a n definition_a.
exists (10*n^2 + 6*n).
liap.
Qed.
Lemma divisibilité_3 : forall a n,
a = 10*n + 3 ->
exists m, a^4 + 4 = 5*m.
Proof.
intros a n definition_a.
destruct (égalité_remarquable_3 a n definition_a) as (x&definition_x).
destruct (égalité_remarquable_9 (a^2) x definition_x) as (y&definition_y).
exists (2*y + 1).
liap.
Qed.
Lemma égalité_remarquable_7 : forall a n,
a = 10*n + 7 ->
exists m, a^2 = 10*m + 9.
Proof.
intros a n definition_a.
exists (10*n^2 + 14*n + 4).
liap.
Qed.
Lemma divisibilité_7 : forall a n,
a = 10*n + 7 ->
exists m, a^4 + 4 = 5*m.
Proof.
intros a n definition_a.
destruct (égalité_remarquable_7 a n definition_a) as (x&definition_x).
destruct (égalité_remarquable_9 (a^2) x definition_x) as (y&definition_y).
exists (2*y + 1).
liap.
Qed.
(* On a alors fait les cas pairs, ainsi que lorsque
le chiffre des unités est 1, 3, 7, ou 9.
Il ne reste que 5.*)
Lemma cas_5 : forall a n,
a = 10*n + 5 ->
exists m, a^4 + 4 = 1000*m + 629.
Proof.
intros a n definition_a.
automatically prove E1: (a^4 = (5*(2*n+1))^4).
automatically prove E2: (a^4 = 625*(2*n+1)^4).
rewrite E2.
automatically prove E3: ((2*n+1)^4 = (4*n^2 + 4*n + 1)^2).
automatically prove E4: ((2*n+1)^4 = 16*n^4 + 32*n^3 + 24*n^2 + 8*n + 1).
rewrite E4.
exists (5*(2*n^4 + 4*n^3 + 3*n^2 + n)).
liap.
Qed.
End Chiffres.
(* ****************************************************** *)
Section Impair.
(* Cas général impair. *)
Lemma a4p4_fact_impair : forall a n,
a = 2*n + 1 ->
a^4 + 4 = (4*n^2 + 1) * (4*n^2 + 8*n + 5).
Proof.
liap.
Qed.
(* Un nombre est premier si et seulement si
toute décomposition en facteurs fait
apparaitre le facteur 1. *)
Definition premier p :=
forall a b, p = a*b -> a = 1 \/ b = 1.
Lemma a4p4_premier_impair : forall a n,
a = 2*n + 1 ->
premier (a^4 + 4) -> n = 0 \/ n = -1.
Proof.
intros a n E P.
apply a4p4_fact_impair in E.
apply P in E.
destruct E as [E|E].
- left.
liap.
- right.
automatically prove E1: (4*n^2 + 8*n + 4 = 0).
automatically prove E2: (n^2 + 2*n + 1 = 0).
automatically prove E3: ((n + 1)^2 = 0).
apply power_eq_0 in E3.
liap.
Qed.
End Impair.
(* ****************************************************** *)
Section Général.
(* Cas général *)
(* On veut montrer que a^4 + 4 = (a^2 - 2*a + 2) * (a^2 + 2*a + 2). *)
Lemma a4p4_fact_1 : forall a,
a^4 + 4 = (a^2 - 2*a + 2) * (a^2 + 2*a + 2).
Proof.
(* On introduit a. *)
intro a.
(* On peut rechercher des lemmes pour traiter la distributivité. *)
Search (_ * (_ + _)).
(* On obtient beaucoup de lemmes, mais parmis eux :
Z.mul_add_distr_l: forall n m p : Z, n * (m + p) = n * m + n * p *)
repeat rewrite Z.mul_add_distr_l.
(* On peut faire la même chose pour la distributivité à droite. *)
repeat rewrite Z.mul_add_distr_r.
(* On peut faire de même avec la distributivité de la soustration sur l’addition. *)
Search ((_ - _) * _).
repeat rewrite Z.mul_sub_distr_r.
(* On réarange les multiplications. *)
sort_mul.
(* On les regroupe par puissance. *)
fact_powers.
simplify.
(* On se retrouve avec une égalité triviale. *)
reflexivity.
Qed.
Lemma a4p4_fact_2 : forall a,
a^4 + 4 = (a^2 - 2*a + 2) * (a^2 + 2*a + 2).
Proof.
(* La preuve précédente était assez calculatoire.
On peut vouloir construire des preuves plus indirectes,
mais avec des étapes plus lisibles.
Ici par exemple, le terme a^2 + 2 joue un rôle assez important :
on peut vouloir le mettre en avant. *)
(* On introduit a. *)
intro a.
(* On réorganise la position des termes pour faire apparaitre a^2 + 2. *)
replace (a^2 - 2*a + 2) by (a^2 + 2 - 2*a).
replace (a^2 + 2*a + 2) by (a^2 + 2 + 2*a).
(* On définit A = a^2 + 2 et B = 2*a. *)
set (A := a^2 + 2).
set (B := 2*a).
(* On peut réécrire l’identité remarquable. *)
rewrite Zmul_sub_add.
(* On peut maintenant remplacer A et B par leur valeur. *)
unfold A, B.
(* On déroule l’identité remarquable du carré d’une somme. *)
repeat rewrite square_add.
(* Comme dans l’autre preuve, il suffit maintenant de réorganiser l’expression.
Notez cependant que les expressions sont maintenant moins longues et un petit peu
plus lisibles. *)
sort_terms.
reflexivity.
Qed.
Lemma a4p4_fact_3 : forall a,
a^4 + 4 = (a^2 - 2*a + 2) * (a^2 + 2*a + 2).
Proof.
(* Une méthode alternative est de profiter de la machine pour automatiser la
construction de la preuve.
Ici, cette tactique est capable de gérer toutes les égalités qui n’utilisent
que l’addition, la soustraction, et certaines formes de multiplication
(ce qu’on appelle « l’arithmétique linéaire sur les entiers »). *)
Lemma a4p4_premier : forall a,
premier (a^4 + 4) ->
a = 1 \/ a = -1.
Proof.
intros a P.
set (F := a4p4_fact_1).
apply P in F.
destruct F as [E|E].
- automatically prove E1: (a^2 - 2*a + 1 = 0).
automatically prove E2: ((a - 1)^2 = 0).
apply power_eq_0 in E2.
left.
liap.
- automatically prove E1: ((a + 1)^2 = 0).
apply power_eq_0 in E1.
right.
liap.
Qed.
End Général.
(* ****************************************************** *)
(* Une autre preuve : on veut montrer que si a ≠ 1, alors a^2 - 2*a + 2 ≠ 1.
Comme auparavant, il y a plusieurs manière de le montrer. *)
Lemma a2m2ad1_1 : forall a,
a <> 1 ->
a^2 - 2*a + 2 <> 1.
Proof.
(* On introduit a. *)
(* On peut réécrire a^2 - 2*a + 2 comme (a - 1)^2 + 1. *)
replace (a^2 - 2*a + 2) by ((a - 1)^2 + 1) in N.
(* On soustrait 1 des deux côtés de l’égalité dans E. *)
apply Z.sub_cancel_r with (p := 1) in N.
simplify_in N.
(* On peut maintenant ajouter 1 des deux côtés de l’égalité pour obtenir notre résultat. *)
apply Z.add_cancel_r with (p := 1) in N.
simplify_in N.
apply N.
Qed.
Lemma a2m2ad1_2 : forall a,
a <> 1 ->
a^2 - 2*a + 2 <> 1.
Proof.
(* Dans le cas où on n’aurait pas vu la factorisation a^2 - 2*a + 2 = (a - 1)^2 + 1,
on peut faire une analyse par disjonction de cas. *)
(* On introduit a tel que a ≠ 1. *)
intros a D.
(* Si a ≠ 1 alors soit a < 1, soit a > 1. *)
apply not_Zeq in D.
(* On considère les deux cas. *)
destruct D as [D|D].
- (* Dans le premier cas, a < 1. *)
(* On a donc 2*a négatif. *)
automatically prove I: (a^2 - 2*a + 2 >= 2).
(* Et donc différent de 1. *)
liap.
- (* Dans le second cas, a > 1. *)
(* On peut alors factoriser a^2 - 2*a en a*(a - 2), deux facteurs positifs. *)
replace (a^2 - 2*a) by (a*(a - 2)).
(* Nous montrons donc que cette expression est plus grande que 1. *)
apply Zeq_not.
right.
(* Plus précisément, de 2. *)
{ liap. }
(* On enlève deux de chaque côté. *)
apply Z.sub_le_mono_r with (p := 2).
simplify.
(* On se ramène à montrer que chacun des facteurs sont positifs. *)
apply Z.mul_nonneg_nonneg.
+ liap.
+ liap.
Qed.
(* ****************************************************** *)
(* Malheureusement… notre définition de premier n’est pas
celle que l’on a l’habitude en maths !
On peut par exemple montrer que 2 n’est pas « premier »
selon notre définition. *)
Lemma deux_pas_premier : ~ premier 2.
Proof.
intro P.
automatically prove E: (2 = (-1) * (-2)).
apply P in E.
destruct E as [E|E].
- inversion E.
- inversion E.
Qed.
(* On a donc en fait sans le savoir montré un mauvais théorème :
il n’est pas faux, mais il ne parle pas de nombre premier
comme en mathématiques.
En l’occurrence, on peut modifier notre définition de « premier »
pour qu’elle corresponde à celle en mathématiques, et cela ne
change pas les résultats (ouf !).
Mais parfois, ce genre de problème de définition peut casser
totalement une preuve : il faut toujours faire attention aux
modèles. *)
End SophieGermain.