Mentions légales du service

Skip to content
Snippets Groups Projects
puissances.v 18.7 KiB
Newer Older
(* Importation de bibliothèques pour les nombres
  relatifs et la logique classique. *)
From Coq Require Import Arith_base ZArith Lia.
From Coq Require Import Logic.Classical.
(* 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 limporter depuis une bibliothèque,
 mais cela peut être plus intéressant de
 laxiomatiser. *)

(* On suppose donc une opération puissance.
 Elle prend en argument un nombre relatif et un
 entier naturel. *)
Hypothesis power : Z * nat -> Z.
(* Ajout dune 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 quelle 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 nont 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 |].

Ltac sort_terms_mul :=
  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] =>
           replace (a * Zpos b * c) by (Zpos b * a * c)
         | |- context [?a * Zpos ?b] =>
           replace (a * Zpos b) by (Zpos b * a)
         | |- _ => 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;
  sort_terms_mul;
  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.

  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.

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 ->
BODIN Martin's avatar
BODIN Martin committed
  exists d, a^2 = 10*d + 1.
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 nest 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 laddition. *)
  Search ((_ - _) * _).
  repeat rewrite Z.mul_sub_distr_r.

  (* On réarange les multiplications. *)
  sort_mul.

  (* On les regroupe par puissance. *)
  fact_powers.
  (* Beaucoup de termes sannulent alors. *)

  (* 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 lidentité remarquable. *)
  rewrite Zmul_sub_add.

  (* On peut maintenant remplacer A et B par leur valeur. *)
  unfold A, B.

  (* On déroule lidentité remarquable du carré dune somme. *)
  repeat rewrite square_add.

  (* Comme dans lautre preuve, il suffit maintenant de réorganiser lexpression.
   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 nutilisent
    que laddition, la soustraction, et certaines formes de multiplication
    (ce quon appelle « larithmé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 raisonne par contraposé. *)
  contrapositive_with D.

  (* 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 en déduit que a - 1 = 0. *)
  apply power_eq_0 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 naurait 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 N: (2*a <= 0).

    (* Et a^2 est positif. *)
    automatically prove P: (a^2 >= 0).

    (* Donc a^2 - 2*a + 2 >= 2. *)
    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. *)
    apply Z.lt_le_trans with (m := 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 nest pas
  celle que lon a lhabitude en maths !
  On peut par exemple montrer que 2 nest 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 nest pas faux, mais il ne parle pas de nombre premier
  comme en mathématiques.
  En loccurrence, on peut modifier notre définition de « premier »
  pour quelle 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. *)