Lazi

Arguments égaux par calcul

Contexte

Nous allons montrer ici que deux formules égales par calcul se comportent de manière identiques du point du vue du calcul. Si on voit ça du point de vue informatique, la notion "égal par calcul" est la notion d'équivalence calculatoire des fonction pure si on considère qu'une boucle infinie est équivalente à une autre.

Nous nous servirons de ce résultat pour le théorème "Toute vérité se calcule en une égalité".

Remarquons que l'on peut facilement étendre ce résultat à divers cas, par exemple: si x1 =c x2 et y1 =c y2 alors x1 +f y1 =c x2 +f y2 : on applique deux fois le théorème avec des "a" adaptés.

Énoncé

Variables

a, b, c

Conditions

  • a, b et c sont des formules
  • b =c c

Conclusion

a +f b =c a +f c

Étude

Recherche d'une preuve

Preuve

Si b ou c est un mot

Dans ce cas comme b =c c, d'après la définition de =c, on déduit b = c, et donc comme =c est réfléxif, on a a +f b =c a +f c.

Si b ou c n'est pas un mot

Soit x une variable inutilisée par les formules a,b et c.

Nous allons montrer que le calcul de a +f x est équivalent (notion d'équivalence à préciser) à a +f b et a +f c. De là nous déduirons que les calculs de a +f b et a +f c sont équivalent. (Comment de là aboutir à a +f b =c a +f c ?)