Lazi

Validité de l'extension

Contexte

Les déductions permettant d'ajouter les mots clés forAll, exists, and, or, imply sont toutes dans la même extension car la traduction est faite pour toutes les déductions en même temps. On a besoin de vérifier que l'extension est valide. On fournira plus tard une preuve formelle en Lazi, il s'agit ici de fournir une preuve sous forme informelle.

Question

L'extension est-elle valide ?

Étude

Domaine en tant qu'extension

Le domaine, en tant qu'extension (le "dom" de la règle d'extension), est défini comme le domaine de la mathématique de l'extension réduit aux déduction traduisibles. Ici nous ne pourront traduire que si la conclusion ne comporte pas un mot clé de l'extension et si la déduction est sans hypothèse.

Cette dernière condition vient du fait que l'on ne peut pas traduire :

  • si on se trouve sous une hypothèse absurde, car alors certaines propriétés de la preuve ne sont plus forcément respectées,
  • ou s'il manque des informations comme une déduction d'ajout, car la traduction des déductions d'applications peuvent nécessiter des informations de la déduction d'ajout correspondante.

Remarquons que ces deux conditions ne sont d'aucune gêne.

Bestiaire

Voir la page spéciale des "cas".

Les traductions à effectuer

Comme on ne peut pas traduire s'il y a des hypothèses, il faut traduire vers Lazi.0.0.

Les traductions suivantes sont à effectuer, l'ordre peut compter:

  • excludedMiddleRuleT, inductionRuleT ou extensionT
  • éventuellement: remplacer les sous-proofT par le contenu
  • les déductions d'application
  • les déductions d'ajout
  • les déductions déduisant une vérités où la fonction principale est un mot clé Lazi.1 sont détruites
  • les mots clés Lazi.1 sont remplacée par une valeur quelconque (par exemple 1b) dans les déductions restantes.

Quelle récurrence utiliser ?

Voir la page spéciale.

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 pouvons d'abord la transformer en preuve ne contenant qu'une seule déduction.

On définit tr = tr2 ∘ tr1
tr1 sera la fonction traduisant la plupart des déductions
tr2 sera la fonction de remplacement des mots clés Lazi.1

tr1 parcourt la liste des déductions de p en commençant par la fin, si le type de la déduction d est :

  • proofT : on remplace d par le contenu de la preuve, puis on réaplique tr1 sur la preuve globale obtenue.
  • si t est excludedMiddleRuleT, inductionRuleT ou extensionT : on remplace la déduction par sa traduction, puis on réaplique tr sur la preuve globale obtenue.
  • si t est une déduction d'ajout

Réponse