| Retour | Sommaire | Suite |
Voyons maintenant ce que donne l'utilisation simultanée des trois techniques de compactions présentées.
|
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). En appliquant l'hypothèse H à z, y, x, H2 et H1 nous avons (R z x). Nous avons montré E:Set.R:(Rel E).(Trans E R)x,y,z:E.(Inv E R x y)(Inv E R y z)(R z x).Qed. |
On arrive à croire que c'est une preuve. Cependant
celle-ci semble incomplète. C'est bien le cas une particularité
de la représentation des preuves dans le Calcul des Constructions
est que toute une partie du raisonnement est implicite (
-conversion des types). Voyons par
la suite le texte obtenu en si l'on fait
ressortir cette partie du raisonnement.
| Retour | Sommaire | Suite |