Lazi

essai 4

5.1 Toute vérité se calcul 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.

Énoncé

Condition

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

Conclusions

  • x se calcul en une égalité
  • si l'un des membres de l'égalité se calcule en un mot, alors l'autre membre se calcule en ce même mot
  • si l'un des membres de l'égalité se calcule en une application alors :
    • l'autre membre se calcule en une application
    • il existe des preuves de l'égalité entre les fonctions des applications et les arguments des applications

Démonstration

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

Si la longueur de p est 1

Alors l'unique déduction ne peut avoir de condition, et 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 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. Les membres de cette égalité sont des applications. On prouve a *=* a par réflexivité de l'égalité. On prouve b *=* c car cette vérité est prouvé par p, il suffit donc de tronquer p jusqu'à la déduction prouvant cette vérité.

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

On utilise un raisonnement similaire au précédent.

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. Comme a se calcule en une application et que l'on a a *=* x , par l'hypothèse de récurrence on déduit que x se calcule en une application x0 +f x2 avec $F[ equal] +f a1 *=* x0 et a2 *=* x2. On a une preuve (scrictement plus courte que p) de $F[ equal] +f a1 *=* x0, on peut réappliquer la récurrence. On obtient au final que x se calcule en une formule $F[ equal] +f x1 +f x2 et qu'il existe des preuves plus courtes que p de a1 *=* x1 et a2 *=* x2.

Définisson localement la relation "S" : S x y = les conjonctions :

  • si x se calcule en un mot alors y se calcule en un mot
  • si x se calcule en une application alors :
    • y se calcule en une application
    • il existe des preuves de l'égalité entre:
      • les fonctions de x et y
      • les arguments de x et y
  • S n y x

Montrons que S est une relation transitive. Soit a,b et c des formules telles que S a b et S b c. Si a se calcul en un mot alors b et donc c aussi et donc c aussi. Si a se calcul en une application alors b aussi et donc c aussi. Soit a1,a2,b1,b2,c1,c2 tel

D'après l'hypothèse de récurrence, si on a x *=* y par une preuve de longueur m<n, alors on a S m x y .

Montrons que l'on a S n x1 s2: comme on a a1 *=* x1 par une preuve de longueur <n, on a par hypothèse de récurrence S n x1 a1. Comme on a a1 = a2 par une preuve de longueur <n, on a S n a1 a2. Comme on a a2 = x2 par une preuve de longueur <n, on a S n a2 x2. Comme S n est une relation transitive, on a S n x1 x2.