Lazi

essai 1

Arguments égaux par calcul

Contexte

Nous allons montrer ici que deux formules égales par calcul se comportent de manière identiques en tant qu'argument dans un calcul. Nous nous servirons de ce résultat pour 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:essai 1:Rebut:Toute vérité se calcule en une égalité".

Énoncé

Variables

a, b, c

Conditions

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

Conclusion

a +f b =c a +f c

Présentation de la preuve

Lors d'un calcul une partie d'une formule (comme b dans a +f b) ne peut être que soit:

  • déplacée ou copiée
  • évaluée pour être testée par if
  • évaluée en tant que fonction

Le déplacement ou la copie ne différencie pas les différentes parties.

Une partie incalculable, pour chacun des 3 cas, ne peut être différenciée d'une autre partie incalculable, ce qui fait que l'on peut voir les parties incalculables comme équivalentes, ce que fait l'égalité par calcul.

Deux parties égales par calcul ne peuvent se différencier que par les sous-formules incalculables. Hors comme elles sont indistinguables l'une de l'autre du point de vue du calcul, cela implique que les deux parties égales par calcul sont indistinguables dans le calcul, les deux calculs sont donc identiques et les formules produites ne sont différentes que par les sous-formules incalculables. Elles sont donc égales par calcul.

Preuve

Pour prouver a +f b =c a +f c, nous allons supposer que a +f b est calculable et prouver que le calcul de a +f c est similaire à celui de a +f b. Pour cela nous allons montrer une propriété par récurrence sur la longueur du calcul de a +f b.

Pour deux formules x et y soit "x =s y" définie par :

  • x = y ou
  • x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1 et x2 =c y2

Remarque =s est comme =c moins la condition sur la calculabilité.

La propriété prouvée par récurrence est "=s" appliquée aux deux formules calculées.

Si le calcul est de longueur nul

Cela implique que a +f b est un calcul terminé.
D'après le théorème "La terminaison d'un calcul est indépendante du dernier argument" on déduit que a +f c est un calcul terminé.
Il nous reste à montrer que a +f b =s a +f c. Pour cela nous montrerons directement la deuxième condition de la disjonction définissant "=s". Comme =c est réflexive on a a =c a, par hypothèse on a b =c c. Donc on a a +f b =s a +f c.

Si la propriété est montrée pour les calculs de longueur <n

Soit a,b,c tels que a +f b soit calculable en un calcul de longueur n.