(* This file is part of the "Initiation aux preuves formelles " course in Villetaneuse, France. Copyright (C) Kerjean, 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. *)

Nombre réels 2 : les réels comme corps ordonné

Corps ordonné

Un corps ordonné est un corps (comme dans Corps.v) qui a, en plus, une relation d'ordre stricte qui est :

• transitive
• asymétrique : forall x y, x < y
• > ~ (x < y)
• totale
• compatible avec l'addition et la multiplication

Module Type AxiomesCorpsOrdonné. Parameter Inline(10) (t : Type). Parameters (add mul : t -> t -> t) (opp inv : t -> t) (zero one : t). Infix "+" := add. Infix "*" := mul. Notation "- x" := (opp x). Notation "/ x" := (inv x). Notation "0" := zero. Notation "1" := one. Axiom add_comm : forall (x y : t), x + y = y + x. Axiom add_assoc : forall (x y z : t), x + (y + z) = x + y + z. Axiom add_0_l : forall (x : t), 0 + x = x. Axiom add_opp_diag_l : forall (x : t), - x + x = 0. Axiom mul_comm : forall (x y : t), x * y = y * x. Axiom mul_assoc : forall (x y z : t), x * (y * z) = x * y * z. Axiom mul_1_l : forall (x : t), 1 * x = x. Axiom mul_inv_diag_l : forall (x : t), x <> 0 -> /x * x = 1. Axiom mul_add_distr_l : forall (x y z : t), x * (y + z) = x * y + x * z. Axiom neq_0_1 : 0 <> 1. Parameter (lt : t -> t -> Prop). Infix "<" := lt. Axiom lt_trans : forall (x y z : t), x < y -> y < z -> x < z. Axiom lt_asymm : forall (x y : t), x < y -> ~ (y < x). Axiom total_order : forall (x y : t), x < y \/ x = y \/ y < x. Axiom add_lt_compat_l : forall (x y z : t), y < z -> x + y < x + z. Axiom mul_lt_compat_l : forall (x y z : t), y < z -> 0 < x -> x * y < x * z. End AxiomesCorpsOrdonné. Module PropriétésCorpsOrdonné (Import A : AxiomesCorpsOrdonné).

Pour des raisons techniques, on doit rappeler certaines propriétés des corps...

Lemma add_opp_diag_r : forall (x : t), x + (- x) = 0. Proof. intros x; rewrite add_comm, add_opp_diag_l. reflexivity. Qed. Lemma add_0_r : forall (x : t), x + 0 = x. Proof. intros x; rewrite add_comm; exact (add_0_l _). Qed. Lemma add_eq_compat_l : forall (x y z : t), y = z -> x + y = x + z. Proof. intros x y z ->. reflexivity. Qed. Lemma add_eq_reg_l : forall x y z : t, x + y = x + z -> y = z. Proof. intros x y z H; apply (add_eq_compat_l (- x)) in H. rewrite 2!add_assoc, add_opp_diag_l, 2!add_0_l in H; exact H. Qed. Lemma double_fixpoint_0 : forall (x : t), x + x = x -> x = 0. Proof. intros x H; apply (add_eq_reg_l x); rewrite add_0_r; exact H. Qed. Lemma mul_0_r : forall x : t, x * 0 = 0. Proof. intros x; apply double_fixpoint_0; rewrite <-(mul_add_distr_l), add_0_l. reflexivity. Qed. Lemma opp_0 : - 0 = 0. Proof. apply (add_eq_reg_l 0); rewrite add_0_r, add_opp_diag_r; reflexivity. Qed. Lemma opp_opp : forall (x : t), - (- x) = x. Proof. intros x. apply (add_eq_reg_l (- x)). rewrite add_opp_diag_r, add_opp_diag_l. reflexivity. Qed. Lemma mul_1_r : forall (x : t), x * 1 = x. Proof. intros x; rewrite mul_comm, mul_1_l; reflexivity. Qed.

Comme dans Corps, il y a certaines propriétés qu'on suppose acquises par construction qu'on appellera "Briques" et que vous pouvez considérer comme des axiomes. L'ordre "inférieur strictement", noté < est appelé lt dans la bibliothèque standard ("lt" pour "less than").

Une relation d'ordre strict est par définition asymétrique :

Check lt_asymm. (* Brique 11 *)

Une conséquence directe et importante est l'irréflexivité :

Exercice : Prouver le théorème suivant.

Lemma lt_irrefl : forall (x : t), ~(x < x). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Une relation d'ordre strict est par définition transitive :

Check lt_trans. (* Brique 12 *)

Noter qu'en général, coq ne peut pas deviner avec quel y (valeur "du milieu") appliquer la transitivité, alors que pour x et y (valeurs "au bord"), il sait souvent le faire. Donc, le plus souvent, pour prouver une inégalité par transitivité, ça donne apply (lt_trans _ bidule). avec bidule à remplacer. Voici une petite application (à but purement pédagogique) :

Exercice : Prouver le théorème suivant.

Theorem exercice_trans : forall x y z, x < y -> y < z -> z < x -> False. Proof. (* Indication : pour prouver False, il suffit de prouver x < x *) (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

On pourrait munir t d'une infinité de relations d'ordre strict. Mais ce qui rend vraiment l'ordre usuel unique est qu'il est compatible avec l'addition et la multiplication par un nombre strictement positif.

On suppose maintenant acquis (Brique 13) que la construction des réels fournit la compatibilité avec l'addition à gauche :

Check add_lt_compat_l. (* Brique 13 *)

Exercice : Prouver le théorème suivant.

Theorem add_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem add_lt_reg_l : forall r r1 r2 : t, r + r1 < r + r2 -> r1 < r2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem opp_decr : forall r1 r2 : t, r2 < r1 -> - r1 < - r2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Ensuite, passons à la compatibilité avec la multiplication par un réel positif.

Check mul_lt_compat_l. (* Brique 14 *)

Exercice : Prouver le théorème suivant.

Theorem mul_lt_compat_r : forall r r1 r2, r1 < r2 -> 0 < r -> r1 * r < r2 * r. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem mul_pos_compat : forall r1 r2 : t, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

On peut multiplier des inégalités entres elles, sous conditions de positivité.

Exercice : Prouver le théorème suivant.

Theorem mul_compat : forall r1 r2 r3 r4, 0 < r3 -> 0 < r2 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

La dernière propriété que l'on admet sur l'ordre < est que c'est un ordre total (brique 15) : pour deux réels x et y, on a soit x < y soit x = y soit y < x.

Check total_order. (* Brique 15 *)

Ordre non strict <=

L'ordre <= (inférieur ou égal) est défini très simplement de la façon suivante :

Definition le x y := x < y \/ x = y. (* le pour "less or equal to" *) Infix "<=" := le.

Quelques exercices rapides : penser à unfold Rle.

Exercice : Prouver le théorème suivant.

L'ordre non strict est (comme tous les ordres non stricts) réflexif :

Theorem le_refl : forall r, r <= r. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem lt_or_le : forall r1 r2 : t, r1 < r2 \/ r2 <= r1. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem lt_le : forall r1 r2, r1 < r2 -> r1 <= r2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

L'ordre <= est aussi (comme tous les ordres non stricts) antisymétrique :

Exercice : Prouver le théorème suivant.

Theorem le_antisym : forall r1 r2 : t, r1 <= r2 -> r2 <= r1 -> r1 = r2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Enfin, l'ordre <= est transitif.

Exercice : Prouver le théorème suivant.

Theorem le_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem le_lt_trans : forall r1 r2 r3 : t, r1 <= r2 -> r2 < r3 -> r1 < r3. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Tous les carrés sont positifs

Le but de cette partie est de montrer que tous les carrés sont positifs. Cela va faire intervenir une bonne partie des résultats précédents.

Le carré d'un réel x est noté x². La fonction associée est sqr ("sqr" pour "square" qui signifie carré en anglais).

Definition sqr x := x * x. Notation "x ²" := (sqr x).

Un petit exemple en fait bien utile :

Theorem sqr_mul_diag : forall r, r² = r * r. Proof. intros r. unfold sqr. reflexivity. Qed.

On a besoin d'un certain nombre de résultats intermédiaires.

On rappelle :

Check opp_opp.

Exercice : Prouver le théorème suivant.

Lemma mul_opp_l : forall (x y : t), x * - y = - (x * y). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem mul_opp_opp : forall r1 r2 : t, - r1 * - r2 = r1 * r2. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem sqr_nneg : forall r : t, 0 <= r². Proof. (* Indice : unfold sqr et raisonner par cas sur l'ordre entre 0 et r. *) (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Comme jolie et importante application : 1 est plus grand que 0 :D

C'est l'occasion d'introduire une nouvelle tactique et un petit théorème utile.

Le théorème eq_sym permet, avec apply de changer le sens d'une égalité.

Theorem eq_sym : forall (A : Type) (x y : A), x = y -> y = x. Proof. intros A x y ->; reflexivity. Qed.

La tactique assert permet (dans cet ordre) 1. d'énoncer une nouvelle hypothèse 2. de la prouver dans le contexte actuel 3. de l'utiliser dans la suite de la preuve. Elle est typique du raisonnement "vers l'avant" souvent utilisé en mathématiques. Voici un exemple idiot.

Theorem exemple_assert : forall x y, 1 <= x -> x <= 1 -> y = 1 -> x = y. Proof. intros x y H1 H2 H3. assert (x = 1) as H. { (* preuve de l'assertion *) apply le_antisym. - exact H2. - exact H1. } (* suite de la preuve : on peut utiliser H *) rewrite H. apply eq_sym. exact H3. Qed. Theorem lt_0_1: 0 < 1. Proof. (* Indice : 1 est un carré, et la propriété [R1_neq_R0] dit que 1 n'est pas égal à 0. *) (* On commence par prouver que [0 <= 1]. *) assert (0 <= 1) as I. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) End PropriétésCorpsOrdonné.