Table of Contents
- 1. Arbres de preuve
- 2. Compléments sur la déduction naturelle
LANGAGES ET TRADUCTEURS – Chapitre 4 Jean-François Monin, 2021
1 Arbres de preuve
Un arbre preuve permet de dériver une conclusion (en bas, à la racine) sous des hypothèses (placées en haut, aux feuilles). Chaque noeud de l'arbre correspond à une inférence désignée par un nom et éventuellement des arguments en paramètre.
Par exemple la règle permettant de dériver une conjonction P ∧ Q est
P Q ------- ∧i P ∧ Q
Certaines règles font varier le stock d'hypothèses, à commencer par la règle d'introduction de l'implication : "pour démontrer P -> Q, on suppose P et on démontre Q". Autrement dit on démontre Q en introduisant une hypothèse supplémentaire pour P.
On distingue les règles de fabrication, qui indiquent comment conclure à une formule de forme donnée (par exemple une conjonction). et les règles dites utilisation, qui indiquent comment exploiter une formule de forme donnée.
1.1 Vocabulaire : règles d'introduction et d'élimination
Traditionnellement, les règles de fabrication sont appelées règles d'introduction et règles d'utilisation sont appelées règles d'élimination. La tactique "introduction" est utilisée en Coq uniquement pour les étapes de preuve correspondant à ∀i (et ->i).
1.2 Règles de l'égalité (déjà vues)
------- eq_refl
x = x
x = y P x
---------------- rew <-
P y
Ce qui amène d'autres questions.
1.2.1 Comment démontrer :
- ∀x, x = x ?
- ∀x∀y, x = y -> y = x ?
- ∀x∀y∀z, x = y -> (y = z -> x = z) ?
1.2.2 Comment utiliser
- addassoc : ∀x∀y∀z, x + (y + z) = x + y + z ?
avec comme but nbo e1 + 1 + (nbo e2 + 1) = nbo e1 + 1 + nbo e2 + 1 (nbo e1 + 1) + (nbo e2 + 1) = ((nbo e1 + 1) + nbo e2) + 1
Substituer dans addassoc
- x par nbo e1 + 1
- y par nbo e2
- z par 1
1.3 Règles de la quantification universelle ∀
--- x
T \ . /
. \ . / t
. \ . /
. ---
P x ∀x:T, P x T
--------- ∀i ------------------------ ∀e
∀x:T, P x P t
∀x, mul2 x ∀x, mul4 x -> mul2 x
Autrement dit addassoc est une fonction qui prend trois arguments x y z, et rend alors une preuve (un arbre de preuve) de l'égalité x + (y + z) = x + y + z.
La justification complète de l'étape de preuve est en fait addassoc (nbo e1 + 1) (nbo e2) 1
Autrement dit on aurait pu écrire explicitement : rewrite (addassoc (nbo e1 + 1) (nbo e2) 1)
Heureusement Coq peut ici deviner les substitutions à effectuer, on écrit juste rewrite addassoc.
Mais parfois il y a ambiguïté, et alors il faut préciser…
1.4 Règles de l'implication ->
--- h A . . . B A -> B A ------ ->i ----------- ->e A -> B B
NB. lorsque l'on a deux implications successives, schématiquement A -> B -> C, cela se lit A -> (B -> C), c'est-à-dire littéralement : "A implique que B implique C", ou encore "à partir de A, alors à partir de B, on peut prouver C" soit encore, intuitivement "A et B impliquent C", mais sans utilisation de la conjonction. A ce propos, voir les compléments.
Interprétation en terme de fonction : une preuve de A -> B est une fonction qui prend en entrée une preuve de A et rend en sortie une preuve de B. C'est pour cela que la tactique Coq correspondant à ->i s'appelle de la même manière que pour ∀i, càd. intro.
1.5 Raisonnements par cas sur les valeurs prises par une structure de données
Ces règles de raisonnement s'écrivent sous forme de règles d'inférence. Elles sont conçues en examinant les différents choix possibles pour construire une structure de données. D'un point de vue fonctionnel, un raisonnement par cas correspond à un match with.
Quelques exemples.
1.5.1 Raisonnement par cas sur un type énuméré
Considérons le type énuméré coulfeu donné dans un cours précédent.
Soit P un prédicat sur coulfeu. Pour démontrer P (c) il suffit de démontrer P (vert), P (orange) et P (rouge).
Cela se formalise par la règle suivante, dite raisonnement par cas :
c : coufeu P vert P orange P rouge
------------------------------------------- cas_coulfeu
P c
1.5.2 Raisonnement par cas sur un type somme
Considérons le type somme signal :
Inductive signal : Set := | stop : signal | feu : coulfeu -> direction -> signal | limitation : nat -> signal
Soit P un prédicat sur ces signalisations routières. Pour démontrer ∀s, P s il suffit de démontrer à la fois
- P stop
- P (feu c d), pour tout c:coulfeu et tout d:direction
- et P (limitation n), pour tout naturel n.
Cela se formalise par la règle de raisonnement par cas suivante :
------- c --------- d --- n
\ coulfeu direction / nat
\ . / .
\ . / .
\ . / .
s:signal P stop P (feu c d) P (limitation n)
---------------------------------------------------------------- cas_signal[ | c d | n]
P s
1.5.3 Raisonnement par cas sur le type des listes d'entiers
Le raisonnement par cas se présente exactement de la même façon
--- x ------- q
nat listnat
\ . /
\ . /
\ . /
l : list P Nil P (Cons x q)
------------------------------------- cas_listnat[ | x q]
P l
1.6 Récurrence structurelle
Le raisonnement par cas est souvent trop limité sur une structure de données récursive, comme les listes. D'un point de vue fonctionnel, la récurrence structurelle c'est un raisonnement par cas plus l'utilisation de la récursivité (un match with à l'intérieur d'un Fixpoint).
1.6.1 Récurrence structurelle sur les listes
Pour le cas du Cons, on peut supposer que la propriété désirée a déja été démontrée sur la sous-liste. La règle est :
x : nat q : listnat ------- Hrec_q
\ P q /
\ . /
\ . /
\ . /
l:listnat P Nil P (Cons x q)
-------------------------------------------------------- rec_listnat[ | x q Hrec_q]
P l
1.6.2 Récurrence structurelle sur les arbres binaires
On considère le type :
type arbin = Vide | Nbin of arbin * nat * arbin
Pour le cas Nbin g n d, l'étape de récurrence consiste à supposer que si la propriété désirée a déja été démontrée sur les deux sous-arbres de gauche g et de droite d, alors on peut la déduire sur Nbin g n d
La règle est :
g, d: arbin n : nat ----- Hrec_g ----- Hrec_d
\ P g P d /
\ /
\ /
a:arbin P Vide P (Nbin g n d)
--------------------------------------------------------------------- rec_arbin
P a
1.6.3 Récurrence structurelle sur les AST
Les AST pour les expressions arithmétiques, booléennes et les commandes du langage WHILE peuvent être traités de la même manière. Simplement, on a plus de cas à considérer : ous en aurons typiquement 5 cas pour Aexp, 6 pour Bexp et 5 pour Stm.
Exercice : énoncer les règles de récurrence structurelle pour Aexp, Bexp et Stm.
2 Compléments sur la déduction naturelle
Pour plus de détails sur ces bases, cf.cours de déduction naturelle, par ex. http://www-verimag.imag.fr/~monin/EnseignementPublic/PEIP/Raisonnement_Structure/
2.1 Principe
tout raisonnement logique peut être présenté en employant des règles d'inférence, organisées sous forme d'arbre de preuve pour déduire une conclusion à partir d'hypothèses. Dans un tel arbre, les noeuds sont étiquetés par le nom des règles d'inférence et les hypothèses sont aux feuilles, et la conclusion se trouve à la racine. Dans la vie courante, ces noeuds correspondent aux endroits du raisonnement où on indique "raisonnement par cas", "raisonnement par récurrence", utilisation de telle hypothèse, etc. En plus du nom des règles, on indique aussi les formules logiques déduites ou supposées.
2.2 Exemple
Pour prouver Q ∧ P à partir de P ∧ Q, le raisonnement est le suivant :
- posons l'hypothèse h1 pour la formule P ∧ Q
- à partir de h1, je déduis P (en retenant le second élément de la formule)
- à partir de h1, je déduis également Q (en retenant le premier élément de la formule)
- à partir de Q et P ainsi obtenus, je déduis Q ∧ P
La présentation sous forme d'arbre de preuve est :
----- h1 ----- h1
P ∧ Q P ∧ Q
----- ∧e2 ----- ∧e1
Q P
---------------- ∧i
Q ∧ P
2.3 Règles de la conjonction ∧
Les règles d'inférences utilisées ci-dessus sont
- ∧i : introduction de ∧, disant comment prouver A ∧ B
A B ----- ∧i A ∧ B
- ∧e1 : élimination de ∧, disant comment utiliser A ∧ B (première manière)
A ∧ B ----- ∧e1 A
- ∧e2 : élimination de ∧, disant comment utiliser A ∧ B (deuxième manière)
A ∧ B ----- ∧e2 B
NB : les logiciens, comme les botanistes et contrairement aux informaticiens, dessinent leurs arbres en plaçant la racine en bas et les feuilles en haut.
Remarque : la règle d'élimination employée par Coq est différente, voir plus bas.
2.4 Règles de l'implication -> et lien avec ∧
--- h A . . . B A -> B A ------ ->i ----------- ->e A -> B B
NB. lorsque l'on a deux implications successives, schématiquement A -> B -> C, cela se lit A -> (B -> C), c'est-à-dire littéralement : "A implique que B implique C", ou encore "à partir de A, alors à partir de B, on peut prouver C" soit encore, intuitivement "A et B impliquent C". En fait cette dernière devrait plutôt s'écrire : (A ∧ B) -> C. On peut assez facilement démontrer que les deux formules A -> (B -> C) et (A ∧ B) -> C sont équivalentes.
Autrement dit on peut inférer (A ∧ B) -> C à partir de l'hypothèse A -> (B -> C) et réciproquement.
La première est techniquement plus pratique à utiliser en déduction naturelle.
2.5 Règles de la disjonction ∨
--- a --- b
A B
. .
. .
. .
A B A ∨ B C C
----- ∨i_l ----- ∨i_r ---------------------- ∨e[a | b]
A ∨ B A ∨ B C
2.6 Remarque
En Coq l'élimination du ∧ se définit (de manière équivalente) en une seule règle, qui indique qu'une preuve de A ∧ B se décompose en deux sous-preuves, une pour A et une pour B.
--- a --- b
\ A B /
\ . /
\ . /
\ . /
A ∧ B C
------------------------ ∧e[a b]
C
Intuitivement, supposons que l'on ait A /\ B en hypothèse, on peut alors remplacer cette dernière par deux hypothèses, une pour A et une pour B L'idée sous-jacente est la suivante. On veutENDntrer C à partir de A ∧ B ; mais si on est parvenu à démontrer A ∧ B, c'est que l'on était capable de démontrer A ainsi que B ; on va donc démontrer C en se donnant deux hypothèses supplémentaires, une pour Α (nommée a ci-dessus), et une pour Β (nommée b ci-dessus).
Cette version de l'élimination de ∧ est analogue à l'élimination traditionnelle du ∨, qui demande de considérer deux cas avec pour chacun une hypothèse supplémentaire, respectivement a:A et b:B.
Cette uniformité se traduit en Coq par le fait que l'on a une seule tactique pour exploiter une conjonction ou une disjonction en hypothèse, nommée destruct. En fait destruct fonctionne comme le filtrage !