The Coq mailing list

[Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr>]

Hello,

If I understand your question correctly it should be possible. Maybe you 
should post some code to make it clearer what are the precise 
circumstances of your troubles.

Arthur Azevedo de Amorim a écrit :
> Hello,
>
> I am having a problem using the new rewriting system in Coq 8.2. 
> First, I declared a basic setoid record
> with a carrier, a relation and a proof that this relation is an 
> equivalence relation. Then I declared a new type
> for maps between setoids (A =>> B), that have a function and a proof 
> that it preserves equality. I added the equality
> and these maps as relations and morphisms, and then added a canonical 
> structure for seeing a setoid morphism
> with a setoid structure. So far so good. The problem appears when I 
> try to curry this scheme: if I have F : A =>> B =>> C,
> I can't proof that a1 == a2 -> F a1 b == F a2 b unless I destruct F 
> explicitly and apply the preservation lemma
> it carries. Is there a way of doing this with a regular rewrite?
>
> --
> Arthur Azevedo de Amorim