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é : ![]() ![]() ![]() 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é ![]() ![]() ![]() ![]() ![]() ![]() 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 |