The Coq mailing list

[Andrew Kennedy <akenn AT microsoft.com>]

Thanks Matthieu - that works great.
- Andrew.

-----Original Message-----
From: Matthieu Sozeau 
[mailto:matthieu.sozeau AT gmail.com]
 
Sent: 20 December 2010 19:11
To: Coq Club
Subject: Re: [Coq-Club] Problem with setoid_rewrite and PER


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