Devoir à la maison de preuves formelles

Consignes

Ce devoir est à rendre sur le dépôt moodle avant le : lundi 9 décembre à 23h59
Vous rendrez un seul fichier appelé Devoir2-2024.v et complèterez la déclaration suivante ci-dessous :

(*
    NOM, prénom, numéro étudiant : Je déclare qu'il s'agit de mon propre
    travail et que ce travail a été réalisé intégralement par un être humain.
*)
C'est un travail individuel. Vous pouvez vous aider les uns les autres mais vous ne devez jamais vous montrer le code de votre solution. L'usage de ChatGPT ou de toute autre intelligence artificielle pour résoudre les exercices est interdit (vous pouvez à la limite lui poser des questions sur des points mal compris). Si vous avez des questions (autres que "comment résoudre cet exercice"), vous pouvez les poser (en anglais) sur : https://coq.zulipchat.com/ dans le "stream" Coq Users (nécessite une inscription avec une adresse mail). Il est possible aussi d'envoyer des mails à rousselin@univ-paris13.fr.
Il y a 5 parties inégales et indépendentes.
  • Partie 1 : calcul des propositions, avec deux questions posées lors du partiel d'initiation aux structures mathématiques
  • Partie 2 : entiers naturels et un ordre "chelou", vu dans le partiel d'initiation aux structures mathématiques.
  • Partie 3 : quelques lemmes de base sur les réels, qui seront utiles par la suite
  • Partie 4 : suites numériques, résultats généraux, dont une question du partiel d'analyse
  • Partie 5 : une suite définie par récurrence dans l'exercice final de votre devoir d'analyse
La difficulté des exercices est notée entre 0 et 50 selon la même gradation que Donald Knuth dans The Art of Computer Programming. 00 : immédiat 10 : simple (quelques minutes, ou alors vous avez raté une information) 20 : moyennement difficile (entre 15 et 30 minutes) 30 : assez difficile (à faire à la fin si tout est bien compris) 40 : projet (plusieurs heures de travail et des initiatives à prendre) 50 : problème de recherche, non encore résolu
Bien sûr, la difficulté est une notion assez subjective... Essayez d'avoir des jolies preuves courtes et structurées.
Vous utiliserez les tactiques :
  • intros
  • unfold
  • exact
  • split
  • destruct pour : un ∧, un ∨, une preuve de False ou une preuve par cas (sur les entiers naturels ou tout ou autre type inductif)
  • left/right
  • exfalso
  • reflexivity
  • apply et apply ... in
  • rewrite, rewrite <-, rewrite ... in et rewrite <- ... in
  • discriminate
  • induction
  • specialize
  • simpl est autorisé et indispensable dans certains cas très faciles, mais on est toujours content de s'en passer
  • pose proof peut être utile à certains endroits
  • assert
  • remember peut être utile
  • lra, field, ring dans la dernière partie
Il n'est pas du tout nécessaire de traiter tous les exercices pour avoir une bonne note. Vous pouvez toujours admettre un théorème pour l'utiliser plus tard dans le devoir.
Si vous arrivez à traiter quelques exercices bien, vous aurez de toute façon une note correcte.

Partie 1 : Calcul des propositions

Exercice : Prouver le théorème suivant, difficulté 15.

Source : partiel 1 d'initiation aux structures mathématiques, Q1(c)
Lemma imp_and_and_imp : ∀ (P Q R : Prop),
  (P → (Q ∧ R)) ↔ ((P → Q) ∧ (P → R)).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

From Coq Require Import Classical.

Exercice : Prouver le théorème suivant, difficulté 25.

Source : partiel 1 d'initiation aux structures mathématiques, Q4 Note : vous aurez à utiliser le tiers exclu pour prouver le sens →. C'est mieux si vous ne l'utilisez pas dans l'autre sens <-.
Lemma classical_equiv : ∀ (P Q : Prop),
  (P ↔ Q) ↔ ((P ∧ Q) ∨ (¬ P ∧ ¬ Q)).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Partie 2 : un ordre "chelou" sur nat

Dans cette partie, on va traiter une partie de la question 5 du partiel 1 d'initiation aux structures mathématiques. On a besoin du concept de parité, on reprend sa formalisation issue du premier devoir.

Inductive pair_ou_impair :=
| pair : pair_ou_impair
| impair : pair_ou_impair.

On calcule maintenant par récurrence la parité d'un entier naturel n :
  • la parité de 0 est "pair"
  • la parité de 1 est "impair"
  • la parité de n + 2 est la même que la parité de n.

Fixpoint parité (n : nat) :=
match n with
| 0 ⇒ pair
| 1 ⇒ impair
| S (S p) ⇒ parité p
end.

En fait, on ne va se servir que des deux résultats suivants : un entier est soit pair, soit impair.

Lemma nat_pair_ou_impair : ∀ n, parité n = pair ∨ parité n = impair.
Proof.
  intros n.
  destruct (parité n) eqn:parn.
  - left. reflexivity.
  - right. reflexivity.
Qed.

Lemma non_pair_et_impair : ∀ n, ~(parité n = pair ∧ parité n = impair).
Proof. intros n [H H']. rewrite H in H'. discriminate H'. Qed.

Maintenant on définit la relation "<~" (ici appelée le_chelou, où le est l'abbréviation de "less than or equal to") :

Definition le_chelou (x y : nat) :=
  (parité x = pair ∧ parité y = impair) ∨
  (parité x = pair ∧ parité y = pair ∧ x ≤ y) ∨
  (parité x = impair ∧ parité y = impair ∧ y ≤ x).

Notation "x <~ y" := (le_chelou x y) (at level 70).

Intuitivement, on ordonne les naturels de la façon suivante : 0 <~ 2 <~ 4 <~ 6 <~... <~ 9 <~ 7 <~ 5 <~ 3 <~ 1 où dans ..., on trouve tous les entier pairs dans l'ordre croissant, puis les impairs, dans l'ordre décroissant.
On aura besoin de quelques résultats sur nat (qui seront rappelés lorsque c'est nécessaire).
From Coq Require PeanoNat. Import PeanoNat.Nat.

Les 6 résultats suivants permettent de raisonner par cas sur la parité des opérandes de l'ordre <~. Conseils :
  • on prouvera souvent qu'un cas est impossible, lorsqu'on a une hypothèse du type H : pair = impair avec la tactique discriminate H.
  • dans certains cas, il est pratique de faire apparaître la définition de <~, vous pourrez utiliser unfold "<~". et ses variantes avec in.

Exercice : Prouver le théorème suivant, difficulté 15.

Lemma le_chelou_pair_l (x y : nat) : parité x = pair →
  (x <~ y) → ((parité y = pair ∧ x ≤ y) ∨ (parité y = impair)).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Lemma le_chelou_impair_l (x y : nat) : parité x = impair → x <~ y →
  (parité y = impair ∧ y ≤ x).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Lemma le_chelou_pair_pair (x y : nat) : parité x = pair → parité y = pair
  → (x <~ y ↔ x ≤ y).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Lemma le_chelou_impair_impair (x y : nat) :
  parité x = impair → parité y = impair → (x <~ y ↔ y ≤ x).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Lemma le_chelou_pair_impair (x y : nat) :
  parité x = pair → parité y = impair → x <~ y.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Lemma le_chelou_impair_pair (x y : nat) :
  parité x = impair → parité y = pair → ¬ x <~ y.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Quelques applications simples. On traite maintenant la question 5(a) du partiel.
Conseils :
  • D'abord, on peut apply un résultat lorsque la conclusion est une équivalence. En général, apply choisira convenablement le sens de l'équivalence à utiliser.
  • Notre fonction parité est calculatoire. Cela veut dire que Coq sait prouver par un calcul (avec simpl ou reflexivity que parité 5 = impair.
  • On a un petit problème avec ≤ sur nat : il ne sais pas calculer. Une technique courante en Coq est de se ramener à une fonction qui calcule (ici, cette fonction est leb, aussi notée <=? et elle retourne un résultat booléen), puis conclure avec reflexivity ou simpl.
Voici un exemple de telle preuve :
On va utiliser les deux équivalences suivantes :
Check leb_le.
Check leb_nle.
Lemma seven_le_forty_two : 7 ≤ 42.
Proof.
  apply leb_le. (* remarquer l'utilisation de l'équivalence *)
  reflexivity.
Qed.

Lemma forty_two_not_le_seven : ~(42 ≤ 7).
Proof.
  apply leb_nle.
  reflexivity.
Qed.

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma le_chelou_exple1 : 2 <~ 4.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma le_chelou_exple2 : ~(1 <~ 2).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma le_chelou_exple3 : 5 <~ 3.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 10.

Lemma le_chelou_exple4 : 6 <~ 5.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On va maintenant prouver que <~ est bien une relation d'ordre. Faîtes ce que vous pouvez, la réflexivité n'est pas trop pénible, les propriétés suivantes un peu plus. On aura besoin du fait que ≤ est elle-même une relation d'ordre sur nat, donc des trois propriétés suivantes :

Check le_refl.
Check le_antisymm.
Check le_trans.

Exercice : Prouver le théorème suivant, difficulté 20.

Lemma le_chelou_refl (x : nat) : x <~ x.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 30.

Lemma le_chelou_antisymm (x y : nat) : x <~ y → y <~ x → x = y.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 30.

Lemma le_chelou_trans (x y z : nat) : x <~ y → y <~ z → x <~ z.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Pour finir, on va voir que pour cet ordre chelou, nat a à la fois un maximum et un minimum.

Exercice : Prouver le théorème suivant, difficulté 20.

On aura besoin d'un résultat similaire sur ≤ :
Check le_0_l.
Lemma le_chelou_minimum_0 : ∀ n, 0 <~ n.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 20.

Conseil : dans un des cas, faire une preuve par cas sur la nullité de n. On en arrive à devoir prouver quelque chose comme 1 ≤ S n qu'on peut prouver par calcul en se ramenant à leb, comme précédemment.
Lemma le_chelou_maximum_1 : ∀ n, n <~ 1.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Quelques résultats sur les nombres réels

Pour toute la suite, on peut utiliser les résultats habituels sur les nombres réels. On rappellera avant chaque exercice ceux qui sont utilisés dans la correction, mais il y a plusieurs façons de prouver les lemmes donc n'hésitez pas à utiliser d'autres résultats.

From Coq Require Import RIneq Rfunctions.
Open Scope R_scope.

Check R1_neq_R0.
Check Rinv_l.
Check Rinv_lt_contravar.
Check Rinv_r.
Check Rle_antisym.
Check Rle_ge.
Check Rle_refl.
Check Rle_trans.
Check Rlt_asym.
Check Rlt_irrefl.
Check Rlt_trans.
Check Rmult_0_l.
Check Rmult_0_r.
Check Rmult_1_l.
Check Rmult_1_r.
Check Rmult_assoc.
Check Rmult_comm.
Check Rmult_eq_compat_l.
Check Rmult_eq_compat_r.
Check Rmult_eq_reg_l.
Check Rmult_eq_reg_r.
Check Rmult_gt_0_compat.
Check Rmult_le_compat_l.
Check Rmult_le_compat_r.
Check Rmult_le_reg_l.
Check Rmult_le_reg_r.
Check Rmult_lt_compat_l.
Check Rmult_lt_compat_r.
Check Rmult_lt_reg_l.
Check Rmult_lt_reg_r.
Check Rmult_plus_distr_l.
Check Rmult_plus_distr_r.
Check Rplus_0_l.
Check Rplus_0_r.
Check Rplus_assoc.
Check Rplus_comm.
Check Rplus_eq_compat_l.
Check Rplus_eq_compat_r.
Check Rplus_eq_reg_l.
Check Rplus_eq_reg_r.
Check Rplus_le_compat_l.
Check Rplus_le_compat_r.
Check Rplus_le_reg_l.
Check Rplus_le_reg_r.
Check Rplus_lt_compat_l.
Check Rplus_lt_compat_r.
Check Rplus_lt_reg_l.
Check Rplus_lt_reg_r.
Check Rplus_opp_l.
Check Rplus_opp_r.
Check Rlt_0_1.

On voudrait faire un peu d'analyse réelle, mais on aura besoin de quelques résultats manquants sur les réels.

Exercice : Prouver le théorème suivant, difficulté 15.

Le corrigé utilise :
Check Rplus_lt_reg_l.
Check Rplus_assoc.
Check Rplus_opp_l.
Check Rplus_0_l.
Check Rplus_comm.
Lemma Rminus_lt_Rplus (x y z : R) : x - y < z → x < y + z.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Le corrigé utilise :
Check Rmult_le_compat_l.
Check Rmult_0_r.
Lemma Rmult_nneg_npos (x y : R) : 0 ≤ x → y ≤ 0 → x × y ≤ 0.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

Le corrigé utilise :
Check Rnot_lt_le.
Check Rlt_Rminus.
Check Rplus_minus.
Check Rlt_irrefl.
Lemma lt_plus_eps_le (x y : R) : (∀ eps, 0 < eps → x < y + eps) → x ≤ y.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Un peu d'analyse de suites réelles : résultats généraux


From Coq Require Import Lra Lia SeqSeries.

On rappelle les définitions habituelles sur les suites.

Definition croissante (Un : nat → R) := ∀ n, Un n ≤ Un (S n).
Definition décroissante (Un : nat → R) := ∀ n, Un (S n) ≤ Un n.
Definition majorée (Un : nat → R) := ∃ M, ∀ n, Un n ≤ M.
Definition minorée (Un : nat → R) := ∃ m, ∀ n, m ≤ Un n.

À partir de maintenant, vous pouvez utiliser les tactiques automatiques comme
  • lia (égalité et inégalités linéaire sur les entiers),
  • lra (idem sur les réels)
  • field et field_simplify (calculs "évidents" sur un corps, comme les réels)
  • ring et ring_simplify (qui marchent parfois mieux).

Exercice : Prouver le théorème suivant, difficulté 15.

Le corrigé utilise :
Check le_0_r.
Check Rle_refl.
Check le_succ_r.
Check Rle_trans.
Check Rle_refl.
Lemma croissante_croissante (Un : nat → R) : croissante Un →
  ∀ n m, (n ≤ m)%nat → (Un n ≤ Un m).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On rappelle la définition de la convergence d'une suite.
Print Un_cv.

Remarque : Rdist est la distance usuelle sur R
Print Rdist.

On prouve que si une suite (u_n) converge, la suite (u_{n+1} converge vers la même limite.

Exercice : Prouver le théorème suivant, difficulté 15.

Le corrigé utilise :
Check le_S.
Lemma cv_shift (Un : nat → R) (l : R) : Un_cv Un l →
  Un_cv (fun n ⇒ Un (S n)) l.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On prouve que suite croissante qui converge est majorée par sa limite.

Exercice : Prouver le théorème suivant, difficulté 20.

Remarque : ceci est une question du partiel d'analyse. Le corrigé utilise :
Check lt_plus_eps_le.
Check le_refl.
Check Rabs_def2.
Lemma cv_le (Un : nat → R) (l M : R) : Un_cv Un l → (∀ n, Un n ≤ M)
  → l ≤ M.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On aura besoin du résultat suivant qui n'a aucun intérêt mathématique, donc on en laisse la preuve ici.
Lemma cv_eq_compat_l (Un Vn : nat → R) (l : R) :
  Un_cv Vn l → (∀ n, Un n = Vn n) → Un_cv Un l.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 30.

Le corrigé utilise :
Check Req_dec.
Check Rmult_0_l.
Check Rdist_eq.
Check Rabs_pos_lt.
Check Rdiv_lt_0_compat.
Check Rdist_mult_l.
Check Rmult_lt_reg_l.
Check Rinv_0_lt_compat.
Check Rgt_not_eq.
Lemma cv_scalar (Un : nat → R) (l : R) (a : R) :
  Un_cv Un l → Un_cv (fun n ⇒ a × Un n) (a × l).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 15.

On suppose déjà prouvé le théorème suivant :
Check CV_plus.
Le corrigé utilise :
Check cv_scalar.
Check CV_plus.
Check cv_eq_compat_l.
Lemma cv_linear (Un Vn : nat → R) (l1 l2 : R) (a b : R) :
   Un_cv Un l1 → Un_cv Vn l2 →
   Un_cv (fun n ⇒ a × Un n + b × Vn n) (a × l1 + b × l2).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

On a besoin du résultat plus difficile qu'une suite croissante et majorée converge. Celui ci est bien dans la bibliothèque standard mais sous une forme pénible à utiliser. Donc vous pourrez utiliser les théorèmes suivants.
Lemma croissante_majorée_cv (Un : nat → R) : croissante Un → majorée Un →
  ∃ l, Un_cv Un l.
Proof.
  intros Hu Hu'.
  destruct (growing_cv Un Hu) as [l Hl].
  - unfold has_ub, bound, EUn. destruct Hu' as [M HM]. ∃ M.
    unfold is_upper_bound. intros x [i Hi]; rewrite Hi; exact (HM i).
  - ∃ l. exact Hl.
Qed.

Lemma décroissante_minorée_cv (Un : nat → R) : décroissante Un → minorée Un →
  ∃ l, Un_cv Un l.
Proof.
  intros Hu Hu'.
  remember (fun n ⇒ - Un n) as Vn eqn:defV.
  destruct (croissante_majorée_cv Vn) as [l' Hl'].
  - intros n; rewrite defV. apply Ropp_le_contravar. exact (Hu n).
  - destruct Hu' as [m Hm]. ∃ (- m). intros n. rewrite defV.
    apply Ropp_le_contravar. exact (Hm n).
  - ∃ (- l'). apply (cv_eq_compat_l _ (fun n ⇒ - Vn n)).
    + pose proof (cv_scalar _ _ (- 1) Hl') as Hm1.
      replace (-1 × l') with (- l') in Hm1 by ring.
      apply cv_eq_compat_l with (1 := Hm1). intros n. ring.
    + intros n. rewrite defV. rewrite Ropp_involutive. reflexivity.
Qed.

Une suite définie par récurrence

Enfin, on voudrait traiter le dernier exercice du partiel d'analyse.
Section Exercice6.

On se donne un réel u0 entre 0 et 1 :
Context (u0 : R) (Hu0 : 0 < u0 ≤ 1).

Et la suite u_ définie par récurrence de la façon suivante :
Let u_ := fix U n :=
  match n with
  | 0 ⇒ u0
  | S p ⇒ U p × / 2 + (U p) × (U p) × / 4
  end.

Pour faciliter les réécritures et se passer de simpl, on utilise les deux outils suivants :
Lemma u_0 : u_ 0 = u0. Proof. reflexivity. Qed.
Lemma u_succ (n : nat) : u_ (S n) = u_ n × / 2 + u_ n × u_ n × / 4.
Proof. reflexivity. Qed.

Exercice : Prouver le théorème suivant, difficulté 25.

On prouve maintenant que u_ est bornée. Cela se fait (de façon plus ou moins agréable) par récurrence. Le corrigé utilise remember (u_ n × u_ n) as x eqn:def_x. pour se débarrasser d'un terme non linéaire qui empêche lra d'avancer.
Lemma u_bornée : ∀ n, 0 < u_ n ≤ 1.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 20.

Le corrigé utilise les tactiques field et lra, ainsi que :
Check Rminus_le.
Check Rmult_nneg_npos.
Lemma u_décroissante : décroissante u_.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant, difficulté 40.

Bon franchement, si vous arrivez à prouver le théorème suivant, vous êtes très très forts... Le corrigé utilise une bonne partie des lemmes prouvés dans ce devoir et lra, field, field_simplify. N'hésitez pas à utiliser assert pour structurer la preuve et pose proof pour avoir sous la main les résultats utiles. Le corrigé (28 lignes assez denses) utilise :
Check u_bornée.
Check décroissante_minorée_cv.
Check cv_shift.
Check CV_mult.
Check cv_linear.
Check cv_eq_compat_l.
Check UL_sequence. (* unicité de la limite *)
Check cv_le.
Check Req_dec.
Check Rmult_eq_compat_l.
Check Rinv_l.
Check Rmult_plus_distr_l.
Lemma u_cv_0 : Un_cv u_ 0.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

End Exercice6.