Lazi

essai 6

Toute vérité se calcule en une égalité

Contexte

Pour raisonner par récurrence sur les preuves lazi.0.0, nous allons déjà trouver des propriétés de base sur les vérités de cette mathématique.

Ce théorème peut se transcrire ainsi en langage courant: au fond les seules vérités sont des égalités. Remarquons que l'égalité renferme toute la complexité de l'existence, par exemple on peut se demander si la fonction "il existe une preuve de" (cette fonction peut tester toutes les preuves possibles) retourne 1b avec comme argument l'énnoncé d'un théorème très complexe.
Ce théorème exprime aussi que deux choses égales sont soit toutes les deux calculables, soit toutes les deux incalculables. De plus si elles sont calculables, en les calculant on obtient une certaine partie fonction syntaxiquement identique et des arguments égaux par calcul.

Énoncé

Condition

p est une preuve lazi.0.0 sans condition et x la conclusion de p.

Conclusions

  • x se calcul en une égalité x1 *=* x2
  • on a x1 =c x2

Démonstration

Recherche d'un contre-exemple (non abouti)

Nous démontrons le théorème par récurrence sur la longueur de la preuve p.

Si la longueur de p est 1

Alors l'unique déduction ne peut avoir de condition, c'est donc l'application de l'une des deux règle "if" ou de la règle "distribute". Donc elle déduit une égalité. Comme le calcul des deux membres de l'égalité aboutit au même calcul, les autres conclusions sont vérifiées:

  • si un des membres est calculable alors l'autre aussi
  • les calculs des deux membres sont syntaxiquement identiques et vérifient donc la relation "=c"

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.

Si d est une déduction provenant des 3 règles sans condition

On peut utiliser le même raisonnement que pour le cas où la longueur de p est 1.

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

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

Comme la vérité b *=* c est prouvée par une preuve strictement plus courte que p, par récurrence on déduit b =c c.
Le théorème "Calcul et remplacement" s'applique, et l'on a donc a +f b =c a +f c.

Si d est une déduction "fonctions égales"

x se calcul en une égalité puisque c'est une égalité de la forme b +f a *=* c +f a. Comme b *=* c est démontré par une troncature stricte de p et se calcul en lui-même, on peut appliquer l'hypothèse de récurrence et on obtient b *=s* c. D'autre part il existe une preuve lazi.0.0 de a *=* a (réfléxivité de l'égalité). Donc par définition de la relation "*=s*", on déduit que l'on a b +f a *=s* c +f a.

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

Montrons que x se calcule en une égalité: soit a la valeur de la variable "x" de la règle. Comme a et a *=* x sont prouvés par des troncatures strictes de p, par récurrence a et a *=* x vérifient les conclusions du théorème. Donc :

  • a se calcul en une égalité a1 *=* a2 et on a a1 =c a2
  • a *=* x étant déjà une égalité (elle se calcul en elle-même), on a a =c x.
Soit ac et xc les résultats des calculs de a et x. Remarquons que ac = (a1 *=* a2).
Par définition de =c , on a deux cas:
  1. ac = xc
  2. comme ac est une application, xc est une application xc1 +f xc2 où:
    • $F[ equal] +f a1 =c xc1
    • a2 =c xc2

Cas 1:

On a xc = (a1 *=* a2)
On a donc la conclusion voulu: x se calcul en une égalité a1 *=* a2 et on a a1 =c a2

Cas 2:

Comme x se calcul en xc1 +f xc2, le calcul de xc1 est terminé (car xc1 a la position de fonction).
Pour l'égalité $F[ equal] +f a1 =c xc1, on a à nouveau deux cas:
Cas de l'égalité : $F[ equal] +f a1 = xc1 :

Dans ce cas x se calcul en $F[ equal] +f a1 +f xc2, donc x se calcul en une égalité.
Il nous reste à montrer que a1 =c xc2:
On a a1 =c a2 et a2 =c xc2, donc si =c est associatif on a a1 =c xc2
Cas du split:
Les deux membres de l'égalité par calcul ont déjà leur calcul terminé donc xc1 est de la forme xc1a +f xc1b et on a xc1a =c $F[equal] et .
Comme $F[equal] a son calcul terminé et n'est pas une application, par définition de =c, on a xc1a = $F[equal].
Donc xc1 = $F[equal] +f xc1b, donc x se calcul en $F[equal] +f xc1b +f xc2.
Il nous reste à montrer que xc1b =c xc2:
On a a1 =c xc1b, a1 =c a2 et a2 =c xc2 donc si =c est commutatif et associatif on a xc1b =c xc2

encours : faire la conclusion, montrer la commutativité et l'associativité de =c