On travaille maintenant avec les nombres réels et les fonctions affines.
Soient a et b deux réels fixés mais quelconques.
Soit f la fonction (affine) suivante :
On commence par un cas assez simple : si a = 0, alors f est constante.
Mais avant de se lancer dans la preuve, il faut dire un peu comment on
travaille dans R.
On a un ensemble de règles de réécritures qu'on peut utiliser pour
remplacer des termes par d'autres dans le but (ou dans les hypothèses).
En voici quelques-unes, suivi d'un exemple et d'un exercice.
La commande Check permet d'afficher un théorème de nom donné
Check Rmult_0_r.
Check Rmult_0_l.
Check Rplus_0_r.
Check Rplus_0_l.
(* l est pour "left", à gauche et r pour "right", à droite *)
Theorem exemple_rewrite (x : R) :
(0 × 2 + x) + 3 × 0 = x.
Proof.
(* D'après Rmult_0_r, 3 * 0 peut être remplacé par 0. *)
rewrite Rmult_0_r.
(* D'après Rmult_0_l, 0 * 2 peut être remplacé par 0. *)
rewrite Rmult_0_l.
(* D'après Rplus_0_l, 0 + x peut être remplacé par x. *)
rewrite Rplus_0_l.
(* D'après Rplus_0_r, x + 0 peut être remplacé par x. *)
rewrite Rplus_0_r.
(* Les deux membres de l'égalité sont les mêmes, la preuve est finie. *)
reflexivity.
Qed.
(* À vous ! *)
Theorem exercice_rewrite (x y : R) :
((0 + (y × 0)) + 0 × x) + x = x.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Check Rmult_0_l.
Check Rplus_0_r.
Check Rplus_0_l.
(* l est pour "left", à gauche et r pour "right", à droite *)
Theorem exemple_rewrite (x : R) :
(0 × 2 + x) + 3 × 0 = x.
Proof.
(* D'après Rmult_0_r, 3 * 0 peut être remplacé par 0. *)
rewrite Rmult_0_r.
(* D'après Rmult_0_l, 0 * 2 peut être remplacé par 0. *)
rewrite Rmult_0_l.
(* D'après Rplus_0_l, 0 + x peut être remplacé par x. *)
rewrite Rplus_0_l.
(* D'après Rplus_0_r, x + 0 peut être remplacé par x. *)
rewrite Rplus_0_r.
(* Les deux membres de l'égalité sont les mêmes, la preuve est finie. *)
reflexivity.
Qed.
(* À vous ! *)
Theorem exercice_rewrite (x y : R) :
((0 + (y × 0)) + 0 × x) + x = x.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
On peut aussi utiliser rewrite avec des hypothèses.
Theorem exercice_rewrite2 (x : R) :
a = 0 → a + a = a × a.
Proof.
(* On suppose (hypothèse (H)) que a = 0. *)
intros H.
(* D'après (H), on peut remplacer a par 0 dans le but. *)
rewrite H.
(* À vous de terminer la preuve. *)
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
(* Maintenant les fonctions affines constantes.
Conseil : unfold constante et unfold f pour remplacer par les définitions. *)
Theorem a_0_affine_constante :
a = 0 → constante f.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
(* La réciproque est vraie : si f est constante, alors a = 0.
Mais la preuve utilise des tactiques pas encore vues, alors on vous la donne
avec les explications mathématiques en commentaires.
*)
Theorem affine_constante_a_0 :
constante f → a = 0.
Proof.
unfold constante, f.
(* On suppose que f est constante, donc que :
(H) : pour tous x, y dans R, a * x + b = a * y + b *)
intros H.
(* Comme c'est vrai pour tous les x et y de R, on peut l'écrire
en particulier pour x = 1 et y = 0. *)
specialize (H 1 0).
(* On a donc
(H) : a * 1 + b = a * 0 + b
On peut remplacer a * 1 par a. *)
rewrite Rmult_1_r in H.
(* Puis a * 0 par 0. *)
rewrite Rmult_0_r in H.
(* Enfin, comme on peut soustraire de chaque côté dans une égalité, on a
a + b = 0 + b -> a = 0, donc pour prouver que a = 0, il suffit
de prouver a + b = 0 + b. *)
apply (Rplus_eq_reg_r b).
(* Ce qui est exactement (H) *)
exact H.
Qed.
a = 0 → a + a = a × a.
Proof.
(* On suppose (hypothèse (H)) que a = 0. *)
intros H.
(* D'après (H), on peut remplacer a par 0 dans le but. *)
rewrite H.
(* À vous de terminer la preuve. *)
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
(* Maintenant les fonctions affines constantes.
Conseil : unfold constante et unfold f pour remplacer par les définitions. *)
Theorem a_0_affine_constante :
a = 0 → constante f.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
(* La réciproque est vraie : si f est constante, alors a = 0.
Mais la preuve utilise des tactiques pas encore vues, alors on vous la donne
avec les explications mathématiques en commentaires.
*)
Theorem affine_constante_a_0 :
constante f → a = 0.
Proof.
unfold constante, f.
(* On suppose que f est constante, donc que :
(H) : pour tous x, y dans R, a * x + b = a * y + b *)
intros H.
(* Comme c'est vrai pour tous les x et y de R, on peut l'écrire
en particulier pour x = 1 et y = 0. *)
specialize (H 1 0).
(* On a donc
(H) : a * 1 + b = a * 0 + b
On peut remplacer a * 1 par a. *)
rewrite Rmult_1_r in H.
(* Puis a * 0 par 0. *)
rewrite Rmult_0_r in H.
(* Enfin, comme on peut soustraire de chaque côté dans une égalité, on a
a + b = 0 + b -> a = 0, donc pour prouver que a = 0, il suffit
de prouver a + b = 0 + b. *)
apply (Rplus_eq_reg_r b).
(* Ce qui est exactement (H) *)
exact H.
Qed.
On passe au cas a > 0. Alors f est strictement croissante.
Pour prouver le théorème suivant, vous aurez besoin de certains
des résultats suivants :
Check Rplus_lt_compat_r.
Check Rplus_lt_compat_l.
Check Rmult_lt_compat_r.
Check Rmult_lt_compat_l.
Theorem a_sup_0_affine_croissante :
a > 0 → strict_croissante f.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Check Rplus_lt_compat_l.
Check Rmult_lt_compat_r.
Check Rmult_lt_compat_l.
Theorem a_sup_0_affine_croissante :
a > 0 → strict_croissante f.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Plus difficile, à faire seulement si vous avez bien compris la preuve de
affine_constante_a_0 :
Théorèmes que vous pouvez utiliser :
Check Rplus_lt_reg_r.
Check Rplus_lt_reg_l.
Check Rlt_0_1.
Theorem affine_croissante_a_sup_0 :
strict_croissante f → 0 < a.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Definition strict_decroissante (f : R → R) :=
∀ x y : R, x < y → f x > f y.
Check Rplus_lt_reg_l.
Check Rlt_0_1.
Theorem affine_croissante_a_sup_0 :
strict_croissante f → 0 < a.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Definition strict_decroissante (f : R → R) :=
∀ x y : R, x < y → f x > f y.
Pour prouver le théorème suivant, vous aurez besoin de ce théorème qui
dit qu'en multipliant une inégalité par un nombre négatif, l'inégalité
est renversée :
Check Rmult_lt_gt_compat_neg_l.
Theorem a_inf_0_affine_decroissante :
a < 0 → strict_decroissante f.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Theorem a_inf_0_affine_decroissante :
a < 0 → strict_decroissante f.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Vraiment si vous en voulez encore, vous pouvez essayer de prouver le
théorème qui va suivre.
Indice : x > y est juste une notation pour y < x.
Exemple pour illustrer l'indice :
Attention ce qui suit est vraiment compliqué. Indice: vous pouvez faire un "rewrite _ in _ "
Theorem affine_decroissante_a_inf_0 :
strict_decroissante f → a < 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
End Variations.
strict_decroissante f → a < 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
End Variations.