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 :
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 :
- 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)
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 la propriété est vraie jusqu'aux SFP de longeur n et que le SFP est de longueur n + 1 :
CQFD