The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

Hi,
the error message indeed seems unintelligible at first sight, but it
holds precious information nonetheless :)
It shows what instances of morphisms the typeclasses mechanism is
failing to generate and can help you understand where things go wrong.
Let us see your case in detail : you want to rewrite the pointwise
equality [f ° g ° h == (f ° g) ° h] in [(f ° g ° h) x == ((f ° g) ° h)
x].

First, please note that you don't actually need rewriting of any kind
in order to prove that lemma, it is true by reflexivity : the two
sides of the equivalence both convert to [hfun f (hfun g (hfun h
x)))], therefore they are (Leibniz-)equal by definition and the
equivalence is true by reflexivity. Similarly, the compose_assoc lemma
could've been proved with a simple call to reflexivity.

In general though, you may need such a rewrite step and the following,
easier, example suffices to reveal what the issue is and how to
correct it.

Goal forall (A B : preord) (f g : hom A B) (x : A), f == g -> f x == g x.
Proof.
  intros A B f g x H.
  rewrite H. (* Failure here *)

The error output of the rewrite tactic looks like this :
...
?71 == (Morphism (?65 ==> ?69 ==> flip impl) equiv)
?70 == (MorphismProxy ?69 (g x))
?69 == (relation B)
?68 == (MorphismProxy ?66 x)
?67 == (Morphism (equiv ==> ?66 ==> ?65) (hfun A B))
?66 == (relation A)
?65 == (relation B).

First, it helps to know that MorphismProxy is just reflexivity,
therefore, for instance, you can read constraint ?70 as [?69 (g x) (g
x)] where ?69 is a relation.
The tactic tries to rewrite on both side of the equivalence, using
relation ?65 on the left-hand side and ?69 on the right-hand side :
the constraint ?71 ensures that [==] is a morphism for these
relations. Of course, there's nothing to do on the right-hand side and
?69 will end up being the Leibniz equality, for which constraint ?70
will hold trivially : [g x = g x].
The last 4 lines, however, concern the left-hand side, ie. rewriting
[f x] in [g x] using [f == g]. Contraints ?68 and ?67 mean that the
tactic is looking for two relations ?66 and ?65 such that [?66 x x]
holds, and such that :
forall f g, f == g -> forall x y, ?66 x y -> ?65 (f x) (g y).
This is the one that shall allow the tactic to use [f == g] to replace
[f x] by [g x] ; therefore you expect ?65 and ?66 to simply be [==] on
the preorder A, for which the reflexivity constraint ?68 holds by
reflexivity. Hence, the issue must come from constraint ?67 which is
the only one left.

Now, it seems that this constraint is simply an instance of a morphism
you proved in your development : [hfun_equiv_morphism]. When this
happens, this is usually sign that notations or implicit arguments are
actually hiding differences between two apparently equal expressions.
By using Set Printing Implicit, you can actually see why the
typeclasses mechanism cant use [hfun_equiv_morphism] to resolve ?67 :

hfun_equiv_morphism : forall A B : preord,
 @Morphism (hom A B -> A -> B)
  (@equiv (hom A B) ==> @equiv A ==> @equiv B) (hfun A B)

?67 == (@Morphism (mono_func A B -> A -> B) (@equiv (hom A B) ==> ?134
==> ?133) (hfun A B))

The two expressions do not unify because [hfun_equiv_morphism] defines
morphisms for functions of type [hom A B -> A -> B], while the type
inferred for the morphism parameter in ?67 is [mono_func A B -> A ->
B]. You have a coercion in your dev that allows you to use a [hom A B]
as a [mono_func A B], but the typeclasses mechanism cannot unify one
with the other. To solve the issue, you should define the morphism for
objects of type [mono_func A B -> A -> B] as well, for instance using
the following Instance declaration :

Instance hfun_equiv_morphism' (A B : preord) :
  @Morphism (mono_func A B -> A -> B)
  ((@equiv (hom A B)) ==> (@equiv A) ==> (@equiv B)) (hfun A B).
exact hfun_equiv_morphism.
Qed.

Once this morphism is in the typeclass database, the rewriting steps
will succeed.

So here you are, sorry for the quite longish response, but I hope that
a detailed explanation can help you figure out issues with the setoid
rewrite in the future.

Stéphane L.

On Fri, Jun 26, 2009 at 10:55 PM, 
Robert<robdockins AT fastmail.fm>
 wrote:
> (* Friends,
>
>   I'm trying to develop a theory of preorders
>   and monotone functions.  I'd like to be able to do
>   rewriting up to equivalance, but I'm having some problems
>   getting it to work.  In some cases rewriting works as
>   expected, but in others I get error messages about not
>   being able to solve constraints.  I don't understand what
>   is causing the error or how to fix it.  Can anyone
>   enlighten me?
>
>   Most of this file is just setup for the problem, which
>   appears near the end.
>
>   I'm using Coq 8.2 (CoqIde, Windows build).
> *)
>
> Require Import Setoid.
>
> Record preord :=
>  { po :> Type
>  ; ord : po -> po -> Prop
>  ; ord_refl : forall x, ord x x
>  ; ord_trans : forall x y z, ord x y -> ord y z -> ord x z
>  }.
>
> Hint Resolve ord_refl ord_trans.
>
> Definition equiv {A:preord} (x y:A) := ord A x y /\ ord A y x.
> Infix "==" := equiv (at level 75, no associativity).
>
> Lemma equiv_refl : forall (A:preord) (x:A), x == x.
> Proof.
>  intros; split; auto.
> Qed.
>
> Lemma equiv_sym : forall (A:preord) (x y:A), x == y -> y == x.
> Proof.
>  unfold equiv; intuition.
> Qed.
>
> Lemma equiv_trans : forall (A:preord) (x y z:A), x == y -> y == z -> x
> == z.
> Proof.
>  unfold equiv; intuition eauto.
> Qed.
>
> Hint Resolve equiv_refl equiv_trans.
>
> Add Parametric Relation (p:preord) : (po p) (ord p)
>  reflexivity proved by (ord_refl p)
>  transitivity proved by (ord_trans p)
>  as po_ord_relation.
>
> Add Parametric Relation (p:preord) : (po p) (@equiv p)
>  reflexivity proved by (equiv_refl p)
>  symmetry proved by (equiv_sym p)
>  transitivity proved by (equiv_trans p)
>  as po_equiv_relation.
>
> Instance equiv_ord_subrelation (p:preord)
>  : subrelation (@equiv p) (@ord p).
> do 3 (intros; hnf).
> unfold equiv; intuition.
> Qed.
>
> Record mono_func (A B:preord) :=
>  { hfun :>  A -> B
>  ; hfun_mono : forall x x',
>       ord A x x' -> ord B (hfun x) (hfun x')
>  }.
>
> Definition pointwise_ord {A B:preord} (f g:mono_func A B) :=
>  forall x, ord B (f x) (g x).
>
> Definition hom (A B:preord) :=
>  Build_preord (mono_func A B) (pointwise_ord)
>      (* refl *)  (fun f x => ord_refl B (f x))
>      (* trans *) (fun f g h H1 H2 x => ord_trans B (f x) (g x) (h x)
>      (H1 x) (H2 x)).
>
> Definition compose {A B C:preord} (f:hom B C) (g:hom A B) : hom A C :=
>  Build_mono_func A C (fun x => f (g x))
>     (fun x x' H => hfun_mono B C f (g x) (g x') (hfun_mono A B g x x'
>     H)).
> Infix "oo" := compose (at level 55, right associativity).
>
> Lemma compose_assoc : forall A B C D (f:hom C D) (g:hom B C) (h:hom A
> B),
>  f oo (g oo h) == (f oo g) oo h.
> Proof.
>  intros; split; simpl; hnf; intros; simpl; auto.
> Qed.
>
> Add Parametric Morphism (A B:preord) : (@hfun A B)
>  with signature (ord (hom A B)) ==> (ord A) ==> (ord B)
>  as hfun_ord_morphism.
> simpl; intros.
> apply ord_trans with (hfun A B y x0).
> apply H.
> apply hfun_mono; auto.
> Qed.
>
> Add Parametric Morphism (A B:preord) : (@hfun A B)
>  with signature (@equiv (hom A B)) ==> (@equiv A) ==> (@equiv B)
>  as hfun_equiv_morphism.
> simpl; intros.
> apply equiv_trans with (hfun A B y x0).
> split.
> apply H.
> destruct H.
> apply H1.
> split; apply hfun_mono; destruct H0; auto.
> Qed.
>
> (* Here is an example demonstrating the sort of problems
>   I'm having.
> *)
> Goal forall (A B C D:preord) (f:hom C D) (g:hom B C) (h:hom A B) (x:A),
>  ((f oo g oo h) x) == (((f oo g) oo h) x).
> Proof.
>  intros.
> rewrite compose_assoc.
> (*
> This rewrite doesn't work, and gives me an unintelligible
> error about unsatisfied constraints.  I don't know how
> to make it happy.
>
> The following, however, does work.  I'd really like
> to get the rewriting to work so I don't have to manually
> apply morphism proofs.
> *)
>  apply hfun_equiv_morphism.
>  apply compose_assoc.
>  apply equiv_refl.
> Qed.
>
> --
>  Robert
> �robdockins AT fastmail.fm
>
> --------------------------------------------------------
> Bug reports: http://logical.saclay.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>



-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06