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 :

Soit x et y vériviant les conditions de P 0. On a x = y, donc y→c1 xc1. D'après la règle 3 de =c, comme xc1 =c xc1 et y→c1 xc1, on a xc1 =c y.

Supposons P n et prouvons P (n+1) :

Soit x et y vériviant les conditions de P (n+1). D'après les propriétés de I on a la disjonction :

- x = y :

alors I x y = 0 et d'après P 0 on a xc1 =c y.

- xc1 =c y (le 1-calcul de x est xc1) et I xc1 y ≤ n :

Dans ce cas on a directement la conclusion recherchée (xc1 =c y).

- il existe yc1 tq y →c1 yc1 et x =c yc1 et I x yc1 ≤ n :

En appliquant P n à x yc1, on a xc1 =c yc1. D'après la règle 3 de =c, on a xc1 =c y.

- x et y sont des applications x1 +f x2 et y1 +f y2 avec x1 =c y1, x2 =c y2, I x1 y1 ≤ n et I x2 y2 ≤ n :

On a la disjonction, suivant la règle du 1-calcul de x ( x →c1 xc1) :
1) x est de la forme $F[ if 1b ] +f xc1 +f x2. On a donc $F[ if 1b ] +f xc1 =c y1.

Comme $F[ if 1b ] +f xc1 est un calcul terminé, $F[ if 1b ] +f xc1 =c y1 ne peut être déduite que des règles 1,3 et 4. Par récurrence on montre que y1 est de la forme $F[ if 1b ] +f a où xc1 =c a. Par la règle 4 de =c, on déduit xc1 =c $F[ if 1b ] +f a +f y2. Puis en réappliquant les règles 1,3 et 4 en ordre inverse qui s'appliquait sur y1, on déduit ? sur $F[ if 1b ] +f a on décuit xc1 =c y1 +f y2.

2) x est de la forme $F[ if 0b ] +f a +f x2. On a donc xc1 = x2.
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.

On a donc xc1 = x1c1 +f x2. Par P n avec x1 et y1 on a x1c1 =c y1. D'après la règle 4 de =c, on a x1c1 +f x2 =c y1 +f y2, donc xc1 =c y.

Essai 1

Si x =c y par le cas 1 :

On a alors x = y, donc xc1 =c yc1, et par la règle 3 on a xc1 =c y.

Si x =c y par le cas 2 :

On a alors directement xc1 =c y.

Si x =c y par le cas 3 :

On a alors x =c yc1. Si on raisonne par récurrence sur le niveau (x,y), on déduit xc1 =c yc1 et par le cas 3 xc1 =c y.

Si x =c y par le cas 4 :

On a x1 =c y1 et x2 =c y2. On a la disjonction, suivant la règle du 1-calcul entre x et xc1 :

Si xc1 laisse intacte x2, i.e. le 1-calcul de x ne toutche pas à l'argument (x2).

Si on raisonne par récurrence sur le niveau (x,y), on a x1c1 =c y1, donc x1c1 +f x2 =c y1 +f y2, donc xc1 =c y.

Dans le cas contraire.

On ne peut être que dans le cas de la règle 1,2 ou 3 du 1-calcul.

Si c'est la règle 2 :

Comme x1 est un calcul terminé et que x1 =c y1, d'après théorème =c plus fine que =s, y1 est calculable et si y1c est le résultat du calcul de y1, on a x1 =s y1c.
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.

Si c'est la règle 1 :

Comme x1 est un calcul terminé et que x1 =c y1, d'après théorème =c plus fine que =s, y1 est calculable et si y1c est le résultat du calcul de y1, on a x1 =s y1c.
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