Guide de lecture des scripts PhoX

Le principe général : les commandes qui ont été envoyées au système sont précédées d'un prompt>PhoX> ou %PhoX%. On distingue alors deux types de commandes:

Les commandes générales, précédées de >PhoX> : elles permettent de commencer une preuve avec les commandes goal ou theorem.
Les commandes Sort et Cst sont utilisées pour définir le langage que l'on va utiliser (elles définissent respectivement de nouvelles sortes (voir chapitre 6 du livre) et de nouvelles constantes d'une sorte donnée. Vous pouvez donc les ignorer.
Les commandes de preuve ou tactiques, précédées de %PhoX%: elle permettent de faire des preuves. Les indications données ci-dessous devraient vous permettre de lire ces preuves.

Lorsque l'on fait une preuve, on doit prouver un certain nombre de buts (ou goal). Chaque but est numéroté par une annotation du genre goal 1/3. Un but est constitué par un ensemble d'hypothèses qui sont nommées (annotation H := ...) et d'une conclusion précédée du signe

Voici un exemple avec 2 buts:

goal 2/2
H := (a  b  c)  c
H0 := (a  c  c)  (b  c  c)  c
H1 := a
H2 := b
    b  c  c

goal 1/2
H := (a  b  c)  c
H0 := (a  c  c)  (b  c  c)  c
H1 := a
H2 := b
    a  c  c

La commande s'applique alors au but numéro 1 (celui qui est juste avant la commande). Voici une liste de commandes avec leur signification:

axiom pour indiquer que le but courant est prouvé par une règle axiome.
intro ou intros pour appliquer une ou plusieurs règles d'introduction de la déduction naturelle.
left ou lefts pour appliquer une ou plusieurs règles d'introduction à gauche (ce sont des règles dérivées de la déduction naturelle). Comme il y a plusieurs hypothèses, on doit indiquer le nom de l'hypothèse concernée.
elim ou apply pour appliquer une séquence de règles d'élimination sur un hypothèse donnée. Dans la cas d'elim, cette séquence d'élimination doit aboutir à prouver le but courant alors que dans le cas d'apply on produit une nouvelle formule qui vient s'ajouter aux hypothèses.
De plus, on peut donner des arguments optionnels à ces commandes pour préciser la règle d'élimination (par exemple la valeur d'une variable dans l'élimination d'un quantificateur).
elim False correspond à la règle d'absurdité intuitionniste.
by_absurd correspond à la règle d'absurdité classique.
instance pour la règle d'introduction du et la règle d'élimination du . On doit normalement préciser la valeur du terme à substituer. Avec PhoX ce n'est pas le cas et le terme inconnu est remplacé par une variable d'unification notée ?1. La commande instance permet de donner une valeur à ces variables d'unification.
trivial pour laisser PhoX terminer seul la preuve.
save pour indiquer que la preuve est terminée.

Guide de lecture des scripts PhoX

Page d'accueil du DNR