The Coq mailing list

["Lucian M. Patcas" <lucian.patcas AT gmail.com>]

Have you tried the setoid_rewrite tactic?

http://coq.inria.fr/distrib/V8.4/refman/Reference-Manual029.html

On 10 January 2014 06:21, Nicolas Magaud <magaud AT unistra.fr> wrote:

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

*)