Le texte brut

4) Le texte brut

Nous utilisons la même technique que précédemment, c'est-à-dire traduire une opérateur par une phrase explicative. Le seule différence est que nous varions les phrases pour les adapter à chaque cas.

Théorème InvTrans.
Énoncé : E:Set.R:(Rel E).(Trans E R)(Trans E (Inv E R)).
Proof :
Considérons un ensemble E quelconque.
  Considérons un terme R quelconque de type (Rel E)
    Posons par hypothèse (Trans R E) (H).
      Considérons un élément x quelconque de E.
        Considérons un élément y quelconque de E.
          Considérons un élément z quelconque de E.
            Posons par hypothèse (Inv E R x y) (H₁).
              Posons par hypothèse (Inv E R y z) (H₂).
                            * Par l'hypothèse H nous avons (Trans E R).
                            * L'élément z appartient à E.
                          * Par application nous avons y₀:E.z₀:E.(R z y₀)(R y₀ z₀)(R z z₀).
                          * L'élément y appartient à E.
                      * Par application nous avons z₀:E.(R z y)(R y z₀)(R z z₀).
                      * L'élément x appartient à E.
                    * Par application nous avons (R z y)(R y x)(R z x).
                    * Par l'hypothèse H₂ nous avons (Inv E R y z).
                  * Par application nous avons (R y x)(R z x).
                  * Par l'hypothèse H₁ nous avons (Inv E R x y).
                Par application nous avons (R z x).
              Nous avons montré (Inv E R y z)(R z x).
            Nous avons montré (Inv E R x y)(Inv E R y z)(R z x).
          Nous avons montré z:E.(Inv E R x y)(Inv E R y z)(R z x).
        Nous avons montré y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).
      Nous avons montré x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).
    Nous avons montré (Trans E R)x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).
  Nous avons montré R:(Rel E).(Trans E R)x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).
Nous avons montré E:Set.R:(Rel E).(Trans E R)x:E.y:E.z:E.(Inv E R x y)(Inv E R y z)(R z x).
Qed.

C'est à peine mieux. On a maintenant la possibilité de se rendre compte que E est ensemble, R une relation et que H représente l'hypothèse qui affirme que R est transitive etc... Cependant, on est en quelque sorte noyé sous la masse. Ce texte utilise plus de cinq phrases là où il n'en faudrait qu'une. Cette verbosité rend impossible toute vision d'ensemble de la preuve.

Nous allons par la suite explorer quelques méthodes pour compacter les textes.

Retour Sommaire Suite

Yann Coscoy