Lazi

Essais 1

Définition de la fonction de traduction

Nous allons définir la fonction tr de traduction d'une preuve p. Si nous avons une déduction à traduire qui n'est pas une preuve, nous pouvous d'abord la transformer en preuve ne contenant qu'une seule déduction.

On définit tr = tr2 ∘ tr1
tr1 sera la fonction traduisant les déductions d'application.
tr2 sera la fonction d'élimination des déductions d'ajout et de remplacement des mots clés Lazi.1.

Définition de tr1

tr1 parcours la liste des déductions en commançant par le début et éxécute les remplacements suivants. Soit d la déduction examinée et t son type :

  • si t est proofT : on remplace d par le contenu de la preuve puis on continue à cet emplacement (donc sur la première déduction de la sous-preuve).
  • si t est excludedMiddleRuleT, inductionRuleT ou extensionT : la déduction est traduite, puis on reprend au début de la traduction obtenue.
  • si t est l'une des déductions d'application: on retrouve, dans la preuve déjà traduite par tr1, la déduction d'ajout correspondante, puis on remplace la déduction par la traduction prévue par le type, puis on se positionne sur le résultat de cette traduction.
  • sinon: la déduction reste inchangée.

Définition de tr2

tr2 parcours la liste des déductions en commançant par le début et éxécute les remplacements suivants. Soit d la déduction examinée et t son type :

  • si t est proofT : on remplace d par le contenu de la preuve puis on continue à cet emplacement.
  • si t est une déduction d'ajout: elle est détruite
  • sinon les mots clés Lazi.1 des formules en argument de la déduciton sont remplacés par 1b (n'importe quelle valeur conviendrait).

Validité de tr1 p

Nous montrerons ici que tr1 p est une preuve Lazi.1 sans déduction d'application autres que celles se trouvant dans des sous-preuves de déductions d'ajout.

L'élimination des déductions d'application est évidente puisque tr1 parcourt p en remplaçant les déductions d'application.

La preuve que la traduction d'une déduction de p ne change pas la validité en tant que preuve Lazi.1 se trouve dans la documentation de la déduction à traduire.

Il reste donc à prouver la finitude de tr1 p. Cette question n'est pas évidente car le résultat de la traduction d'une déduction de p par tr1 est lui-même retraduit par tr1 quand celui-ci est une preuve (par exemple pour la traduction de la déduction d'application de "∀").

Nous allons déjà définir une mesure M sur les preuves Lazi.1. Elle nous servira a prouver la décroissance de la mesure de la preuve lors de la traduction.

Si x est une preuve, nous définissons la profondeur de x "pr x" par la profondeur maximale relativement aux sous-preuves des déductions. Une preuve sans sous-preuve a une profondeur de 1, si elle contient des déductions ayant des sous-preuves pr x est 1 + le max des pronfondeurs des sous-preuves.

Si x est une preuve Lazi.1, M x est un pr x uple d'entiers :
( nombre de déductions de x de profondeur pr x, nombre de déductions de x de profondeur pr x - 1, ...
, nombre de déductions de x de profondeur 1)

On définit un ordre total > sur les mesures des preuves par :
soit x, y deux preuves Lazi.1, x ≥ y ssi

  • pr x > pr y
  • ou pr x = pr y et M x est suppérieur ou égal à M y suivant l'ordre lexicographique.

Pour prouver que tr1 p est fini, nous montrerons que chaque étape dans la traduction a une mesure inférieure ou égale à la preuve traduite.

On divise en 4 cas l'action de tr1 sur la déduction à traduire :

  • Si le remplacement n'est pas par une preuve, alors la mesure de la preuve ne change pas.
  • S'il s'agit de la traduction de proofT, excludedMiddleRuleT, inductionRuleT ou extensionT : le remplacement est par une preuve q déjà valide et avec toutes ses conditions de prouvée à la place de la traduction. Comme le remplacement diminue la profondeur de la déduction traduite, la mesure globale de la preuve traduite est strictement inférieure.
  • S'il s'agit de la traduction d'une déduction d'application où la preuve q est déjà valide et a toutes ses conditions déjà prouvée à la place de la déduction d'ajout : Alors la traduction de q ne se fait que par des références à la preuve se trouvant au dessus de la déduction d'où provient q (par construction de la fonction de recherche des déductions d'ajout). On peut donc traduire q dans une preuve plus courte que celle de départ, et donc par récurrence la traduction de q par tr1 est valide.
  • Sinon on traduit la déduction d'application de l'implication. Voir la page spéciale pour ce cas.