Lazi

Théorème toute vérité lazi.0.0 + ajout

Contexte

Pour les traductions des mots clés forAll, exists, imply nous avons besoin de légèrement généraliser le théorème "toute vérité lazi.0.0 se calcule en une égalité" en y ajoutant des déductions d'ajout.

Énoncé

Variables

p,a,m

Condition

  • m est la mathématique lazi.0.0 à laquelle on a ajouté des règles de déductions (dites "supplémentaires") déduisant une vérité qui est une application et où la fonction minimale est un mot clé non lazi.0.0.
  • p est une preuve m sans condition
  • a est la vérité déduite par p

Conclusion

Il existe b tq a →c[univocal] b
b est une application.
Soit f la fonction minimale de b.
Si f est le mot "equal" alors :

  • il existe une sous-preuve lazi.0.0 q de p tq l'objet de q soit a.
  • il existe des formules b1,b2 tq :
    • b = (b1 *=* b2)
    • b1 =c b2
Sinon f est l'un des mots clés ajoutés à lazi.0.0 et il existe une preuve composée de déductions de p tq :
  • l'objet de q est a
  • la longeur de q est ≤ à la longeur de p
  • la première déduction d de q provient d'une règle supplémentaire et le reste des déductions sont lazi.0.0
  • si b est de la forme f +f b1 +f ... +f bn alors la formule déduite par d est de la forme f +f c1 +f ... +f cn et l'on a pour 1 ≤ k ≤ n bk =c ck

Preuve

Elle est similaire à la preuve du théorème "toute vérité lazi.0.0 se calcule en une égalité".
Nous démontrons le théorème par récurrence sur la longueur de la preuve p.

Preuve du théorème pour les preuves de longueur 1

Nous étudierons le cas un peu plus général où la dernière déduction n'a pas de condition. C'est toujours le cas pour les preuves de longueur 1 car pour qu'il y ait une condition il faut au moins une autre déduction précédant la déduction (rappelons que p est sans condition).

Si la déduction provient d'une régle supplémentaire, alors la conclusion est évidente.
Sinon l'unique déduction provient de l'une des deux règle "if" ou de la règle "distribute". Donc elle déduit une égalité. Donc a se univocal-calcule en une égalité a1 *=* a2 puisque c'est une égalité et un calcul terminé.

Comme a1 →c[univocal]1 a2, on a a1 →c[loose] a2 donc on a a1 =c a2.

Si le théorème est montré pour les preuves de longueur < n

Soit p une preuve de longueur n. Soit d la dernière déduction de p. Nous avons déjà prouvé les conclusions si la dernière déduction de p n'a pas de condition. Il nous reste à traiter les autres cas:

Si d est une déduction "arguments égaux"

a se calcul en une égalité puisque c'est une égalité de la forme z +f x *=* z +f y.

Comme x *=* y est une condition de la déduction, elle est démontrée par p, donc on peut extraire de p une preuve lazi.0.0 q de longueur < n de cette condition. Donc par récurrence on déduit x =c y. Donc il existe t tq x →c[loose]= t et y →c[loose]= t. De par les règles du calcul loose, on déduit que z +f x →c[loose]= z +f t et z +f y →c[loose]= z +f t, donc par définition de =c on a z +f x =c z +f y.
Si on ajoute d à la fin de q on a une sous-preuve lazi.0.0 de p déduisant a.

Si d est une déduction "fonction égale"

La démonstration est similaire au cas "arguments égaux".

Si d est une déduction "égalité et vérité"

Soit x et y les variables de la déduction, donc p prouve x et x *=* y. D'autre part, comme a est par hypothèse la conclusion de la déduction on a y = a.

p contient une sous-preuve de longueur < n de x, donc par récurrence nous avons deux cas :

Cas 1, de l'égalité

Il existe x1,x2 tq x →c[univocal] (x1 *=* x2) avec x1 =c x2, ce qui implique x =c (x1 *=* x2).
p contient une sous-preuve q lazi.0.0 de longueur < n de x *=* y, donc par récurrence on a x =c y.

Comme =c est une relation d'équivalence, de x =c (x1 *=* x2) et x =c y on déduit y =c (x1 *=* x2).

Comme on a y =c (x1 *=* x2), d'après le théorème d'égalité des arguments pour un calcul terminé , il existe y1 et y2 tq :

  • y →c[univocal] (y1 *=* y2)
  • y1 =c x1
  • y2 =c x2

Comme x1 =c x2, x1 =c y1 et x2 =c y2, =c étant une relation d'équivalence on déduit y1 =c y2.

Comme y = a, a se univocal-calcule en une égalité y1 *=* y2 et y1 =c y2.

Il nous reste à montrer qu'il existe une sous-preuve lazi.0.0 de p ayant a pour objet :

Comme x est prouvé par p et que x se univocal-calcule en une égalité, par récurrence il existe une sous-preuve r lazi.0.0 de longueur < n de x. En concaténant q et r et en y ajoutant d à la fin, nous obtenons une preuve lazi.0.0 de a.

Cas 2, de la règle supplémentaire

Il existe une application b tq x →c[univocal] b.
f est l'un des mots clés ajoutés à lazi.0.0 et par récurrence il existe une sous-preuve q de p tq :

  • la première déduction e de q provient d'une règle supplémentaire et le reste des déductions sont des déductions lazi.0.0
  • si b est de la forme f +f b1 +f ... +f bn alors la formule déduite par e est de la forme f +f c1 +f ... +f cn et l'on a pour 1 ≤ k ≤ n bk =c ck
On a donc x =c f +f b1 +f ... +f bn =c f +f c1 +f ... +f cn.

p contient une sous-preuve de longueur < n de x *=* y, donc par récurrence il existe une sous-preuve lazi.0.0 r de p de longueur < n prouvant x *=* y, de plus on a x =c y.

Soit s la concaténation de q et r où l'on ajoute d à la fin et où l'on enlève les déductions identiques. s est une preuve dans m de a, cette preuve n'a qu'une déduction (e) provenant d'une règle supplémentaire, qui est au début. Comme s n'a pas de duplication de déductions et que toutes ses déductions proviennent de p, sa longeur est ≤ p.

Comme =c est une relation d'équivalence on déduit y =c f +f c1 +f ... +f cn.
D'après le théorème du calcul loose vers univocal , il existe d1,...,dn tq :

  • y →c[univocal] (f +f d1 +f ... +f dn)
  • pour 1 ≤ k ≤ n : dk →c[loose] ck

Donc a (a=y) se univocal-calcul en une formule f +f d1 +f ... +f dn, la formule déduite par e est f +f c1 +f ... +f cn et pour 1 ≤ k ≤ n on a ck =c dk