Langages et Traducteurs – Chapitre 4 - Arbres de preuve
1 Arbres de preuve
Un arbre de 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 Rocq 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
add_assoc : ∀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 add_assoc
xparnbo e1 + 1yparnbo e2zpar1
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 add_assoc 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
add_assoc (nbo e1 + 1) (nbo e2) 1
Autrement dit on aurait pu écrire explicitement :
rewrite (add_assoc (nbo e1 + 1) (nbo e2) 1)
Heureusement Rocq peut ici deviner les substitutions à effectuer, on écrit juste
rewrite add_assoc.
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 Rocq 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 stopP (feu c d), pour toutc:coulfeuet toutd:direction- et
P (limitation n), pour tout natureln.
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 : nous 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
h1pour la formuleP ∧ Q - à partir de
h1, je déduisP(en retenant le second élément de la formule) - à partir de
h1, je déduis égalementQ(en retenant le premier élément de la formule) - à partir de
QetPainsi obtenus, je déduisQ ∧ 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 prouverA ∧ B
A B ----- ∧i A ∧ B
∧e1: élimination de∧, disant comment utiliserA ∧ B(première manière)
A ∧ B ----- ∧e1 A
∧e2: élimination de∧, disant comment utiliserA ∧ 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 Rocq 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 Rocq 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 veut montrer 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 Rocq 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 !
∼∼∼
Made with Org-mode