Require Import Unicode.Utf8. (* sorties plus jolies *)

Équivalence ↔

Locate "<->".
Print iff.
L'équivalence logique est notée en coq ↔. Une preuve de P ↔ Q est à la fois une preuve de P → Q et une preuve de Q → R. Les tactiques destruct (pour utiliser une équivalence) et split (pour prouver une équivalence) s'appliquent de la même manière que pour la conjonction.

Theorem iff_sym : ∀ P Q : Prop, P ↔ Q → Q ↔ P.
Proof.
  (* Soient P et Q deux propositions quelconques. *)
  intros P Q.
  (* On suppose (H) : P <-> Q. *)
  intros H.
  (* De (H) on déduit :
     (HPQ) : P -> Q
     (HQP) : Q -> P *)
  destruct H as [HPQ HQP].
  (* Pour prouver P <-> Q, il suffit de prouver P -> Q et Q -> P. *)
  split.
  - (* Preuve de P -> Q : *)
    assumption.
  - (* Preuve de Q -> P : *)
    assumption.
Qed.

Exercice : Prouver le théorème suivant.


Theorem iff_refl : ∀ P : Prop, P ↔ P.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.


Theorem iff_trans : ∀ P Q R : Prop, (P ↔ Q) → (Q ↔ R) → (P ↔ R).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)


Lois de de Morgan

Les "lois" de de Morgan sont un résultat très connu (et très utile !) de logique classique. Que se passe-t-il en logique intuitionniste ?

Exercice : Prouver le théorème suivant.


Theorem de_morgan_not_or : ∀ P Q : Prop, ~(P ∨ Q) ↔ (¬ P) ∧ (¬ Q).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.


Theorem de_morgan_not_or_not : ∀ P Q : Prop, (¬ P) ∨ (¬ Q) → ¬ (P ∧ Q).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Remarquez qu'on ne vous a demandé qu'une seule implication dans l'exercice précédent... C'est parce que l'autre n'est tout simplement pas prouvable en logique intuitionniste.

Exercice :

En essayant de prouver le théorème suivant, se convaincre que ce n'est pas possible.
Theorem de_morgan_not_and : ∀ P Q : Prop, ¬ (P ∧ Q) → (¬ P) ∨ (¬ Q).
Proof.
  (* Essayez d'aller le plus loin possible dans la preuve. *)
Abort.

Logique intuitionniste et logique classique

La différence avec votre cours de mathématiques classiques est que coq n'est pas équipé par défaut du tiers exclu qui dit qu'une proposition est soit vraie, soit fausse. En pratique, cela veut dire pour les inconvénients :
  • pas de preuve par l'absurde
  • pas de raisonnement par contraposition
mais il y a un gros avantage à cela : les preuves sont constructives.
Peut-on ajouter le tiers-exclus à coq pour prouver les mêmes théorèmes qu'en mathématiques ?

Axiom excluded_middle : ∀ P : Prop, P ∨ ¬ P.

Attention ! Un axiome n'est pas un théorème ! En ajoutant un axiome on prend le risque (énorme) que tout s'écroule ! Un théorème difficile montre que si coq est correct (c'est-à-dire ne permet pas de prouver quelque chose de faux), alors (coq + tiers-exclus) est aussi correct. On peut donc, si on le souhaite ajouter l'axiome du tiers-exclus.
Avec cet axiome, on peut prouver, par exemple, que le raisonnement par l'absurde est correct.

Theorem NNPP : ∀ P : Prop, ¬ ¬ P → P.
Proof.
  (* Soit P une proposition quelconque. *)
  intros P. unfold not.
  (* On suppose (hyp. (H)) que P est non contradictoire. *)
  intros H.
  (* Par le principe du tiers-exclus appliqué à P, on a
     (HP) : P
     ou
     (HnP) : ~ P *)
  destruct (excluded_middle P) as [HP | HnP].
  - (* cas 1 : (HP) *)
  assumption.
  - (* cas 2 : (HnP) *)
  (* On va ici utiliser le principe d'explosion : ce cas est contradictoire. *)
  exfalso.
  unfold not in HnP.
  apply H.
  assumption.
Qed.

Remarquer destruct (excluded_middle P) as [HP | HnP].. Ici, excluded_middle est un axiome qui prend une proposition en argument et (excluded_middle P) est une preuve de (P ∨ ¬P). Avec destruct, on peut donc la détruire et faire une preuve par cas.

Exercice :

En utilisant le tiers-exclus ou l'une de ses conséquences, prouver le théorème suivant :

Theorem de_morgan_not_and : ∀ P Q : Prop, ¬ (P ∧ Q) → (¬ P) ∨ (¬ Q).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Remarque :
  • les trois autres lois de de Morgan sont prouvables en logique intuitionniste.
  • celle-ci ne l'est pas, on a absolument besoin du tiers exclu.

Theorem classical_imp : ∀ P Q : Prop, (P → Q) ↔ (Q ∨ ¬ P).
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)


Exercice :

En utilisant le tiers-exclus ou l'une de ses conséquences, prouver le théorème suivant :

Theorem Peirce_law : ∀ P Q : Prop, ((P → Q) → P) → P.
Proof.
  (* Remplir la preuve ici *)
Admitted. (* Remplacer cette ligne par Qed. *)

Remarque :
  • les trois autres lois de de Morgan sont prouvables en logique intuitionniste.
  • celle-ci ne l'est pas, on a absolument besoin du tiers exclu.
Pour terminer cette partie sur la logique classique. Il y a bien des théorème qu'on peut démontrer en logique classique et pas en logique intuitionniste. Ceci dit, une preuve dite "constructive", c'est-à-dire en logique intuitionniste, lorsqu'elle est possible, apporte toujours plus d'informations qu'une preuve non constructive. Les preuves par l'absurde peuvent très souvent (même dans les preuves de mathématiciens professionnels) être remplacées par des preuves plus simples et plus parlantes. Dans vos études de mathématiques, vous devriez éviter de vous jeter dessus.