Théorème de conservation par calcul n°1
Contexte
La définition de =c (voir essai 4 de Recherche d'une preuve) permet de prouver x =c y si on a xc1 =c y. Mais il parait logique que l'on ait la réciproque (x =c y implique xc1 =c y) car =c est une manière de calculer ce qui est sémentiquement égal.
Énoncé
Variables
x,y,xc1
Conditions
- x, y et xc1 sont des formules
- x →c1 xc1
- x =c y
Conclusion
xc1 =c y
Preuve
Recherche d'une preuve
Essai 3
Contexte
Il y a un problème dans l'essai 2 , soit la démonstration est impossible, soit elle est plus compliquée qu'en adoptant un autre système pour définit =c.
Nouvelle définition de =c
- on définit x →c+ y par : x = y ou x→c y ou x = x1 +f x2, y = y1 +f y2, x1 →c+ y1, x2 →c+ y2
- on définit x =c y par : il existe z tq x →c+ z et y →c+ z
Indexation du calcul par →c+
Il faut définir un nouvel index pour la récurrence. Il ressemblera au précédent, il doit toujours être sur un couple car c'est par rapport à un point d'arrivé du calcul commun.
Pour cela on définit un index pour →c= (le nombre de calcul), pour →c+, puis pour =c. On renomme les index Ice, Icp, I=c
À faire
Il nous faut montrer que si x →c+ y et x →c1 xc1, alors xc1 →c+ y.
Il faut revoir les théorèmes faisant intervenir
Essai 2
Contexte : On reprend l'essai 1 en remetant à jour d'après les dernières modifications.
Nous allons prouver ce théorème par récurrence. Pour cela nous utiliser I comme définit dans le théorème de l'indexation des couples égaux par calcul.
Pour n∈ℕ, soit P n la propriété : si x,xc1 et y sont des formules telles que x =c y, x →c1 xc1 et I x y ≤ n, alors xc1 =c y.
Prouvons P 0 :
Supposons P n et prouvons P (n+1) :
1) x est de la forme $F[ if 1b ] +f xc1 +f x2. On a donc $F[ if 1b ] +f xc1 =c y1.
3) x est de la forme $F[distribute] +f a +f b +f x2
4) x est de la forme $F[ if ] +f a +f b +f x2 où le calcul de a n'est pas terminé.
5) Le calcul de x1 n'est pas terminé, soit x1c1 tq x1 →c1 x1c1.
Essai 1
Si x =c y par le cas 1 :
Si x =c y par le cas 2 :
Si x =c y par le cas 3 :
Si x =c y par le cas 4 :
Comme le résultat du 1-calcul de x est x2, on a xc1 = x2, comme x2 =c y2 on a xc1 =c y2. Donc y1 +f y2 ->c y2. Comme xc1 =c y2, par application multiple du cas 3 de la définition de =c, on a xc1 =c y.
Soit zx le résultat du 1 calcul de x, et zy le résultat du 1-calcul de y1c +f y2.
Pour prouver que zx =c zy, il faudrait peut-être raisonner sur les niveaux et pouvoir utiliser la récurrence ?
@theorem