The Coq mailing list

[Nicolas Magaud <magaud AT unistra.fr>]

Dear Coq users,

I have a technical question about rewriting with an alternative equality in 
Coq.

To make it short, I consider a type A (in Set) equipped with any equivalence 
relation (equal). I do not want to use Leibnitz Equality.
I try to prove a goal (see below) which involves rewriting in the type of an 
universally quantified variable :
I expect the goal "forall p:(Q x), (R x p)" to be transformed into "forall 
p:(Q y), (R y p)"  when I try to rewrite with an hypothesis "H:equal x y".

This actually works fine when "equal" is Leibnitz equality. But with my 
equality, I simply lead to an error message which I do not know how to 
interpret.
Instead, I would have expected the system to tell me about some Proper 
instances which were missing to do the job correctly.

Is this just a limitation of the current implementation of Coq (I checked 
with 8.4pl2 and trunk) or simply impossible to obtain with a non-Leibnitz 
equality ?

Thanks in advance for your suggestions.

Nicolas Magaud

-------------------------------------------------------------

Require Import Setoid Morphisms.

Parameter A:Set.

Parameter equal : A -> A -> Prop.

Parameter Q:A-> Prop.
Parameter R:forall a, Q a->Prop.

Instance equiv_equal : Equivalence equal.
Admitted.

Lemma test : forall x y:A, equal x y -> forall p:(Q x), (R x p).
intros x y H.
rewrite H.
(*

Error: build_signature: no constraint can apply on a dependent argument

*)