The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Hi all

I'm formalizing some basic algebra over carriers that are represented by a 
partial equivalence relation on a type, giving me a "subdomain" and an 
equivalence not fixed to Leibniz equality. But I'm having trouble getting 
setoid_rewrite to work: I can apply the "morphism" property directly, but 
setoid_rewrite fails. Here's a cut-down example:

Require Import RelationClasses.
Require Import Equivalence.
Open Scope equiv_scope.

Class SemiGroup {A:Type} {R} (sg_PER: PER R)  `(op: A -> A -> A) :=
{ ass : forall x y z, x =~= x -> y =~= y -> z =~= z -> op x (op y z) =~= op 
(op x y) z;
  mor : forall x x' y y', x =~= x' -> y =~= y' -> op x y =~= op x' y'
}.

Require Import Setoid. Require Import Morphisms. 

Add Parametric Morphism {A} `(SemiGroup A) : (op) with signature R ==> R ==> 
R as g_op_morphism. 
Proof. intros x x' xx' y y' yy'. apply mor; assumption. Qed.

Lemma boring: forall A `(SG: SemiGroup A), forall x y z, z =~= z -> x =~= y 
-> op x z =~= op y z. 
Proof. intros. setoid_rewrite H.


At this point, I get a "tactic failure: setoid rewrite failed: unable to 
satisfy the rewriting constraints".  This despite the following explicit use 
of g_op_morphism working:

Proof. intros. apply (g_op_morphism _ _ _ _ _ _ _ H0 _ _ H). Qed.


Possibly I haven't set up the morphisms correctly. 
Any help very much appreciated! 
Cheers
Andrew.