The Coq mailing list

[Benedikt AHRENS <Benedikt.Ahrens AT unice.fr>]

Hi,

you might want to add an instance of Proper as follows:

On 04/27/2011 11:22 AM, Florent Becker wrote:
> Hi list,
>
> I have an equivalence relation that is compatible with an operator, as
> follows:
>
> Require Import Setoid.
>
> Inductive eq': nat -> nat -> Prop :=
> | eq'_refl: forall x, eq' x x.
>
> Notation "s =' t" := (eq' s t) (at level 70, no associativity).

[...]

> But I cannot see how to rewrite on the right side (i'm really interested
> in non-commutative operators, please ignore that + is commutative):


Instance bla : Proper (eq' ==> eq' ==> eq') plus.
Proof.
  unfold Proper; do 2 red.
  intros x x' H y y' H0.
  destruct H.
  destruct H0.
  constructor.
Qed.


> Goal forall a a' b, a =' a' -> a+b =' a' + b.
> intros.
> rewrite H. (* this fails *)

Should work now.

Greetings,
benedikt