Rattrapage Initiation aux preuves formelles 2024 -- 2025

Ce sujet comporte 3 parties :
  • logique propositionnelle
  • calcul des prédicats (sans tiers-exclus)
  • entiers naturels et induction
Dans les deux premières parties, aucun lemme n'est nécessaire. Dans la troisième partie, les lemmes nécessaires sont rappelés et les lemmes prouvés précédemment sont disponibles dans les questions suivantes.
Les tactiques autorisées sont :
  • 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
Si vous voulez, pour gagner du temps, vous pouvez utiliser des "intro patterns" comme intros [H1 H2] [H | H] [x Hx]... mais ce n'est jamais strictement nécessaire.

From Coq Require Import PeanoNat.
Set Keyed Unification.

Logique

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.

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.

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. *)

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. *)

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. *)

On rajoute add_comm à la liste des lemmes autorisés.
Hint Rewrite add_comm : ipf.
Print Rewrite HintDb ipf.

On rajoute quelques lemmes sur la multiplication à la liste des lemmes autorisés.

Hint Rewrite mul_succ_l mul_succ_r mul_0_l mul_0_r : ipf.
Print Rewrite HintDb ipf.

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. *)

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.