The Coq mailing list

[Evgeny Makarov <emakarov AT gmail.com>]

> Pardon me if I am asking something obvious, but is it possible to use
> 'rewrite' with an equivalence relation with type A->A->Set instead of
> A->A->Prop?

rewrite seems to work with identity, which is a Type analog of Leibniz 
equality defined in Coq.Init.Datatypes. Concerning other relations, it 
seems that currently one cannot declare a relation E : A -> A -> Set as 
a setoid relation; therefore, it cannot be used with rewrite. Of course, 
if it is possible to prove the theorem

forall (P : A -> Prop), P x -> forall y: A, E x y -> P y

then one can write an imitation of rewrite in Ltac, though it may not 
determine the subterms that are to be replaced by unification, as 
rewrite does.

At this moment I am not sure if it makes sense to have reflexive, 
symmetric and transitive relations in Set: after all, E x y may consist 
of many elements and E x y -> E y x only guarantees the existence of a 
function from E x y to E y x, not that the sets E x y and E y x are 
equal. Do you have an interesting example where rewriting a relation in 
Set makes sense?

Evgeny