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 :
Supposons P n et prouvons P (n+1) :
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
- 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 :
Supposons que P n soit démontré et montrons P \ n+1 pour deux formules x et y de profondeurs ≤n+1 :
CQFD
Essai 4
Contexte
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 :
- 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 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 :
Problème pour les calculs car on ne peut pas appliquer la récurrence sur les arguments dans x1c et y1c.
- il faut que la contrainte du niveau s'applique aux arguments car on doit pouvoir utiliser l'hypothèse de récurrence dessus.
Essai 3
Contexte
Pour deux formules x,y on définit x =s y par :
- 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
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