9) Le texte compacté complet

  Nous utilisons une technique de double calcul des assertions (cf inférence de type par héritage est par synthèse) qui permet de retrouver la totalité du raisonnement mathématique représenté par la preuve.

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 ; un terme R quelconque de type (Rel E) ; posons par hypothèse (Trans R E) (H).   Considérons trois éléments x, y, et z quelconques de E ; posons par hypothèse (Inv E R x y) (H1) et (Inv E R y z) (H2).     * Par l'hypothèse H nous avons (Trans R E) ce qui est équivalent à x0,y0,z0:E.(R x0 y0)(R y0 z0)(R x0 z0).     * L'élément z appartient à E.     * L'élément y appartient à E.     * L'élément x appartient à E.     * Par l'hypothèse H2 nous avons (Inv E R y z) ce qui est équivalent à (R z y).     * Par l'hypothèse H1 nous avons (Inv E R x y) ce qui est équivalent à (R y x).     Par application nous avons (R z x).   Nous avons montré x,y,z:E.(R y x)(R z y)(R z x), ce qui est équivalent à (Trans E (Inv E R)). Nous avons montré E:Set.R:(Rel E).(Trans E R)(Trans E (Inv E R)). Qed.

  Ce texte est trop verbeux et présente des détails inutiles qui détourne l'attention du lecteur. Nous utilisons quelques techniques pour le rendre plus lisible. (Suite)

Retour

Sommaire

Suite

Yann Coscoy