The Coq mailing list

[jean-francois.monin AT imag.fr]

Dans votre cas il suffirait d'avoir un peu de eta-convertibilité 
(non présente dans Coq actuellement) :
(1)  R = fun x y => R x y
puisque trivialement, trans (trans R) = fun x y => R x y

Il arrive que (1) soit naturellement vérifié dans le contexte de travail.
Si ce n'est pas le cas, pouvez-vous vous contenter de travailler
systématiquement sur des formes eta-expansées, i.e.

Definition eta2 R := fun x y => R x y.

et remplacer sytèmatiquement forall... R..., blabla... R... blabla
par forall... R..., blabla... (eta2 R)... blabla

Par exemple : 
Goal forall R, trans (trans (eta2 R)) = (eta2 R).
Proof. reflexivity. Qed.

Theorem T1 : forall R, P (eta2 R) -> P (trans (eta2 R)).
Theorem T2 : forall R, P (trans (eta2 R)) -> P (eta2 R).
Proof. 
  intros R hR. exact (T1 (trans R) hR).
Qed.

  Jean-François

-- 
Jean-François Monin           http://www-verimag.imag.fr/~monin/
VERIMAG - Centre Equation     tel (+33 | 0) 4 56 52 03 72
2 avenue de Vignate           fax (+33 | 0) 4 56 52 03 44 
F-38610 GIERES

Damien Pous a ecrit :
 > Bonjour,
 > 
 > Je travaille sur les bisimulations, et suis donc amené à utiliser
 > intensivement des relation binaires:
 > 
 > Ma solution actuelle: 
 > REL(X Y: Set) := X -> Y -> Prop.
 > ne me conviens pas car il me manque une "égalité pratique":
 > 
 > si je définis la transposée:
 > trans R x y := R y x.
 > 
 > je peux prouver "forall R x y, trans (trans R) x y <- R x y"
 > mais pas "forall R, trans (trans R) = R"
 > 
 > or c'est ce dernier résultat qui est pratique:
 > si j'ai prouvé "forall R, P R -> P (trans R)" (où P est un prédicat sur
 > les relations),
 > pour prouver "forall R, P (trans R) -> P R"
 > il me faut recopier, et adapter la première preuve, alors qu'avec (ii),
 > un simple rewrite me permettrait d'appliquer le résultat précédent...
 > 
 > (bien sûr ce schéma se retrouve pour des choses beaucoup plus complexes
 > que la transposée...)
 > 
 > Faut-il poser en axiome la proof-irrelevence et/ou une forme affaiblie
 > d'extensionalité ?
 > (ce qui ne me plaît pas car si je n'étais pas fainéant, je recopierais
 > mes preuves, et ça passerai sas axiome...)
 > 
 > Existe-t-il une meilleure façon de définir les relation binaires ?
 > 
 > Au passage, quelqu'un a-t-il déjà généralisé la partie Relations de la
 > librairie standard au cas "X -> Y -> Prop", X<>Y ?
 > 
 > Merci d'avance,
 > Damien
 > 
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club