The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

The setoid_rewrite tactic fails as well. It's not enough for equal to be an equivalence relation. Q and R have to be compatible with equal. I'm not sure how to set up the rewrite tactic to use equal_R.

Axiom A : Set.

Axiom equal : A -> A -> Prop.

Axiom Q : A -> Prop.

Axiom R : forall a, Q a -> Prop.

Axiom equal_refl : forall x, equal x x.

Axiom equal_symm : forall x y, equal x y -> equal y x.

Axiom equal_trans : forall x y z, equal x y -> equal y z -> equal x z.

Axiom equal_Q : forall x y, equal x y -> Q x -> Q y.

Axiom equal_R : forall x y p q, equal x y -> R x p -> R y q.

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

intros.

assert (q : Q y).

info_eauto 2 using equal_refl, equal_symm, equal_trans, equal_Q, equal_R.

cut (R y q).

info_eauto 3 using equal_refl, equal_symm, equal_trans, equal_Q, equal_R.

On Fri, Jan 10, 2014 at 12:57 PM, Lucian M. Patcas <lucian.patcas AT gmail.com> wrote:

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

*)