Nombres réels 3 : La valeur absolue et la distance sur les réels

On introduit dans ce sujet les nouveaux ingrédients fondamentaux pour l'analyse que sont la valeur absolue sur R et la distance sur R.

Rappels des propriétés des réels

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 les propriétés vues précédemment.

Lemma mul_add_distr_r : forall (x y z : t), (y + z) * x = y * x + z * x.
Proof.
  intros x y z. rewrite 3!(mul_comm _ x). exact (mul_add_distr_l _ _ _).
Qed.
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 add_eq_reg_r : forall x y z : t, y + x = z + x -> y = z.
Proof.
  intros x y z; rewrite (add_comm y), (add_comm z).
  exact (add_eq_reg_l x y z).
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 mul_0_l : forall x : t, 0 * x = 0.
Proof. intros x. rewrite mul_comm. exact (mul_0_r _). 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.
Lemma lt_irrefl : forall (x : t), ~(x < x).
Proof. intros x H. apply (lt_asymm x x); exact H. Qed.
Lemma add_lt_compat_r : forall x y z, y < z -> y + x < z + x.
Proof.
  intros x y z H; rewrite (add_comm y), (add_comm z).
  exact (add_lt_compat_l _ _ _ H).
Qed.
Lemma add_lt_reg_l : forall x y z : t, x + y < x + z -> y < z.
Proof.
  intros x y z H.
  rewrite <-(add_0_l y), <-(add_0_l z), <-(add_opp_diag_l x), <-2!add_assoc.
  exact (add_lt_compat_l _ _ _ H).
Qed.
Lemma opp_decr : forall x y : t, y < x -> - x < - y.
Proof.
  intros x y H; apply (add_lt_reg_l (x + y)).
  rewrite (add_comm x), <-add_assoc, add_opp_diag_r, add_0_r.
  rewrite (add_comm y), <-add_assoc, add_opp_diag_r, add_0_r.
  exact H.
Qed.
Lemma opp_add_distr : forall (x y : t), - (x + y) = (- x) + (- y).
Proof.
  intros x y. apply (add_eq_reg_l (x + y)).
  rewrite add_opp_diag_r, (add_comm x), <-add_assoc, (add_assoc x).
  rewrite add_opp_diag_r, add_0_l, add_opp_diag_r.
  reflexivity.
Qed.
Lemma mul_lt_compat_r : forall x y z, y < z -> 0 < x -> y * x < z * x.
Proof.
  intros x y z Hr H. rewrite 2!(mul_comm _ x).
  exact (mul_lt_compat_l _ _ _ Hr H).
Qed.
Lemma mul_pos_compat : forall x y : t, 0 < x -> 0 < y -> 0 < x * y.
Proof.
  intros x y H1 H2; rewrite <-(mul_0_r x); apply mul_lt_compat_l.
  - exact H2.
  - exact H1.
Qed.
Lemma mul_lt_compat : forall x y z t,
  0 < z -> 0 < y -> x < y -> z < t -> x * z < y * t.
Proof.
  intros x y z t H3 H2 H H'.
  apply (lt_trans _ (y * z)).
  - apply mul_lt_compat_r; [exact H | exact H3].
  - apply mul_lt_compat_l; [exact H'| exact H2].
Qed.
Definition le x y := x < y \/ x = y. (* le pour "less or equal to" *)
Infix "<=" := le.
Lemma le_refl : forall x, x <= x.
Proof. right. reflexivity. Qed.
Lemma lt_or_le : forall x y : t, x < y \/ y <= x.
Proof.
  intros x y.
  destruct (total_order x y) as [H | [H | H]].
  - left. exact H.
  - right. right. rewrite H. reflexivity.
  - right. left. exact H.
Qed.
Lemma lt_le : forall x y, x < y -> x <= y.
Proof. intros x y H. left. exact H. Qed.
Lemma le_antisym : forall x y : t, x <= y -> y <= x -> x = y.
Proof.
  intros x y [H1 | H1] [H2 | H2].
  - exfalso; apply (lt_asymm x y); [exact H1 | exact H2].
  - rewrite H2. reflexivity.
  - rewrite H1. reflexivity.
  - rewrite H1. reflexivity.
Qed.
Lemma le_trans : forall x y z, x <= y -> y <= z -> x <= z.
Proof.
  intros x y z [H1 | H1].
  - intros [H2 | H2].
    + left; exact (lt_trans _ _ _ H1 H2).
    + rewrite <-H2. left. exact H1.
  - intros H2. rewrite H1. exact H2.
Qed.
Lemma le_lt_trans : forall r1 r2 r3 : t, r1 <= r2 -> r2 < r3 -> r1 < r3.
Proof.
  intros r1 r2 r3 [H | H] H'.
  - exact (lt_trans _ _ _ H H').
  - rewrite H. exact H'.
Qed.
Definition sqr x := x * x.
Notation "x ²" := (sqr x) (at level 20).
Lemma sqr_mul_diag : forall x, x² = x * x.
Proof. intros x. unfold sqr. reflexivity. Qed.
Lemma mul_opp_l : forall (x y : t), x * - y = - (x * y).
Proof.
  intros x y.
  apply (add_eq_reg_l (x * y)).
  rewrite add_opp_diag_r, <-mul_add_distr_l, add_opp_diag_r, mul_0_r.
  reflexivity.
Qed.
Lemma mul_opp_opp : forall x y : t, - x * - y = x * y.
Proof.
  intros x y.
  rewrite mul_opp_l, mul_comm, mul_opp_l, opp_opp, mul_comm.
  reflexivity.
Qed.
Lemma nneg_sqr : forall x : t, 0 <= x².
Proof.
  intros x; unfold sqr.
  destruct (total_order 0 x) as [H | [H | H]].
  - left. apply mul_pos_compat; exact H.
  - right. rewrite <-H, mul_0_r. reflexivity.
  - left. rewrite <-mul_opp_opp. apply mul_pos_compat;
    rewrite <-opp_0; apply opp_decr; exact H.
Qed.
Lemma lt_0_1: 0 < 1.
Proof.
  assert (0 <= 1) as I. {
    rewrite <-(mul_1_r 1), <-sqr_mul_diag. exact (nneg_sqr 1).
  }
  destruct I as [I | E]; [exact I |].
  - exfalso. apply neq_0_1. exact E.
Qed.
End PropriétésCorpsOrdonné.

La valeur absolue : `Rabs`

Vous connaissez certainement la valeur absolue. Dans un cours de mathématiques, la valeur absolue d'un réel x est le réel noté |x| défini par : |x| =

x si x < 0 x si x >= 0.

En fait il y a certainement mille façon de définir la valeur absolue, mais ce qui importe ici, c'est que cette fonction s'appelle abs et qu'on admet les deux théorèmes suivants :

Pour prouver des choses sur abs, le plus souvent on raisonne par cas. Voici un exemple important : remarquer (lt_or_le x 0) : x < 0 \/ 0 <= x.

Deux remarques importantes sur la preuve précédente :

Nous avons utilisé rewrite avec un énoncé du type : x < 0 -> abs x = - x.

Ce qui se passe alors est :

dans le but, abs x est remplacé par -x;
vous continuez votre preuve;
à la fin, Coq vous demande de prouver que x < 0.
la deuxième fois on a fourni directment la preuve que 0 <= x avec rewrite abs_nneg by (exact I).

La preuve de x < 0

> 0 <
x va nous servir souvent, en fait c'est :

Exercice : Prouver le théorème suivant.

Petit détour par la fonction carré

La fonction carré s'appelle sqr dans notre bibliothèque. Le carré d'un réel x est noté x². Le plus simple est encore d'utiliser unfold sqr.

Exercice : Prouver le théorème suivant.

La fonction carré est injective sur les réels positifs.

Valeur absolue et carré

Exercice : Prouver le théorème suivant.

On se souvient qu'un carré est toujours positif :

et que le carré est invariant par opposé :

Exercice : Prouver le théorème suivant.

Pour le prochain exercice, il y a deux stratégies différentes :

séparer en 4 cas suivant le signe de x et de y
ou bien passer par la fonction carré

Exercice : Prouver le théorème suivant.

Bon... celui-ci est assez pénible à la main, vous avez le droit de le passer.

Exercice : Prouver le théorème suivant.

Ici, vous pourrez utiliser :

Exercice : Prouver le théorème suivant.

Distance usuelle sur les réels

La distance usuelle est notée dist dans cette bibliothèque.

Dans un cours de mathématique, elle est définie par d(x, y) = |y

Remarque culturelle au passage : généralement, en mathématiques, une distance sur un ensemble E est une fonction d de E * E dans l'ensemble des réels positifs ou nuls qui satisfait :

symétrie : d(x, y) = d(y, x)
séparation : d(x, y) = 0 <-> x = y
inégalité triangulaire : d(x, z) <= d(x, y) + d(y, x).

Nous concluons cette partie par une preuve de ces faits.

Exercice : Prouver le théorème suivant.

Penser à unfold dist

Exercice : Prouver le théorème suivant.

Penser à unfold dist et à opp_add_distr

Pour faciliter la preuve de la réflexivité, on a :

Exercice : Prouver le théorème suivant.

Vous pourrez utiliser la tactique replace

La tactique replace A with B remplace tous les A par B dans le but puis vous demande de prouver que A = B.

Nombres réels 3 : La valeur absolue et la distance sur les réels

Rappels des propriétés des réels

La valeur absolue : Rabs

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Petit détour par la fonction carré

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Distance usuelle sur les réels

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

Exercice : Prouver le théorème suivant.

La valeur absolue : `Rabs`