The Coq mailing list

[Benjamin Werner <werner AT lix.polytechnique.fr>]

Bonjour,

> 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"

Oui. P Et la double transposee sont eta-convertibles  et la eta-conversion 
n'est pas prise en compte par Coq.
> 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...

Ca serait plus simple avec l'egalite en effet. Cela dit, vous pouvez aussi 
prouver que votre P donne le meme resultat pour deux predicats 
extentionellement egaux (cad ici   si (R x y)<->(R' x y)  alors
(P R)<->(P R').

En fait, Prop est un setoide pour l'equivalence (qui est une relation 
d'equivalence). Les tactiques existantes vous donnent un peu de support.


> (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...)

L'axiome disant que deux predicats equivalents sont egaux est en effet un 
peu violent. Il est toutefois valide dans les versions de Coq recentes ou 
Set n'est pas impredicatif (il etait incoherent sinon).

> Existe-t-il une meilleure façon de définir les relation binaires ?

Si vos relations ont le bon gout d'etre decidables, vous serez beaucoup 
plus heureux avec des fonctions booleenes. Sinon je ne pense pas.

Bon courage,


Benjamin