(* 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

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, parfois aussi noté ℙ dans certaines interfaces, est celui des propositions, c'est-à-dire des énoncés mathématiques que l'on peut chercher à prouver ou à réfuter.

La commande Check permet d'imprimer le type d'un terme. Appuyer sur Ctrl+↓ (si vous utilisez 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.

Check 2 + 2 = 4. Check 2 + 2 = 5.

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 »). Intuitivement, dans la logique de Coq, la proposition P -> Q signifie « si P, alors Q » ou, plus précisément, « je sais construire une preuve de Q à partir d'une preuve de P. » Remarque : 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.

Première preuve

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 (* ... *). Ici, comme à beaucoup d'autres endroits de ce cours, ils sont destinés à vous montrer la preuve « mathématique » très détaillée correspondant à la preuve en Coq.

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 !

Theorem imp_refl : forall 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. *)

Sans entrer dans tous les détails, quelques commentaires s'imposent :

• 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.

Pour pouvoir passer à la suite, il faut avoir vraiment bien compris que

• 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. Si besoin, exécuter de nouveau la preuve et bien regarder l'évolution de l'état de la preuve.

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.

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

Plusieurs flèches à la suite

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

Exercice : Prouver le théorème suivant.

Theorem imp_ex2 : forall P Q : Prop, Q -> (P -> P). Proof. (* Remplir la preuve ici *) Admitted. (* Remplacer cette ligne par 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 Pet Q, alors R », ou encore, « si j'ai une preuve de P et une preuve de Q, alors je sais construire 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 : forall 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.

• Socrate est un homme. ( P)
• Tous les hommes sont mortels. ( P -> Q)
• Donc Socrate est mortel. ( 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.

Exercice : Prouver le théorème suivant.

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

Les sous-buts

Il arrive très souvent qu'une tactique crée des sous-buts (en anglais subgoals ), comme dans cette preuve du théorème suivant.

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

Remarque : la preuve de l'exemple précédent est volontaire idiote pour vous montrer comment des sous-buts peuvent être générés. Seriez-vous capable de trouver une preuve beaucoup plus courte ?

Exercice : Prouver le théorème suivant.

Theorem premisses_non_ordonnées1 : 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.

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

Conjonction /\

Le « et logique » aussi appelé opérateur de conjonction est noté en Coq /\. Si P et Q sont deux propositions, alors P /\ Q est une proposition dont une preuve est à la fois une preuve de P et une preuve de Q.

Utiliser une conjonction : destruct

Pour décomposer une preuve de P /\ Q en une preuve de P et une preuve de Q, on utilise la tactique destruct.

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

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

Theorem proj1' : forall P Q : Prop, P /\ Q -> P. Proof. intros P Q [H1 H2]. exact H1. Qed.

Exercice : Prouver le théorème suivant en utilisant un «  intro pattern  ».

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

Prouver une conjonction : split

Prouver P /\ Q se fait en deux étapes : il faut une preuve de P et une preuve de Q. Ceci se fait avec la tactique split.

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

Exercice : Prouver le théorème suivant.

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

Disjonction \/

En Coq, le « ou logique », aussi appelée opérateur de disjonction, est noté \/. Une preuve de P \/ Q est une preuve de P ou une preuve de Q.

Prouver une disjonction : left et right

Pour pouvoir prouver une disjonction (par exemple P \/ Q) en logique intuitionniste, il faut dire explicitement si l'on donne une preuve de l'opérande de gauche (ici P) ou de celui de droite (ici Q). Ceci se fait avec les tactiques left et right.

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

Exercice : Prouver le théorème suivant.

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

Utiliser une disjonction : destruct

Pour utiliser une disjonction (par exemple une preuve de P \/ Q), on doit faire une preuve par cas :

• 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. Ceci se fait encore avec la tactique destruct.

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

Exercice : Prouver le théorème suivant.

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

De la même manière que pour /\, on peut utiliser un «  intro pattern  » pour détruire une disjonction directement.

Theorem or_comm1' : forall P Q : Prop, P \/ Q -> Q \/ P. 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 : forall P Q R : Prop, P \/ (Q /\ R) -> (P \/ Q) /\ (P \/ R). Proof. intros P Q R [H1 | [H2 H3]]. (* À vous de terminer ! *) (* 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 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 (Remarque encourageante, nous avons vu la moitié environ des tactiques utilisées dans ce cours.) Vous devez écrire une fiche décrivant le rôle de chaque tactique, un exemple de syntaxe, et la façon dont elle modifie l'état de la preuve (contexte et/ou but).

Nous avons aussi rencontré (dans cet ordre) des connecteurs logiques :

• implication ->
• conjonction /\
• disjonction \/ Vous devez écrire, pour chacun d'entre eux, son sens « intuitif », la façon dont on le prouve et la façon dont on l'utilise dans une preuve.

Enfin, vous devez savoir utiliser un théorème déjà prouvé dans une autre preuve et comprendre qu'on peut laisser à Coq certains « trous » qu'il peut remplir avec l'unification.