Lazi

essai 2

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 et x la formule objet de p.

Conclusions

  • x se calcul en une égalité
  • soit y *=* z cette égalité, alors:
    • si y se calcule en un mot, z ce calcule en ce même mot
    • si y se calcule en une application y1 +f y2 alors :
      • z se calcul en une application z1 +f z2
      • il existe des preuves de y1 *=* z1 et y2 *=* z2
      • ces preuves sont de longueur strictement inférieures à la longueur de p

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é. y et z sont des applications. y1 *= z1 par réflexivité de l'égalité. y2 *=* z2 car c'est une hypothèse de la déduction.

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 est 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é $F[ equal] +f a1 +f a2, donc x se calcul en une application x1 +f z. On a $F[ equal] +f a1 *=* x1 et a2 *=* z par des preuves plus courtes que p. En réappliquant ce raisonnement on obtient que x se calcul en une formule $F[ equal] +f y +f z avec a1 *=* y et a2 *=* z prouvés par des preuves plus courtes que p.

Montrons le reste des conclusions.
Si a1 se calcule en un mot, comme a est prouvé par une troncature de p, on peut par récurrence déduire que a2 se calcul en un mot.
De même, si a1 se calcule en une application a11 +f a12, on peut déduire que a2 se calcul en une application a21 +f a22 avec des preuves plus courtes de a11 *=* a21 et a21 *=* a22.