coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Florent Becker <florent.becker AT ens-lyon.org>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] setoid rewrite and binary operators
- Date: Wed, 27 Apr 2011 11:22:39 +0200
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
- [Coq-Club] setoid rewrite and binary operators, Florent Becker
- Re: [Coq-Club] setoid rewrite and binary operators, Benedikt AHRENS
Archive powered by MhonArc 2.6.16.