The Coq mailing list

[Damien Pous <Damien.Pous AT ens-lyon.fr>]

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