Rattrapage Initiation aux preuves formelles 2024 -- 2025
- logique propositionnelle
- calcul des prédicats (sans tiers-exclus)
- entiers naturels et induction
- intros, exact, reflexivity, split, left, right
- destruct pour détruire une preuve de ∨, de ∧, de ∃ ou un raisonnement par cas sur la nullité d'un nat
- exfalso
- apply, apply ... in ..., apply ... in ... as ...
- rewrite, rewrite ... in
- specialize
- injection, discriminate
- induction
- assert, pose proof
Section LogiqueProp.
Context (P Q R : Prop).
Lemma ex1 : (P → Q → R) → (P → Q) → P → R.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex2 : P ∧ Q → Q ∧ P.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex3 : ¬ (P ∧ ¬ P).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex4 : P → ~~ P.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex5 : ∃ (A : Prop), ∀ (B : Prop), A → B.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex6 : (P → R) → (Q → R) → (P ∨ Q) → R.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
End LogiqueProp.
Section Predicats.
Context (P Q R : Prop).
Lemma ex1 : (P → Q → R) → (P → Q) → P → R.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex2 : P ∧ Q → Q ∧ P.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex3 : ¬ (P ∧ ¬ P).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex4 : P → ~~ P.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex5 : ∃ (A : Prop), ∀ (B : Prop), A → B.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex6 : (P → R) → (Q → R) → (P ∨ Q) → R.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
End LogiqueProp.
Section Predicats.
Dans toute cette section, t désigne un type quelconque,
P et Q sont deux prédicats sur ce type, c'est à dire des
fonctions de type t → Prop.
On suppose aussi qu'il existe un élément x0 de type t (le
type t est supposé habité, c'est-à-dire non vide).
Context {t : Type} (P : t → Prop) (Q : t → Prop) (x0 : t).
Check x0.
Lemma ex7 : (∀ x, P x) → ∃ x, P x.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex8 : (∃ x, (P x) ∨ (Q x)) ↔
(∃ x, (P x)) ∨ (∃ y, (Q y)).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma ex9 : (∃ x, ∀ y, (P x → Q y)) →
∀ y, ∃ x, (P x → Q y).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
End Predicats.
Create HintDb ipf.
Section Naturels.
Ne pas lire : passage technique hors-programme du cours
Import PeanoNat.Nat(add_0_l, add_succ_l, mul_0_l, mul_0_r, mul_succ_l,
mul_succ_r).
Hint Rewrite add_0_l add_succ_l : ipf.
mul_succ_r).
Hint Rewrite add_0_l add_succ_l : ipf.
Dans toute cette section, on pourra à tout moment utiliser la commande
suivante pour afficher les lemmes autorisés.
Print Rewrite HintDb ipf.
Pour le moment, on suppose seulement connus les lemmes suivants:
Check add_succ_l.
Check add_0_l.
Lemma ex10 : ∃ n, n + n = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma add_0_r : ∀ n, n + 0 = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Check add_0_l.
Lemma ex10 : ∃ n, n + n = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma add_0_r : ∀ n, n + 0 = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
On rajoute add_0_r à la liste des lemmes autorisés.
Hint Rewrite add_0_r : ipf.
Print Rewrite HintDb ipf.
Lemma add_succ_r : ∀ n m, n + S m = S (n + m).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Print Rewrite HintDb ipf.
Lemma add_succ_r : ∀ n m, n + S m = S (n + m).
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
On rajoute add_succ_r à la liste des lemmes autorisés.
Hint Rewrite add_succ_r : ipf.
Print Rewrite HintDb ipf.
Lemma add_comm : ∀ n m, n + m = m + n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Print Rewrite HintDb ipf.
Lemma add_comm : ∀ n m, n + m = m + n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
On rajoute add_comm à la liste des lemmes autorisés.
On rajoute quelques lemmes sur la multiplication à la
liste des lemmes autorisés.
Indice : rappelez vous que 1 n'est qu'une notation pour S 0.
Lemma mul_1_r : ∀ n : nat, n × 1 = n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma add_diag : ∀ n : nat, n + n = 2 × n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma add_diag : ∀ n : nat, n + n = 2 × n.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Pour le lemme suivant, petit rappel :
la tactique injection permet de simplifier une égalité lorsqu'elle
est de type C n = C m, où C est un constructeur.
Voir l'exemple suivant :
Example ex_injection : ∀ n m : nat, S n = S m → n = m.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Lemma add_cancel_l : ∀ n m p : nat, p + n = p + m → n = m.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Hint Rewrite add_cancel_l : ipf.
Lemma add_cancel_r : ∀ n m p : nat, n + p = m + p → n = m.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Hint Rewrite add_cancel_l : ipf.
Lemma mul_eq_0 : ∀ (n m : nat), n × m = 0 → n = 0 ∨ m = 0.
Proof.
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Hint Rewrite mul_eq_0 : ipf.
Hint Rewrite eq_sym f_equal : ipf.
Pour ce dernier exercice (difficile), on ajoute à la liste des lemmes
autorisés :
Check eq_sym.
Check f_equal.
Lemma mul_cancel_l : ∀ n m p, p ≠ 0 → p × n = p × m → n = m.
Proof.
(* On vous donne la bonne hypothèse d'induction ci-dessous : *)
intros n m. revert n. induction m as [| m IH]; intros n p Hp.
(* À vous *)
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Hint Rewrite mul_cancel_l : ipf.
End Naturels.
Check f_equal.
Lemma mul_cancel_l : ∀ n m p, p ≠ 0 → p × n = p × m → n = m.
Proof.
(* On vous donne la bonne hypothèse d'induction ci-dessous : *)
intros n m. revert n. induction m as [| m IH]; intros n p Hp.
(* À vous *)
(* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)
Hint Rewrite mul_cancel_l : ipf.
End Naturels.