The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Le 20 déc. 2010 à 19:33, Andrew Kennedy a écrit :

> Hi all

Hi Andrew,

> 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! 

It's precisely that: the fact that [z] is a proper element for [pequiv] in 
your example
should be added as another morphism instance declaration. One way is to 
[change (z =~= z) to (Proper pequiv z)] in this case, or to directly extend 
the resolution tactic to try applying
reflexivity hypotheses:

Hint Extern 4 (Proper ?R ?z) => 
  match goal with H : R z z |- _ => eapply H end : typeclass_instances.

Beware that [PER] refers to something in [Relation_Definitions] after you 
import [Setoid] and [Morphisms].

Cheers,
-- Matthieu