(*Bienvenue dans ce premier atelier d’assistant de preuve. Vous vous trouvez dans un fichier '….v', c’est-à-dire un fichier destiné à Coq contenant des théorèmes et des preuves. Vous pouvez intéragir avec ce fichier. Le texte placé entre '(*' et '*)' correspond à des commentaires, cela permet d’intégrer des explications dans le code des démonstrations pour le rendre plus lisible et facile à utiliser. Le 'vrai' code Coq, celui qui apparaît en couleurs, peut être exécuté. Les commandes et instructions Coq finissent toujours par un point. Pour exécuter une commande, on peut demander à Coq de lire ce qui est écrit jusqu’au prochain point; avec Ctrl + ↓ Pour revenir au point précédent : Ctrl + ↑. Vous pouvez aussi lire toutes les commandes jusqu’au curseur avec Ctrl + →. *) (*La commande suivante permet de découper les fichiers en différentes sections*) Section Premiers_Pas. (* J’indique d’abord à Coq que je vais utiliser par la suite des formules A, B et C quelconques. Comme je ne fais pas d’autre hypothèse sur ces formules, les théorèmes que nous allons démontrer seront valides en logique propositionnelle pour n’importe quelles autres formules.*) Variable A B C: Prop. (*Notez qu’après avoi r lu cette ligne, Coq nous indique que ces formules sont bien déclarées, dans l’encadré en bas à droite où apparaissent les messages (dont les messages d’erreurs, on en verra souvent et il sera important de les lire et de les comprendre !) *) (* Comment est-ce qu’on démontre la validité des formules ? D’abord, il faut donner un nom à la propriété qui nous intéresse, et l’énoncer en tant que théorème. Cela s’écrit comme ça : « 'Theorem'[nom du théorème (on le choisit)] ':' [formule à prouver] '.' » (ne pas oublier le point ! *) Theorem a: A. (* Intéressons-nous à ce qui se passe dans la fenête en haut à droite : Ce qui se trouve sous la barre est l'objectif, c’est-à-dire la formule à prouver. Ce qui se trouve au-dessus, ce sont les hypothèses. Ici il n’y en a pas vraiment, Coq nous indique uniquement les formules qui existent et que l’on peut utiliser. La commande 'Proof' indique que nous entrons dans la démonstration du théorème.*) Proof. (*Bien sûr, on ne peut pas démontrer ce théorème : si je vous demande de prouver une formule A quelconque, vous serez tout de suite bloqué. La commande 'Abort' indique que nous abandonnons la preuve de ce théorème. Ça peut vouloir dire qu’il est faux, ou que l’on a pas réussi à le démontrer. *) Abort. (* Cela veut dire une chose importante : Un théorème est validé par Coq si sa preuve est terminée. (Il peut être présent dans le code Coq sous le nom 'Theorem …' et être faux, comme dans notre exemple) Une preuve complète est terminée par la commande 'Qed' (pour 'Quod Erat Demonstrandum', qui signifie en latin : 'Ce qu’il fallait démontrer' (=CQFD en français)) *) (* Regardons maintenant un vrai théorème da la logique propositionnelle : En déduction naturelle, comment est-ce qu’on prouve A -> A ? En partant de la formule à prouver (du bas vers le haut dans la preuve), On introduit la flèche, puis on utilise l’axiome. ------(ax) A |- A --------- (->i) |- A -> A En Coq on va faire exactement pareil. *) Theorem tauto : A-> A. Proof. (*on a d’abord notre formule à démontrer, sans hypothèse*) intro H. (*maintenant, le but a changé, il faut démontrer la formule A. mais on a cette fois une hypothèse (nommée H) : la formule A elle-même. On n’est pas obligé de donner le nom à l’hypothèses, si on écrit simplement "intro", Coq choisit automatiquement un nom (H,H0,etc…). Mais c’est mieux de le faire pour que la preuve (la suite des commandes) soit plus compréhensible : Sinon, quand on utilisera 'H', il faudra deviner quand Coq aura introduit cette hypothèse. On est donc dans la configuration où il faut prouver A|-A.) Cela se fait en disant à Coq que ce qu’il faut prouver apparaît dans les hypothèses. La commande correspondant est 'assumption' (= 'hypothèse' en anglais) *) assumption. (*Il n’y a plus d’objectifs restant, ça veut dire qu’on a démontré tout ce qu’il fallait. On peut conclure et terminer la preuve.avec 'Qed'. *) Qed. (*Exercice : démontrez le théorème suivant : *) (*Theorem tauto' : A-> (A-> A).*) (* +++++++++++++++++++++++++++++++++ *) (* On a vu comment utiliser l’axiome (assumption) et l’introduction de la flèche (intro). Regardons maintenant ce qui correspond à une règle d’élimination. En déduction naturelle, on peut prouver (A/\B->A) avec la preuve suivante : ------------(ax) A/\B |- A/\B ------------ (et-elim-gauche) A/\B|- A ---------- (-> i) |- A/\B->A En Coq, on ne va pas utiliser la même règle d’élimination : Le principe est de dire que si on a l’hypothèse A/\B, alors c’est comme si on avait deux hypothèses : A, et B. Cette nouvelle règle s’appellera 'destruct', car elle 'casse' l’hypothèse (qui est une formule composée) en plusieurs hypothèses (qui sont plusieurs hypothèses simples). Si on avait cette règle en déduction naturelle pour la conjonction, elle s’écrirait : A,B|- C -----------(destruct) A/\B|-C Remarquez que ce n’est plus de la déduction naturelle comme vous l’avez vue en cours, car la règle modifie ce qui est à gauche du taquet. (ce nouveau calcul s’appelle 'calcul des séquents') Notre preuve de A/\B->A peut s’écrire un peu différemment : -------(ax) A,B|-A -------(destruct) A/\B|-A ---------(-> i) |-A/\B->A En Coq, il faut dire quelle est l’hypothèse que l’on 'casse', donc on utilise son nom (souvent c’est H, H0, H1,…, ou on peut nous même donner un nom à l’hypothèse introduite si l’on écrit 'intro Nom_de_l_Hypothèse'). Allons-y. *) Theorem projection : A /\ B -> A. Proof. intro H. destruct H. (* Cette règle m’a bien créé deux nouvelles hypothèses (H et H0), parmi lesquelles figure mon objectif. Je peux donc terminer. Je peux aussi écrire "destruct H in (H1, H2)" si je veux fixer le nom de mes nouvelles hypothèses. *) assumption. Qed. (*Exercice : prouvez le théorème suiivant :*) (* Theorem projection' : (A/\B)/\C->B. *) (* +++++++++++++++++++++++++++++++++++++ *) (* On a vu comment utiliser une conjonction en hypothèse, en récupérant les sous-formules. Voyons maintenant comment s’y prendre lorsque l’on veut prouver une formule de la forme A/\B. Prenons une formule valide et sa preuve en déduction naturelle : ----(ax) -------(ax) A|-A B|-B ------------------(^-i) A,B|-A/\B ----------(->i) A|-B->(A/\B) -------------(->i) |-A->B->(A/\B) En Coq, la preuve va être la même. Ce qu’il nous manque est l’équivalent de la règle (^i) qui permet de dire que pour prouver A/\B, il est possible de prouver d’abord A, et ensuite B. En Coq, cela signifie que l’on va se retrouver avec plusieurs objectifs, un par sous-formule. *) Theorem conj : A->B->(A/\B). intro Ha. (* je donne un nom à mon hypothèse. Ma preuve sera plus compréhensible*) intro Hb. split. (* je me retrouve avec deux objectifs *) (* le tiret permet de dire 'je commence la preuve du premier objectif il n’est pas obligatoire, mais ça rend la preuve plus agréable à écrire et à lire. Si on ne l’utilise pas, on passe juste à la sous-preuve suivante dès qu’une est terminée (c’est-à-dire n’a plus d’objectif) *) - assumption. (*facile, A est dans les hypothèses *) (*la preuve du premier but est terminée, je commence celle du deuxième but *) - assumption. (*Tous les objectifs sont terminés, on peut conclure *) Qed. (* Exercice : prouvez le théorème suivant, qui signifie que la conjonction est commutative (l’ordre des formules ne change pas la validité) *) (*Theorem commut : A/\B->B/\A. *) (* +++++++++++++++++++++++++++++++++++++++ *) (* Équivalence et preuves imbriquées : Une formule de la forme A <-> B est simplement une abréviation pour (A -> B) /\ (B -> A). Donc pour prouver une équivalence, on commence souvent par 'split', pour nous retrouver avec les deux objectifs correspondant. Quand on est dans une preuve pour un objectif particulier, on peut être amené à utiliser à nouveau 'split' (ou une autre tactique qui génère plusieurs objectifs). Dans ce cas on se retrouve avec des sous-objectifs de sous-objectifs,… et ce type d’imbrication peut aller très loin. Pour éviter de se mélanger les pinceaux, il est recommandé d’utiliser des 'puces' (comme '-') pour structurer la preuve. Dans un arbre de déduction naturelle, s’il y a plusieurs conjonctions, c’est facile de voir à quelle partie correspond quelle sous-preuve, car on 'voit' les branches juste en regardant la preuve. En Coq, il faut rendre les choses aussi lisibles que possible (comme en programmation, ou dans des démonstrations écrites à la main d’ailleurs !). On a le droit d’utiliser des puces différentes (-, --, ---,…, +,++,+++,…, *, **,. En exercice, essayez de prouver l’associativité de la conjonction. Conseils : - commencez par faire une preuve au brouillon en déduction naturelle ou calcul des séquents - dès que vous avez comme objectif une conjonction (ou <->), Utilisez 'split' et utilisez des puces pour identifier facilement les sous-preuves. - n’hésitez pas à insérer des commentaires pour éviter à vous ou à vos éventuels relecteurs de se mélanger les pinceaux. *) (*Exercice : Theorem assoc : A/\(B/\C) <-> (A/\B)/\C. *)