The Coq mailing list

[Danko Iliḱ <danko AT lix.polytechnique.fr>]

Evgeny Makarov wrote:
> 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.

Thanks for the tip. I'm sure there is some workaround for what I want to
do. Maybe the best is to modify the setoid code of Coq so that it works
with any type, not just Prop...?

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

I am writing in Coq an interpreter for a programing language that is an
equational theory and I want to extract my theorems as ML code, so my
equality can't be in Prop. I also want to use as much automation as
possible, in particular the ring tactic, for which I need to have a setoid.

Is there any theoretical reason why setoids are limited to
Prop-relations in Coq? I have used them in context of Martin-Löf type
theory which has no Prop.

Thanks,
Danko