Logique intuitionniste en Coq
La flèche ou implication
Type Prop et →
L'objet fondamental du système Coq est le type (on dit qu'il est basé sur la théorie des types). Tous les objets que l'on manipule ont un certain type. Le type Prop est celui des propositions, c'est-à-dire des énoncés mathématiques que l'on peut chercher à prouver ou à réfuter.coqide
) ou Alt+↓
(si vous utilisez la version web) pour faire interpréter
la prochaine ligne à Coq. Voir le résultat dans la fenêtre en bas à droite.
Les énoncés 2 + 2 = 4 et 2 + 2 = 5 sont tous deux de type Prop,
peu importe qu'ils soient prouvables ou non.
Étant données deux propositions P et Q, on peut en former une nouvelle,
P → Q (lire : « P flèche Q » ou « P implique Q »).
Intuituivement, dans la logique de Coq,
la proposition P → Q signifie « si P, alors Q » ou, plus précisément,
« je sais contruire une preuve de Q à partir d'une preuve de P. »
Deux remarques importantes :
Nous allons maintenant énoncer et prouver un premier théorème. Exécuter pas
à pas cette preuve pour bien voir les modifications dans le contexte et le
but.
En Coq, les commentaires sont écrits entre
Ce premier théorème énonce que, quelle que soit la proposition P, on a
P → P. Cela peut paraître évident, mais en Coq il faut tout prouver !
- La notation usuelle des mathématiques pour « P implique Q » est P ⇒ Q. Continuez à l'utilisez lors de vos cours plus classiques de mathématiques.
- En logique classique (voir plus loin) et en particulier dans vos cours de mathématiques, l'implication est définie par sa table de vérité et a un sens un peu différent.
- Ce qui différencie la logique « de base », dite « intuitionniste » de Coq de celle apprise en mathématiques est qu'on ne dispose pas du tiers-exclus (qui dit que pour toute proposition A, A est soit vraie, soit fausse). Ceci dit, toutes les formules et techniques de preuves que nous voyons dans ce cours sont encore valides dans un cours de mathématiques classique.
Première preuve
(* ... *)
.
Ici, comme à beaucoup d'autres endroites de ce cours, ils sont destinés à
vous montrer la preuve « mathématique » très détaillée correspondant à la
preuve en Coq.
Theorem imp_refl : ∀ P : Prop, P → P.
Proof.
(* Soit P une proposition quelconque. *)
intros P.
(* Pour montrer une implication on suppose que ce qui est à gauche est prouvé.
On doit prouver ce qui est à droite avec cette hypothèse supplémentaire. *)
(* On suppose (hypothèse (H)) que P est prouvée. *)
intros H.
(* On doit prouver P, or (H) prouve exactement P. *)
exact H.
Qed. (* Quod erat demonstrandum. Ce qu'il fallait démontrer. *)
Proof.
(* Soit P une proposition quelconque. *)
intros P.
(* Pour montrer une implication on suppose que ce qui est à gauche est prouvé.
On doit prouver ce qui est à droite avec cette hypothèse supplémentaire. *)
(* On suppose (hypothèse (H)) que P est prouvée. *)
intros H.
(* On doit prouver P, or (H) prouve exactement P. *)
exact H.
Qed. (* Quod erat demonstrandum. Ce qu'il fallait démontrer. *)
Sans entrer dans tous les détails, quelques commentaires s'imposent :
Pour pouvoir passer à la suite, il faut avoir vraiment bien compris que
- imp_refl est le nom que nous avons choisi pour ce théorème.
- La preuve se trouve entre les mots-clés Proof. et Qed.
- Lorsque vous avez fait interpréter à Coq la ligne Proof., vous avez vu apparaître en haut à droite de l'écran une fenêtre qui décrit l'état de la preuve.
- Cet état contient deux parties séparées par une ligne horizontale. En-dessous de cette ligne se trouve le but : c'est ce qu'il faut démontrer. Au-dessus de cette ligne se trouve le contexte : un ensemble de variables et d'hypothèses qu'on peut utiliser pour prouver le but.
- Les éléments de la preuve intros et exact sont appelés des tactiques de preuve. Ils font évoluer l'état de la preuve.
- Lorsque l'évaluation par Coq atteint Qed., Coq vérifie que la preuve est correcte et dans le cas contraire affiche un message d'erreur.
- Petit point de syntaxe : en Coq, les commandes et les tactiques se terminent toujours par un point.
- intros nom_de_variable. introduit une nouvelle variable dans le contexte
en supprimant un quantificateur universel (un « pour tout » en français,
forall
en Coq ou le symbole ∀). - intros nom_d_hypothese. introduit une nouvelle hypothèse dans le contexte en supprimant la première implication, à gauche, du but.
- exact nom_d_hypothese. dit que l'hypothèse nom_d_hypothese est une preuve du but.
Exercice : à vous de remplir la preuve suivante !
Lorsque Coq vous indique que la preuve est terminée, vous devez remplacer la ligne Admitted. par Qed.. C'est vraiment facile, on veut juste s'assurer que vous avez compris la preuve précédente et mémorisé ses tactiques.Plusieurs flèches à la suite
L'implication n'est pas associative, ce qui veut dire que (P → Q) → R n'est pas équivalente à P → (Q → R), ces deux propositions ont des sens très différents. En Coq, lorsqu'on ne met pas de parenthèses dans une expression avec des →, c'est comme s'il y en avait à droite : P → Q → R est la même proposition que P → (Q → R).Exercice : Prouver le théorème suivant.
Theorem imp_ex1 : ∀ P Q : Prop, P → (Q → P).
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons (hypothèse (H)) que P est prouvée. *)
intros H.
(* Supposons (hypothèse (H')) que Q est prouvée. *)
intros H'.
(* Il reste à prouver P, ce qui est donné par H. *)
exact H.
Qed.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons (hypothèse (H)) que P est prouvée. *)
intros H.
(* Supposons (hypothèse (H')) que Q est prouvée. *)
intros H'.
(* Il reste à prouver P, ce qui est donné par H. *)
exact H.
Qed.
Theorem imp_ex2 : ∀ P Q : Prop, Q → (P → P).
Proof.
(* Soient P et Q deux propositions. *)
intros P Q.
(* Supposons (hypothèse (H)) que Q est prouvée. *)
intros H.
(* Supposons (hypothèse (H')) que P est prouvée. *)
intros H'.
(* Il reste à prouver P, or P est prouvée par hypothèse. *)
exact H'.
Qed.
Remarque importante :
Après avoir introduit toutes les variables et toutes les hypothèses dans ces
deux derniers exercices, les contextes sont exactement les mêmes. En fait,
plutôt que de penser à P → Q → R comme (P implique que (Q implique
R)), il vaut mieux y voir « si P et Q, alors R », ou encore, « si
j'ai une preuve de P et une preuve de Q, alors je sais contruire une
preuve de R ».
Appliquer une implication
Maintenant qu'on a vu comment prouver (introduire) une implication, on va voir comment on utilise (élimine, applique) une implication.Theorem modus_ponens : ∀ P Q : Prop, P → (P → Q) → Q.
Proof. (* Démonstration. *)
(* Soient P et Q deux propositions quelconques.*)
intros P Q.
(* Supposons (hypothèse (H)) que P est prouvée ... *)
intros H.
(* ... et (hypothèse (H')) que (P → Q) est prouvée. *)
intros H'.
(* Comme, d'après H', (P → Q) est prouvée,
pour montrer Q _il suffit_ de montrer P. *)
apply H'.
(* Or, P est prouvée par l'hypothèse H. *)
exact H.
Qed. (* CQFD. *)
Revenons sur la tactique apply.
Si la formule à prouver est Q et qu'une hypothèse H a la forme
P → Q, alors l'utilisation de apply H. entraîne le changement du but en
P.
Ceci est conforme à la règle appelée syllogisme ou modus ponens qui dit
que de P → Q et P, on peut déduire Q.
Pour passer à la suite, vous devez vraiment avoir compris comme la tactique
apply agit sur le but, si besoin en exécutant de nouveau la preuve
précédente.
- Socrate est un homme. (P)
- Tous les hommes sont mortels. (P → Q)
- Donc Socrate est mortel. (Q)
Exercice : Prouver le théorème suivant.
Theorem imp_trans : ∀ P Q R : Prop,
(P → Q) → (Q → R) → (P → R).
Proof.
(* Soient P, Q et R trois propositions. *)
intros P Q R.
(* Supposons (hypothèse (H)) que P → Q. *)
intros H.
(* Supposons (hypothèse (H')) que Q → R. *)
intros H'.
(* Supposons (hypothèse (K)) que P est prouvée. *)
intros K.
(* Remarque pour aller plus vite la prochaine fois :
intros P Q R H H' K. *)
(* Pour prouver R, d'après H' il suffit de prouver Q. *)
apply H'.
(* Pour prouver Q, d'après H, il suffit de prouver P. *)
apply H.
(* Or, P est prouvée par l'hypothèse K. *)
exact K.
Qed.
Les sous-buts
Theorem imp3 : ∀ P Q R : Prop,
(P → Q → R) → P → Q → R.
Proof.
(* Soient P, Q et R trois propositions quelconques. *)
intros P Q R.
(* Supposons :
(H) : P → Q → R
(H1) : P
(H2) : Q *)
intros H H1 H2.
(* D'après (H), pour prouver R il suffit d'avoir une preuve de P et une
preuve de Q. *)
apply H.
(* Remarquer les deux sous-buts ici ! *)
(* On peut utiliser les caractères - + et *
pour mettre en évidence le fait qu'on travaille sur un sous-but *)
- (* Preuve de P: *)
exact H1.
- (* Preuve de Q: *)
exact H2.
Qed.
Theorem premisses_non_ordonnées1 : ∀ P Q R : Prop, (P → Q → R) → (Q → P → R).
Proof.
intros P Q R H.
intros H1 H2.
apply H.
- exact H2.
- exact H1.
Qed.
Theorem imp_trans2 : ∀ P Q R S : Prop,
(P → Q) → (Q → R) → (R → S) → P → S.
Proof.
(* Soient P, Q, R et S des propositions quelconques *)
intros P Q R S.
(* On suppose prouvées
(H1) : P → Q
(H2) : Q → R
(H3) : R → S
(H) : P
et on doit montrer S.*)
intros H1 H2 H3 H.
(* D'après H3, pour prouver S il suffit de prouver R. *)
apply H3.
(* D'après H2, pour prouver R il suffit de prouver Q. *)
apply H2.
(* D'après H1, pour prouver Q il suffit de prouver P. *)
apply H1.
(* Or, P est prouvée par l'hypothèse H. *)
exact H.
Qed.
(P → Q) → (Q → R) → (R → S) → P → S.
Proof.
(* Soient P, Q, R et S des propositions quelconques *)
intros P Q R S.
(* On suppose prouvées
(H1) : P → Q
(H2) : Q → R
(H3) : R → S
(H) : P
et on doit montrer S.*)
intros H1 H2 H3 H.
(* D'après H3, pour prouver S il suffit de prouver R. *)
apply H3.
(* D'après H2, pour prouver R il suffit de prouver Q. *)
apply H2.
(* D'après H1, pour prouver Q il suffit de prouver P. *)
apply H1.
(* Or, P est prouvée par l'hypothèse H. *)
exact H.
Qed.
Conjonction ∧
Utiliser une conjonction : destruct
Theorem proj1 : ∀ P Q : Prop, P ∧ Q → P.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∧ Q *)
intros H.
(* De H on déduit :
(H) : P
(H') : Q *)
destruct H as [H H'].
(* Alors P est prouvée par l'hypothèse H. *)
exact H.
Qed.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∧ Q *)
intros H.
(* De H on déduit :
(H) : P
(H') : Q *)
destruct H as [H H'].
(* Alors P est prouvée par l'hypothèse H. *)
exact H.
Qed.
Noter la syntaxe avec crochets pour destruct une proposition conjonctive :
la tactique destruct H as [H1 H2] a détruit l'hypothèse H
(elle n'est plus présente dans le contexte) et a ajouté les deux nouvelles
hypothèses H1 et H2, qui sont, respectivement une preuve de P et
une preuve de Q.
Exercice : Prouver le théorème suivant.
Theorem proj2 : ∀ P Q : Prop, P ∧ Q → Q.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∧ Q. *)
intros H.
(* De H on déduit :
(H1) : P
(H2) : Q *)
destruct H as [H1 H2].
(* Alors Q est prouvée par l'hypothèse H2. *)
exact H2.
Qed.
Les « intro patterns »
Les preuves pouvant être longues, les concepteurs de Coq essaient continuellement de nous faciliter la tâche avec des constructions qui font gagner du temps. Les intro pattern sont des transformations que l'on peut faire dès l'introduction de nouvelles hypothèses. Ici, au lieu d'écrire intros H suivi directement de destruct H as [H1 H2] il est possible d'écrire simplement intros [H1 H2] et l'hypothèse est directement introduite et détruite. La preuve de proj1 peut donc s'écrire en deux tactiques :Prouver une conjonction : split
Theorem conj : ∀ P Q : Prop, P → Q → P ∧ Q.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons :
(H1) : P
(H2) : Q. *)
intros H1 H2.
(* Pour prouver P ∧ Q on doit prouver P puis Q. *)
split. (* Remarquer l'apparition de 2 sous-buts. *)
- (* Preuve de P : *)
(* P est prouvée par l'hypothèse H1. *)
exact H1.
- (* Preuve de Q : *)
(* Q est prouvée par l'hypothèse H2. *)
exact H2.
Qed.
Theorem and_comm1 : ∀ P Q : Prop, P ∧ Q → Q ∧ P.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∧ Q *)
intros H.
(* De H on déduit :
(H1) : P
(H2) : Q *)
destruct H as [H1 H2].
(* Pour prouver Q ∧ P on doit prouver Q puis P. *)
split.
- (* Preuve de Q : *)
(* Q est prouvée par l'hypothèse H2. *)
exact H2.
- (* Preuve de P : *)
(* P est prouvée par l'hypothèse H1. *)
exact H1.
Qed.
Remarque : comme pour → l'opérateur ∧ est "associatif à droite" en Coq,
ce qui signifie que P ∧ Q ∧ R dénote en fait P ∧ (Q ∧ R).
Comme on va le voir ci-dessous, ceci n'a pas tellement d'importance ici.
Exercice : Prouver le théorème suivant.
Theorem and_assoc1 : ∀ P Q R : Prop, (P ∧ Q) ∧ R → P ∧ Q ∧ R.
Proof.
intros P Q R [[H1 H2] H3].
split.
- (* Preuve de P : *)
exact H1.
- (* Preuve de Q ∧ R *)
split.
+ (* Preuve de Q : *)
exact H2.
+ (* Preuve de R : *)
exact H3.
Qed.
Theorem and_assoc2 : ∀ P Q R : Prop, P ∧ Q ∧ R → (P ∧ Q) ∧ R.
Proof.
intros P Q R [H1 [H2 H3]].
split.
- (* Preuve de P ∧ Q : *)
split.
+ (* Preuve de P : *)
exact H1.
+ (* Preuve de Q : *)
exact H2.
- (* Preuve de R : *)
exact H3.
Qed.
Disjonction ∨
Prouver une disjonction : left et right
Theorem or_introl : ∀ P Q : Prop, P → P ∨ Q.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P *)
intros H.
(* Pour prouver P ∨ Q il suffit de prouver P. *)
left.
(* Or P est vraie par l'hypothèse H. *)
exact H.
Qed.
Attention : Le fait de choisir left ou right est en général important
et doit être fait le plus tard possible (lorsque vous avez tous les éléments
pour choisir). Si vous vous sentez bloqué dans la preuve, il peut être
intéressant de revenir en arrière et d'essayer de prouver l'autre côté.
Exercice : Prouver le théorème suivant.
Theorem or_intror : ∀ P Q : Prop, Q → P ∨ Q.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : Q *)
intros H.
(* Pour prouver P ∨ Q il suffit de prouver Q. *)
right.
(* Or Q est vraie par l'hypothèse H. *)
assumption.
Qed.
Theorem and_imp_or : ∀ P Q : Prop, P ∧ Q → P ∨ Q.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∧ Q. *)
intros H.
(* De H on déduit :
(H1) : P
(H2) : Q *)
destruct H as [H1 H2].
(* On a l'embarras du choix. *)
(* Pour prouver P ∨ Q il suffit de prouver P. *)
left.
(* Or P est vrai par l'hypothèse H1. *)
exact H1.
Qed.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∧ Q. *)
intros H.
(* De H on déduit :
(H1) : P
(H2) : Q *)
destruct H as [H1 H2].
(* On a l'embarras du choix. *)
(* Pour prouver P ∨ Q il suffit de prouver P. *)
left.
(* Or P est vrai par l'hypothèse H1. *)
exact H1.
Qed.
Utiliser une disjonction : destruct
- Dans un premier temps, on prouve le but sous l'hypothèse que l'opérande de gauche (ici P) est prouvée.
- Dans un second temps, on prouve le but sous l'hypothèse que l'opérande de droite (ici Q) est prouvée.
Theorem or_comm1 : ∀ P Q : Prop, P ∨ Q → Q ∨ P.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* Supposons
(H) : P ∨ Q. *)
intros H.
(* De (H) on déduit
(H1) : P
ou
(H2) : Q *)
destruct H as [H1 | H2].
(* Noter beaucoup de choses ici :
- la syntaxe avec la barre verticale dans les crochets pour le « ou »
- il y a maintenant deux sous-buts, un par cas. En fait ce ne sont pas les
buts qui diffèrent, mais les contextes (hypothèses). *)
- (* cas 1 : sous l'hypothèse (H1) que P est prouvée *)
right.
exact H1.
- (* cas 2 : sous l'hypothèse (H2) que Q est prouvée *)
left.
exact H2.
Qed.
Theorem or_ind : ∀ P Q R: Prop, (P → R) → (Q → R) → P ∨ Q → R.
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q R.
(* Supposons
(H1) : P → Q
(H2) : Q → R
(H) : P ∨ Q. *)
intros H1 H2 H.
(* De (H) on déduit que P est prouvée (hyp. (K)) ou
que Q est prouvée (hyp. (L). *)
destruct H as [K | L].
- (* cas 1 : hyp. (H1) *)
apply H1.
exact K.
- (* cas 2 : hyp. (H2) *)
apply H2.
exact L.
Qed.
De la même manière que pour ∧, on peut utiliser un « intro pattern »
pour détruire une disjonction directement.
Theorem or_comm1' : ∀ P Q : Prop, P ∨ Q → Q ∨ P.
Proof.
intros P Q [H1 | H2].
- right.
exact H1.
- left.
exact H2.
Qed.
Proof.
intros P Q [H1 | H2].
- right.
exact H1.
- left.
exact H2.
Qed.
On peut même mettre des « intro patterns » dans des « intro patterns »
Theorem or_and_dist : ∀ P Q R : Prop, P ∨ (Q ∧ R) → (P ∨ Q) ∧ (P ∨ R).
Proof.
intros P Q R [H1 | [H2 H3]].
(* À vous de terminer ! *)
- split.
+ left. exact H1.
+ left. exact H1.
- split.
+ right. exact H2.
+ right. exact H3.
Qed.
Proof.
intros P Q R [H1 | [H2 H3]].
(* À vous de terminer ! *)
- split.
+ left. exact H1.
+ left. exact H1.
- split.
+ right. exact H2.
+ right. exact H3.
Qed.
Négation ¬
La proposition False
La proposition False
désigne le faux, l'absurde, souvent notée en mathématiques ⊥
(symbole bottom). Elle est définie par la règle appelée ex falso quod
libet (du faux, on peut déduire n'importe quoi), aussi appelée principe
d'explosion.
Si False est dans les hypothèses, alors la tactique destruct appliquée à
celle-ci permet simplement de terminer la preuve.
Theorem ex_falso_quod_libet : ∀ P : Prop, False → P.
Proof.
(* Soit P une proposition quelconque. *)
intros P.
(* Supposons (hypothèse (H)) que False est prouvée. *)
intros H.
(* Explosion : le faux fait partie des hypothèses, tout est prouvé. *)
destruct H.
Qed.
Theorem exo_false : ∀ P Q : Prop,
P → False → (P → P) → (Q → P → P) → (Q → Q → P) → P → Q.
Proof.
intros P Q H' H.
destruct H.
Qed.
La tactique exfalso remplace le but courant par False.
En effet, si l'on prouve False on prouve tout de toute façon.
Theorem stupide : ∀ P Q : Prop, (P → False) → P → (Q → P → Q).
Proof.
(* Soient P et Q deux propositions quelconques. *)
intros P Q.
(* On suppose
(H1) : P → False
(H2) : P *)
intros H1 H2.
(* Comme False implique n'importe quoi, il suffit de prouver False. *)
exfalso. (* Remarquer que le but a été simplement changé en False. *)
(* Par H1 il suffit de prouver P. *)
apply H1.
(* Or P est vrai par hypothèse. *)
exact H2.
Qed.
Theorem P_et_P_imp_False : ∀ P Q : Prop, P ∧ (P → False) → Q.
Proof.
intros P Q [H H'].
exfalso.
apply H'.
exact H.
Qed.
Proof.
intros P Q [H H'].
exfalso.
apply H'.
exact H.
Qed.
Réfuter une proposition
En logique intuitionniste, plutôt que de dire qu'une proposition est fausse, on dit qu'elle est contradictoire, ce qui signifie qu'ajouter cette proposition dans les hypothèse mène à une explosion : une preuve de False (et donc, par ex falso quod libet de toutes les propositions).
On peut déplier une notation, c'est-à-dire la remplacer par ce qu'elle
représente avec la tactique unfold (littéralement « déplier »).
Theorem exemples_unfold : ∀ A B C : Prop, ¬A → ¬B → ¬C → ¬A ∧ ¬C.
Proof.
intros A B C H1 H2 H3.
(* On peut préciser dans quelle hypothèse on souhaite déplier. *)
unfold not in H1.
(* Éventuellement, dans plusieurs hypothèses d'un coup. *)
unfold not in H2, H3.
(* Si on ne précise rien, c'est dans le but. *)
unfold not.
(* Fin de la preuve de ce théorème idiot : *)
split.
- exact H1.
- exact H3.
Qed.
Le prochain théorème dit la chose suivante :
- si de C on peut déduire le faux
- et que A → C
- alors de A on peut aussi déduire le faux.
Theorem contraposée : ∀ A C : Prop, (A → C) → ¬C → ¬A.
Proof.
(* Soient A et C deux propositions quelconques. *)
intros A C.
(* On suppose :
- (H) : A → C
- (H') : ¬C *)
intros H H'.
(* Dans le but, on remplace ¬A par sa définition, à savoir A → False. *)
unfold not.
(* On suppose (K) : A et on cherche à prouver False. *)
intros K.
(* Dans l'hypothèse (H'), on remplace ¬C par sa définition. *)
unfold not in H'.
(* Pour prouver False, par (H') il suffit de prouver C. *)
apply H'.
(* Pour prouver C, par (H), il suffit de prouver A. *)
apply H.
(* Or, A est vraie par hypothèse. *)
exact K.
Qed.
(* En fait, avec un peu d'habitude, on peut sauter l'étape unfold not. *)
Theorem contraposée' : ∀ A C : Prop, (A → C) → (¬C → ¬A).
Proof.
intros A C H H'.
(* On peut se passer de unfold not si on a bien compris. *)
(* On suppose (K) : A et on cherche à prouver False. *)
intros K.
(* Si on a compris que ¬C est en fait la même chose que C → False,
on peut apply directement H'. *)
apply H'.
apply H.
exact K.
Qed.
Theorem absurd : ∀ A C : Prop, A → ¬A → C.
Proof.
intros A C H H'.
unfold not in H'.
exfalso.
apply H'.
exact H.
Qed.
Theorem exo_neg : ∀ P Q : Prop,
(P → Q) → (P → ¬Q) → ¬P.
Proof.
intros P Q H H' K.
apply H'.
- exact K.
- apply H.
exact K.
Qed.
L'équivalence logique est notée en Coq ↔.
Comme vous le voyez ci-dessus, pour toutes propositions P et Q,
P ↔ Q est la même chose que (P → Q) ∧ (Q → P).
Pour prouver P ↔ Q, il faut donc prouver les deux implications
P → Q et Q → P. Ceci se fait avec la tactique split.
Pour utiliser une équivalence, la tactique destruct fournira les deux
implications, comme pour n'importe quelle 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 :
(H1) : P → Q
(H2) : Q → P *)
destruct H as [H1 H2].
(* Pour prouver P ↔ Q, il suffit de prouver P → Q et Q → P. *)
split.
- (* Preuve de P → Q : *)
exact H2.
- (* Preuve de Q → P : *)
exact H1.
Qed.
Theorem iff_refl : ∀ P : Prop, P ↔ P.
Proof.
intros P.
split.
- intros H.
exact H.
- intros H.
exact H.
Qed.
Theorem iff_trans : ∀ P Q R : Prop, (P ↔ Q) → (Q ↔ R) → (P ↔ R).
Proof.
intros P Q R H H'.
destruct H as [H1 H2].
destruct H' as [H1' H2'].
split.
- intros K.
apply H1'.
apply H1.
exact K.
- intros K.
apply H2.
apply H2'.
exact K.
Qed.
Appliquer un théorème
Module ArgumentsThéorèmes.
(* Module pour ne pas polluer le reste du fichier avec les paramètres A, B
et C. *)
Parameters A B C : Prop.
(* Module pour ne pas polluer le reste du fichier avec les paramètres A, B
et C. *)
Parameters A B C : Prop.
Le théorème and_comm1 a deux variables universellement quantifiées.
On peut appliquer le théorème and_comm1 à deux propositions.
Ou bien à une seule, l'autre restant universellement quantifiée.
On peut même donner en argument des propositions plus compliquées.
On peut alors utiliser dans des preuves des théorèmes déjà prouvés.
Theorem and_comm : ∀ P Q : Prop, (P ∧ Q) ↔ (Q ∧ P).
Proof.
intros P Q.
split.
- exact (and_comm1 P Q).
- exact (and_comm1 Q P).
Qed.
Proof.
intros P Q.
split.
- exact (and_comm1 P Q).
- exact (and_comm1 Q P).
Qed.
Au passage, remarquer le parenthésage un peu particulier de Coq. La plupart
des mathématiciens auraient écrit quelque chose comme
Prouver le théorème suivant en utilisant premisses_non_ordonnées1
and_comm1(P, Q)
,
ici, on écrit simplement la fonction (ou le théorème) et ses arguments
séparés par des blancs et si besoin on les entoure de parenthèses.
Exercice :
Check premisses_non_ordonnées1.
Theorem premisses_non_ordonnées :
∀ P Q R : Prop, (P → Q → R) ↔ (Q → P → R).
Proof.
intros P Q R.
split.
- exact (premisses_non_ordonnées1 P Q R).
- exact (premisses_non_ordonnées1 Q P R).
Qed.
Theorem premisses_non_ordonnées :
∀ P Q R : Prop, (P → Q → R) ↔ (Q → P → R).
Proof.
intros P Q R.
split.
- exact (premisses_non_ordonnées1 P Q R).
- exact (premisses_non_ordonnées1 Q P R).
Qed.
Check and_assoc1.
Check and_assoc2.
Theorem and_assoc : ∀ P Q R, (P ∧ Q) ∧ R ↔ P ∧ (Q ∧ R).
Proof.
intros P Q R.
split.
- exact (and_assoc1 P Q R).
- exact (and_assoc2 P Q R).
Qed.
Unification : Coq travaille pour vous
Theorem and_comm' : ∀ P Q : Prop, (P ∧ Q) ↔ (Q ∧ P).
Proof.
intros P Q.
split.
- (* Le théorème and_comm1 ne peut être appliqué qu'aux arguments P et Q
donc pas la peine de les expliciter. *)
exact (and_comm1 _ _).
- (* Le théorème and_comm1 ne peut être appliqué qu'aux arguments Q et P
donc pas la peine de les expliciter. *)
exact (and_comm1 _ _).
Qed.
Proof.
intros P Q.
split.
- (* Le théorème and_comm1 ne peut être appliqué qu'aux arguments P et Q
donc pas la peine de les expliciter. *)
exact (and_comm1 _ _).
- (* Le théorème and_comm1 ne peut être appliqué qu'aux arguments Q et P
donc pas la peine de les expliciter. *)
exact (and_comm1 _ _).
Qed.
Parfois, Coq ne peut pas tout deviner, il a besoin de certains arguments.
Theorem iff_trans' : ∀ P Q R : Prop, (P ↔ Q) → (Q ↔ R) → (P ↔ R).
Proof.
(* On va en donner une nouvelle preuve avec imp_trans. *)
intros P Q R [H1 H1'] [H2 H2'].
split.
- (* On veut utiliser le fait que (P → Q) et (Q → R) implique
(P → R). *)
Check imp_trans.
(* Le théorème imp_trans a 3 arguments.
Ici, Coq peut deviner, vu la forme du but
et la conclusion de imp_trans :
que le premier est P et que le troisième est R, mais il n'a aucun
moyen de savoir que le deuxième devrait être Q !
On va donc lui fournir. *)
apply (imp_trans _ Q _).
+ exact H1.
+ exact H2.
- (* On recommence, pour prouver R → P, il suffit de prouver R → Q
et Q → P (qu'on a déjà dans le contexte).
Coq peut encore deviner, vu le but :
que le premier argument est R, le troisième est P, mais il ne peut
unifier sans qu'on lui donne le deuxième argument. *)
apply (imp_trans _ Q _).
+ exact H2'.
+ exact H1'.
Qed.
Proof.
(* On va en donner une nouvelle preuve avec imp_trans. *)
intros P Q R [H1 H1'] [H2 H2'].
split.
- (* On veut utiliser le fait que (P → Q) et (Q → R) implique
(P → R). *)
Check imp_trans.
(* Le théorème imp_trans a 3 arguments.
Ici, Coq peut deviner, vu la forme du but
et la conclusion de imp_trans :
que le premier est P et que le troisième est R, mais il n'a aucun
moyen de savoir que le deuxième devrait être Q !
On va donc lui fournir. *)
apply (imp_trans _ Q _).
+ exact H1.
+ exact H2.
- (* On recommence, pour prouver R → P, il suffit de prouver R → Q
et Q → P (qu'on a déjà dans le contexte).
Coq peut encore deviner, vu le but :
que le premier argument est R, le troisième est P, mais il ne peut
unifier sans qu'on lui donne le deuxième argument. *)
apply (imp_trans _ Q _).
+ exact H2'.
+ exact H1'.
Qed.
Theorem or_comm : ∀ P Q : Prop, P ∨ Q ↔ Q ∨ P.
Proof.
intros P Q.
split.
- exact (or_comm1 _ _).
- exact (or_comm1 _ _).
Qed.
Proof.
intros P Q.
split.
- exact (or_comm1 _ _).
- exact (or_comm1 _ _).
Qed.
Exercice : Prouver le théorème suivant en utilisant imp_refl et en laissant au maximum Coq unifier.
Theorem imp3' : ∀ P Q R : Prop, (P → Q → R) → (P → Q → R).
Proof.
intros P Q R.
exact (imp_refl _).
Qed.
Proof.
intros P Q R.
exact (imp_refl _).
Qed.
Bilan
Vient la partie la plus importante, il faut que tout ce que vous avez appris cette semaine soit acquis pour les suivantes. Nous avons rencontré (dans cet ordre), les tactiques suivantes :- intros une variable universellement quantifiée dans le but
- intros une hypothèse lorsque le but est une implication
- exact
- apply une preuve d'une implication
- destruct une preuve d'une conjonction
- split
- destruct une preuve d'une disjonction
- left et right
- unfold
- implication →
- conjonction ∧
- disjonction ∨
- False et négation ¬
- équivalence ↔