The Coq mailing list

[Florent Becker <florent.becker AT ens-lyon.org>]

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).


Lemma eq'_trans: forall a b c,
  a =' b -> b =' c -> a =' c.
intros a b c Hab.
induction Hab; tauto.
Qed.

Lemma eq'_sym: forall a b,
  a =' b -> b =' a.
intros a b Hab.
induction Hab; constructor.
Qed.

Add Relation nat eq'
  reflexivity proved by eq'_refl
  symmetry proved by eq'_sym
    transitivity proved by eq'_trans
      as eq'_m.

Add Parametric Morphism b: (fun a => a + b)
  with signature (eq' ==> eq')
    as plus_l_m.
intros x y Hxy; case Hxy; constructor.
Qed.

Add Parametric Morphism a: (plus a)
  with signature (eq' ==> eq')
    as plus_m.
intros x y Hxy; case Hxy; constructor.
Qed.

When I try to rewrite equivalences on the left side of my operator, 
everything works fine:

Goal forall a a' b, a =' a' -> b+a =' b + a'.
intros.
rewrite H.
constructor.
Qed.

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

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

yields:

Toplevel input, characters 21-30:
Error: Tactic failure:setoid rewrite failed: unable to satisfy the 
rewriting constraints.
Unable to satisfy the following constraints:
EVARS:
 ?1526==[a a' b H |- Morphisms.ProperProxy ?1524 (a' + b)]
 ?1525==[a a' b H (do_subrelation:=Morphisms.do_subrelation)
          |- Morphisms.Proper (?1519 ==> ?1524 ==> Basics.flip Basics.impl)
               eq']
 ?1524==[a a' b H |- relation nat]
 ?1522==[a a' b H |- Morphisms.ProperProxy ?1520 b]
 ?1521==[a a' b H (do_subrelation:=Morphisms.do_subrelation)
          |- Morphisms.Proper (eq' ==> ?1520 ==> ?1519) plus]
 ?1520==[a a' b H |- relation nat]
 ?1519==[a a' b H |- relation nat]

I've tried playing with pattern, or making "(fun x => x + b) a" appear 
explicitely, but to no avail. Is there a way to have rewrite work in 
that situation?

Thanks,

Florent