Calcul et remplacement
Contexte
Nous serons amenés à comparer les calcul d'une formule x avec x où une partie est remplacée par une autre (voir le théorème "Recherche:Roadmap:5 Vérif types:4 Définir extensions:1 Mots clés:3 Traduction sans hypothèse:Règle du tiers exclu:Toute vérité se calcule en une égalité:Rebut:Toute vérité se calcule en une égalité". Nous allons voir ici que lors d'un calcul une sous-partie ne peut subir que les traitements suivant:
- duplication et déplacement (par la règle distribute)
- comparaison à 1b ou 0b (argument de if)
- calcul (argument de if ou position de fonction)
Ce qui fait que si on remplace une partie d'une formule par une formule de même calculabilité et, si elle est calculable alors elle est de même résultat de calcul, alors la calculabilité de la formule globale est inchangée.
Remarquons que la valeur syntaxique du résultat du calcul de la formule globale peut être changée: par exemple si dans equal (if 1b 0b 0b) on remplace if 1b 0b 0b par if 0b 0b 0b, le résultat final passe de equal (if 1b 0b 0b) à equal (if 0b 0b 0b).
Énoncé
Conditions
x, y,z et t sont des formules lazi.0.0 telles que
- x =c z
- on a la disjonction:
- x est une fonction constante par calcul
- y =c t
Conclusion
x +f y =c z +f t
Preuve
Nous allons prouver le théorème par récurrence. Soit x,y,z,t tels que dans les conditions.
Calculons x +f y et z +f t pour montrer que x +f y =c z +f t.
On utilise une forme du premier ordre du tiers exclu pour explorer deux cas: x est ou non calculable.
Si x n'est pas calculable alors z n'est pas calculable, donc x +f y et z +f t ne sont pas calculables et on a donc par définition x +f y =c z +f t.
Si x est calculable, soit xc le résultat du calcul de x et zc le résultat du calcul de z. Les calculs de x +f y et z +f t reviennent à calculer xc +f y et zc +f t.
Comme x =c z, nous avons deux cas:
xc = zc
Si le calcul de xc +f y ou xc +f t est terminé, comme la terminaison d'un calcul ne dépend pas de la valeur du dernier argument cela implique que les deux sont des calculs terminés et comme xc =c zc et y =c t, on a x +f y =c z +f t.
Si le calcul de xc +f y n'est pas terminé, alors c'est aussi le cas de zc +f t. Comme l'application d'une règle sur une formule est indépendante du dernier argument, la règle de calcul applicable à xc +f y ou xc +f t est la même.
- indéfiniment, et alors x +f y et z +f t ne sont pas calculables, on a donc x +f y =c z +f t.
- jusqu'à ce que la règle "if 1b" ou "if 0b" puisse s'appliquer, et on a déjà traité ce cas
- la condition du if est calculable mais n'aboutit ni à 0b ni à 1b, le calcul est terminé avec des valeurs de la forme xc2 +f x et xc2 +f y. Comme xc2 =c xc2 et x =c y, on a x +f y =c z +f t.
Si on peut appliquer la récurrence: il nous faut l'appliquer sur le 4-uple (a +f y, b +f y, a +f t, b +f t) et montrer que a +f y =c a +f t et b +f y =c b +f t.
xc et zc sont des applications
Soit xc1 +f xc2 et zc1 +f zc2 ces applications. Par définition de =c, nous avons xc1 =c zc1 et xc2 =c zc2
@todo