Théorème de la preuve de l'égalité par calcul

Contexte

Le théorème "toute vérité lazi.0.0 se calcule en une égalité" établit un lien allant d'une verité vers un calcul loose. Ici nous allons donner une réciproque : si x =c y alors x et y sont sémantiquement égaux.

Énoncé

Variables

m,x,y

Conditions

m est une mathématique étandant lazi.0.0
x et y sont des formules pour m
x =c y

Conclusion

Soit mf = lazi.0.0 plus le type des formules de m.
Il existe une preuve dans mf et sans condition de x *=* y.

Preuve

Comme l'égalité sémantique est une relation d'équivalence (voir lazi/mathematic/02-tools-to-prove/05-equality.deduc.lazi), il suffit de montrer que si a →c[loose]1 b alors il existe une preuve de a *=*b.

Comme un calcul loose est un calcul univocal à un certain endroit de la formule, nous allons déjà montrer que les calculs univocaux se transcrivent en preuve.

Soit au et bu deux formules tq qu'il existe un calcul univocal c de longueur 1 tq calculate univocal c au = bu. Nous allons prouver qu'il existe une preuve en de au *=* bu par récurrence sur la profondeur de au :

Si la règle appliquée est la règle 1 à 3 : la preuve est consituée de la déduction correspondante : "if 1b" , "if 0b" , "distribute"
au ne peut être de profondeur < 3 car alors aucun calcul n'est possible.
Si au est de profondeur 3 : alors seuls les règles de 1 à 3 sont applicables et nous avons déjà traité ce cas.
Si pour n ≥ 3 au est de profondeur n+1 et que le théorème est montré pour les formules de profondeur ≤ n :

Si le calcul utilise la règle n° :

- 1 à 3 : le cas est déjà traité
- 4 : Comme la condition du if est de profondeur ≤ n il existe une preuve q traduisant le calcul. On ajoute alors les "if" z et t de la règle en ajoutant à q les déductions :

arguments égaux (avec "if" et la condition)
fonctions égales (avec l'égalité précédente et z)
fonctions égales (avec l'égalité précédente et t)

-5 : raisonnement similaire au cas 4

Il nous reste à montrer qu'un calcul loose élémentaire se traduit en preuve. Nous allons le montrer par récurrence sur la longueur du SFP (un SFP est représenté par une liste binaire) représentant le calcul élémentaire.

Si le SFP est de longueur 0 : alors le calcul est équivalent à un calcul univocal, on a donc déjà le résultat par la propriété précédemment démontrée.
Si la propriété est vraie jusqu'aux SFP de longeur n et que le SFP est de longueur n + 1 :

- Si le premier élément de la liste est un 0b :

Par récurrence il existe q la preuve correspondant au calcul élémentaire représenté par le SFP moins son premier élément et appliqué sur la partie fonction de la formule. Soit p la preuve constituée de q suivie de la déduction "fonction égale" appliqué à l'égalité déduite par q et pour l'argument celui de la formule. p est alors la preuve correspondant au SFP.

- Si le premier élément de la liste est un 1b :

La preuve est symétrique function/argument par rapport au cas précédent.

CQFD