Lazi

Étude démonstration cas 2 et 4

Contexte

Voir "Recherche d'une preuve / essai 4 / transitivité / cas 2 et 4"
On a xc1 =c y et y et z sont des applications y1 +f y2 et z1 +f z2 avec y1 =c z1 et y2 =c z2.

Question

Comment démontrer pour le cas "2 et 4" ?

Étude

Exemple

x = (if 0b 1b) (0b \ if 0b 0b 1b)
y = 0b (if 0b 0b 1b)
z = 0b (if 1b 1b 1b)
On a x =c y et y =c z

Pour prouver que x =c z, il faut passer par :
x =c 0b (if 0b 0b 1b)

Calculer pour aboutir à une égalité

Soit x et y deux formules telles que x =c y. D'après la définition de =c, cela est équivalent à ce qu'il y ait un calcul sur x, y et leurs sous-parties qui aboutit à la même formule des deux côtés.
On peut représenter ce calcul pour une formule par une arborescence où la racine est le résultat du calcul et où chaque noeud a un ou deux fils: un fils c'est un 1-calcul, deux fils c'est le calcul qui continue sur la fonction et l'argument de la formule.

Si on ne fait la récurrence que sur le niveau du premier couple

On reprend la démonstration de la transitivité, mais en appliquant la récurrence que sur le niveau du premier couple.

On prouve la propriété par récurrence sur le niveau de calcul de (x,y) :

Soit x,y,z tq x =c y et y =c z où le niveau de calcul de (x,y) est ≤1 :

Puisque x =c y, on se trouve dans un des quatres cas de la disjonction définissant =c :

  • Cas 1 : comme x = y, x =c z.
  • cas 2 : on a xc1 =c y et x →c1 xc1. Comme le niveau de (x,y) est 1, on a xc1 = y. Donc x →c1 y et comme on a aussi y =c z, par application de la règle 2, on a x =c z.
  • cas 3 : on a x =c yc1 et y →c1 yc1. Comme le niveau de (x,y) est 1, on a x = yc1. Donc y →c1 x et comme on a aussi y =c z, d'après le théorème de conservation par calcul n°1, on a x =c z.
  • cas 4 : Comme le niveau de (x,y) est 1, on a x1 = y1 et x2 = y2. Donc x = y, donc x =c z.

Si la propriété est prouvée pour les niveaux du premier couple ≤n avec n≥1 :

Soit x,y,z tq x =c y et y =c z où le niveau de calcul de (x,y) est n+1.
Puisque x =c y, on se trouve dans un des quatres cas de la disjonction définissant =c :

  • Cas 1 : impossible car alors on aurait n≤1.
  • Cas 2 : on a xc1 =c y. Comme le niveau de calcul de (xc1,y) est n, par récurrence on déduit xc1 =c z. Par la règle 2, on déduit x =c z.
  • Cas 3 : on a x =c yc1 et y →c1 yc1. D'après le théorème de conservation par calcul n°1, on a yc1 =c z. Comme le niveau de calcul de (x,yc1) est n, par récurrence on déduit x =c z.
  • Cas 4 : on a x1 =c y1 et x2 =c y2 et les niveau de calcul de (x1,y1) et (x2,y2) sont ≤n.
    • Si y =c z par 1 : on a y = z, donc x =c z.
    • Si y =c z par 4 : on a y1 =c z1 et y2 =c z2. Par récurrence on a x1 =c z1 et x2 =c z2. Donc par le cas 4 on a x =c z.
    • Si y =c z par 3 : on a y =c zc1. Si on traite les autres cas, on peut montrer ce cas par récurrence.
    • Si y =c z par 2 : on a yc1 =c z. D'après le théorème de conservation par calcul n°1 on a x =c yc1, mais il faudrait que le niveau ne soit pas augmenté. Dans ce cas on pourrait itérer, mais il faudrait quelque par une décroissance pour qu'il n'y ait pas de boucle.

Réponse