(* This file is part of the "Initiation aux preuves formelles" course in Villetaneuse, France. Copyright (C) Kerjean, Mayero, Rousselin This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version. This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details. *)

Logique de base en Coq (deuxième partie)

Négation ~

La négation en Coq est un peu particulière par rapport à la négation d'un cours de mathématique usuel. En effet, on ne définit pas la négation d'une proposition par sa table de vérité mais en ajoutant une nouvelle proposition appelée False.

La proposition False

Check 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 : forall 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.

Exercice : prouver le théorème suivant :

Indice : réfléchissez avant de tout introduire...

Theorem exo_false : forall P Q : Prop, P -> False -> (P -> P) -> (Q -> P -> P) -> (Q -> Q -> P) -> P -> Q. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par 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 : forall 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.

Exercice : Prouver le théorème suivant en utilisant exfalso.

Theorem P_et_P_imp_False : forall P Q : Prop, P /\ (P -> False) -> Q. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Réfuter une proposition

La négation d'une proposition P, notée en Coq ~P, ou encore not P, est en fait simplement une notation pour P -> False.

Check not. Print not. Locate "~".

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 : forall 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 : forall A C : Prop, (A -> C) -> ~C -> ~A. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *) (* En fait, avec un peu d'habitude, on peut sauter l'étape [unfold not]. *) Theorem contraposée' : forall 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.

Exercice : Prouver le théorème suivant. Pensez à exfalso.

Theorem absurd : forall A C : Prop, A -> ~A -> C. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant.

Theorem exo_neg : forall P Q : Prop, (P -> Q) -> (P -> ~Q) -> ~P. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Équivalence <->

Locate "<->". Print iff.

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 : forall 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.

Exercice : Prouver le théorème suivant.

Theorem iff_refl : forall 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 : forall P Q R : Prop, (P <-> Q) -> (Q <-> R) -> (P <-> R). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Appliquer un théorème

On peut fournir des arguments à un théorème pour produire des formules déjà prouvées.

Pour les besoins de cette section, on rappelle les lemmes suivants vus dans Logique1 et Logique1Maison

Lemma and_comm1 : forall P Q : Prop, (P /\ Q) -> (Q /\ P). Proof. intros P Q [HP HQ]. split. - exact HQ. - exact HP. Qed. Lemma premisses_non_ordonnées1 : forall P Q R : Prop, (P -> Q -> R) -> (Q -> P -> R). Proof. intros P Q R H1 H2 H3. apply H1. - exact H3. - exact H2. Qed. Theorem and_assoc1 : forall P Q R : Prop, (P /\ Q) /\ R -> P /\ Q /\ R. Proof. intros P Q R [[H1 H2] H3]. split; [exact H1 | split]; [exact H2 | exact H3]. Qed. Theorem and_assoc2 : forall P Q R : Prop, P /\ (Q /\ R) -> (P /\ Q) /\ R. Proof. intros P Q R [H1 [H2 H3]]. split; [split | exact H3]; [exact H1 | exact H2]. Qed. Theorem imp_trans : forall P Q R : Prop, (P -> Q) -> (Q -> R) -> (P -> R). Proof. intros P Q R H1 H2 H3. exact (H2 (H1 H3)). Qed. Theorem or_comm1 : forall P Q : Prop, P \/ Q -> Q \/ P. Proof. intros P Q [H1 | H2]; [right; exact H1 | left; exact H2]. Qed. Theorem imp_refl : forall P : Prop, P -> P. Proof. intros P H. exact H. Qed. Section ArgumentsThéorèmes. (* Section 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.

Check and_comm1.

On peut appliquer le théorème and_comm1 à deux propositions.

Check and_comm1 A B.

Ou bien à une seule, l'autre restant universellement quantifiée.

Check and_comm1 A.

On peut même donner en argument des propositions plus compliquées.

Check and_comm1 (A -> B) (B -> C). End ArgumentsThéorèmes.

On peut alors utiliser dans des preuves des théorèmes déjà prouvés.

Theorem and_comm : forall P Q : Prop, (P /\ Q) <-> (Q /\ P). 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 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 :

Prouver le théorème suivant en utilisant premisses_non_ordonnées1

Check premisses_non_ordonnées1. Theorem premisses_non_ordonnées : forall P Q R : Prop, (P -> Q -> R) <-> (Q -> P -> R). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice :

Prouver le théorème suivant en utilisant and_assoc1 et and_assoc2

Check and_assoc1. Check and_assoc2. Theorem and_assoc : forall P Q R, (P /\ Q) /\ R <-> P /\ (Q /\ R). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Unification : Coq travaille pour vous

En mathématiques, il est fréquent d'omettre les arguments que l'on donne à un théorème, d'autant plus lorsqu'il n'y a aucune ambigüité. En Coq, il faut souvent être beaucoup plus explicite. Mais il y a des mécanismes qui permettent d'éviter de tout préciser. L'un deux est l'unification : Coq essaie de deviner quels arguments donner à une formule un ou théorème. Lorsqu'à la place d'un terme on écrit _, on dit à Coq qu'il doit essayer de deviner ce qu'il y a à la place.

Theorem and_comm' : forall P Q : Prop, (P /\ Q) <-> (Q /\ P). Proof. intros P Q. split. - (* Vu le but, 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 _ _). - (* Vu le but, 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' : forall 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.

Exercice : Prouver le théorème suivant en utilisant or_comm1 et en laissant au maximum Coq unifier.

Theorem or_comm : forall P Q : Prop, P \/ Q <-> Q \/ P. Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par Qed. *)

Exercice : Prouver le théorème suivant en utilisant imp_refl et en laissant au maximum Coq unifier.

Votre preuve doit utiliser seulement un intros et un exact.

Theorem imp3' : forall P Q R : Prop, (P -> Q -> R) -> (P -> Q -> R). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par 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 notions suivantes :

• proposition False, négation
• élimination de False avec destruct
• remplacement du but par False avec exfalso dans le cas d'un contexte contradictoire
• équivalence : prouver avec split, utiliser avec destruct
• une équivalence n'est rien d'autre que la conjonction de deux implications
• utiliser un théorème déjà prouvé, comme n'importe quel autre terme du contexte
• l'unification faite par Coq (implicitement ou non) Assurez-vous d'avoir bien compris ces notions, fondamentales pour la suite du modules (et en général).