Théorème =c plus fine que =s

Contexte

Pour démontrer le Théorème de conservation par calcul n°1 on aurait besoin de prouver certaines propriétés de conservation par =c.

Énoncé

Variables

x,y

Conditions

x et y sont des formules
x =c y

Conclusion

x =s y

Preuve

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 et y sont des formules telles que x =c y et I x y ≤ n, alors x =s y.

Prouvons P 0 :

Soit x et y vériviant les conditions de P 0. On a x = y, et donc x =s 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 :

d'après la définition de =s on a x =s y.

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

Par récurrence on a xc1 =s y. x et xc1 ont la même calculabilité et éventuel calcul terminal, donc d'après la définition de =s, on a x =s y.

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

Raisonnement similaire à celui ci-dessus.

- 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 :

Comme les niveaux de (x1,y1) et (x2,y2) sont ≤n, par récurrence la propriété est vraie pour ces couples et donc on a x1 =s y1 et x2 =s y2. Par le théorème des calculs et de l'égalité structurel, on a x1 +f x2 =s y1 +f y2, donc x =s y.

CQFD

Recherche d'une preuve

Essai 6

On reprend l'essai 5 pour le nétoyer.
Voir la preuve.

Essai 5

Contexte

L'essai 4 a un problème pour l'index de la récurrence. Il faut changer la définition de =s pour qu'elle ne fasse plus appel à =c. Il faut trouver un index de récurrence adapté.

Nouvelle définition de =s

Contexte : L'égalité structurelle entre deux formules représente une égalité se trouvant entre le syntaxique (où l'on a juste à comparer les formules sans calcul) et la sémantique (où il faut rechercher des preuves).

Def x =s y :

La calculabilité de x et y est identique.
Si x ou y est calculable, soit xc et yc leur calcul respectif, on a la disjonction :
- xc et yc sont des mots et xc = yc
- xc et yc sont des applications xca +f xcb et yca +f ycb et on a xca =s yca et xcb =s ycb

Remarque : Si x =s y alors hormis les sous-parties incalculables les deux formules sont identiques. Par exemple s'il n'y a pas de sous-formule incalculable on a x = y.

Recherche de l'index de la récurrence

Avec cette définition de =s, il reste les contraintes suivantes pour l'indexation de la récurrence :

cas 2 ou 3 de =c : Il faut que xc1 (resp. yc1) soit d'un niveau inférieur à x (resp. y).
cas 4 de =c : il faut que x1,x2,y1,y2 soient de niveau inférieur.

Ce qui ne marche pas :

La profondeur des formules : car xc1 peut être plus profond (avec distribute).
Le nombre de 1-calcul jusqu'au calcul terminal : car la formule peut être incalculable.

Candidats :

le niveau de (x,y) (le nombre minimum de règles de calcul de =c à appliquer pour prouver x =c y).

Essai de démonstration

Soit O n x y défini par la conjonction :

le niveau

de (x,y) est ≤n

si x =c y alors x =s y

Soit P n défini par la conjonction : P n = Pour toute formule x et y tq le niveau de (x,y) soit ≤n on a O n x y

Montrons P 0 :

Comme (x,y) est de niveau 0 on a x = y. On a vu que =c est une relation réflexive et on voit facilement que =s est une relation réflexive. Donc on voit que l'on obtient la conclusion voulue.

Supposons que P n soit démontré et montrons P \ n+1 pour deux formules x et y de profondeurs ≤n+1 :

Nous divisons la démonstration suivant les cas de la disjonction d'où provient x =c y :

1) On a x = y, on a vu que =c est une relation réflexive et on voit facilement que =s est une relation réflexive. Donc on voit que l'on obtient la conclusion voulue.

2) Il existe xc1 tq x →c1 xc1 et xc1 =c y. Il est évident que x et xc1 ont la même calculabilité et éventuel calcul terminal. Comme (xc1,y) est de niveau inférieur, on peut appliquer la récurrence. La propriété étant vraie pour (xc1,y), elle l'est aussi pour (x,y).

3) Il existe yc1 tq y →c1 yc1 et x =c yc1. On fait le raisonnement symétrique du 2.

CQFD

Essai 4

Contexte

L'essai 3 me semble fonctionnel, mais le théorème n'est pas assez puissant. Il faudrait pouvoir déduire que les sous-parties sont égales par calcul. Donc il semble bien de renforcer la propriété "=s" pour faire déduire des égalités par calcul dans le cas de l'application, comme ceci :
Si xc ou yc est une application alors les deux sont des applications, soit x1,x2,y1,y2 tq x = x1 +f x2 et y = y1 +f y2. On a alors x1 =c x2 et y1 =c y2.
Mais pour cela il faudrait que =s et =c soient identiques car =s perd de l'information sur les formules incalculables, ce qui empêche de déduire une égalité par calcul comme on le voudrait.
Il faudrait donc :

Définir =s ainsi :

x =s y ssi : x et y sont ensemble soit une application ou un mot. Si l'un est un mot, l'autre lui est égal. On a x1 =s y1 et x2 =c y2.

Que l'énnoncer du théorème soit le suivant :

Pour x,y deux formules, si x =c y alors:

- la calculabilité de x et y est identique
- si x ou y est calculable, soit xc et yc leur calculs, on a xc =s yc

Recherche de démonstration

Le critère de récurrence devrait se baser sur le nombre de 1-calcul pour arriver au calcul terminé, peut être pas de l'expression entière mais le max de la partie fonction et argument (récursivement ?).
Ou alors le critère de récurrence est la profondeur max des formules x et y.

Canevas de la démonstration:

Si on a montré pour une profondeur n:
Si x ou y est une application, le cas difficile est le cas 4 : x et y sont des applications x1 +f x2 et y1 +f y2 et que l'on a x1 =c y1 et x2 =c y2. Par récurrence (préciser) on a la propriété sur (x1,y1) et (x2,y2). Si x1 ou y1 est incalculable alors les deux le sont, ainsi que x et y. Reste donc à prouver la propriété pour le cas où x1 et y1 sont calculables. Soit x1c et x2c leur calcul respectif. En résumé: x1c et x2c sont similaires, et traitent donc x2 et y2 pareil. x2 et y2 sont ensemble soit incalculables soit calculables. S'ils sont calculables, si l'un vaut 0b ou 1b, l'autre a la même valeur.

Il nous faut un théorème sur les structures : si x =s y, alors leurs fonctions minimales sont égales et leurs arguments sont en même nombre et deux à deux égaux par calcul.

Essai de démonstration

Soit P défini par : P n = Pour toute formules x et y tq le niveau de (x,y) soit ≤n, si x =c y alors :

la calculabilité de x et y est identique
si x ou y est calculable, soit xc et yc leur calculs, on a xc =s yc

Montrons P 1 : à faire

Supposons que P n soit démontré et montrons P \ n+1 pour deux formules x et y de profondeurs ≤n+1 :

Nous divisons la démonstration suivant les cas de la disjonction d'où provient x =c y :

1) On a x = y, on a vu que =c est une relation réflexive et on voit facilement que =s est une relation réflexive. Donc on voit que l'on obtient la conclusion voulue.

2) Il existe xc1 tq x →c1 xc1 et xc1 =c y. Il est évident que x et xc1 ont la même calculabilité et calcul terminal. Comme (xc1,y) est de niveau inférieur, on peut appliquer la récurrence. La propriété étant vraie pour (xc1,y), elle l'est aussi pour (x,y).

3) Il existe yc1 tq y →c1 yc1 et x =c yc1. On fait le raisonnement symétrique du 2.

4) x et y sont des applications x1 +f x2 et y1 +f y2 et on a x1 =c y1 et x2 =c y2. Comme les niveaux de (x1,y1) et (x2,y2) sont ≤n, par récurrence la propriété est vraie pour ces couples. Si x1 ou y1 est incalculable alors x1 et y1 le sont, ce qui implique que x et y le sont et dans ce cas la propriété est vraie pour (x,y). Plaçons nous dans le cas où x1 et y1 sont calculables, soit x1c et y1c leur calcul respectif, on a x1c =s y1c.
Problème pour les calculs car on ne peut pas appliquer la récurrence sur les arguments dans x1c et y1c.

Est-ce que le "niveau" pourrait être le maximum des nombres de calcul jusqu'au calcul terminal pour tous les arguments et la formules entière, récursivement, qui ne sont pas incalculables ?

- Il faut que xc1 soit d'un niveau inférieur à x, donc on ne peut pas traiter le niveau des arguments à égalité avec le niveau général.
- il faut que la contrainte du niveau s'applique aux arguments car on doit pouvoir utiliser l'hypothèse de récurrence dessus.

Remarque: si la définition de =s ne fait pas appel à =c, alors on peut avoir un critère non récursif.

Essai 3

Contexte

Lors de l'essai 1 on voit que l'on a besoin d'une hypothèse de récurrence encore plus forte et définie récursivement.

Pour deux formules x,y on définit x =s y par :

Si x ou y est calculable alors x et y sont calculables. Dans ce cas soit xc et yc le résultat de leur calcul respectif, on a alors :

Si xc ou yc est un mot alors xc = yc.
Si xc ou yc est une application alors les deux sont des applications, soit x1,x2,y1,y2 tq x = x1 +f x2 et y = y1 +f y2. On a alors x1 =s x2 et y1 =s y2.

Le théorème devient en conclusion : x =s y

On montre la propriété par récurrence sur le niveau de l'égalité par calcul.

Montrer que la propriété est vérifiée pour le n de départ.

Si la propriété est vérifiée au niveau ≤n, soit x,y tq x =c y où (x,y) est de niveau n+1. Suivant le cas d'où provient l'égalité par calcul :

impossible, car le niveau serait <n+1.
On a xc1 =c y et (xc1,y) est de niveau ≤n, donc xc1 =s y. La calculabilité de xc1 est la même que la calculabilité de x, et comme xc1 =s y, la calculabilité de x et y sont les mêmes. Supposons que x ou y est calculable. Soit xc et yc le résultat de leur calcul. Comme xc est aussi le résultat du calcul de xc1, on a x =s y.
Toutes les propriétés sont symétriques en x et y, donc le raisonnement du cas 2, adapté à la symétrie, reste valide.
x et y sont des applications x1 +f x2 et y1 +f y2 et on a x1 =c y1 et x2 =c y2. Comme (x1,y1) et (x2,y2) sont de niveau inférieur on a x1 =s y1 et x2 =s y2. D'après le théorème =s et calcul, on déduit x =s y.

Remarque : la démonstration me semble correcte, il reste à copier et compléter dans la section Preuve.

Essai 2

Contexte

Lors de l'essai 1 on voit que l'on a besoin d'une hypothèse de récurrence plus forte.

Hypothèse de récurrence : comme le théorème avec en plus que si x se calcul en un mot alors y se calcul en ce même mot.
Mais comment montrer que pour la partie fonction, on a le même calcul ? Il faut encore renforcer l'hypothèse de récurrence en ajoutant que si la formule est une application alors la propriété est vraie aussi pour les sous-parties. Il faut donc définir la propriété comme une relation pour pouvoir la définir récursivement.

Essai 1

On montre la propriété par récurrence sur le niveau de l'égalité par calcul.

évident.
xc1 est calculable, par récurrence y l'est (car xc1 =c y et de niveau inférieur)
Par récurrence on déduit que yc1 est calculable, comme y →c1 yc1, y est calculable.
On a besoin que l'argument (x2 et y2) se comportent identiquement par rapport au test du if. On voit que l'on a besoin de prouver que dans une égalité par calcul, si l'un se calcul en un mot alors l'autre se calcul en ce même mot. Il parait intéressant de renforcer la conclusion du théorème.

@theorem