The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 4 févr. 09 à 11:50, Thomas Braibant a écrit :

> Hi,

Hi Thomas,

> The behavior of setoid_rewrite under binders is a little bit
> confusing. Could someone explain what is wrong in the following
> examples ?

There are a number of combined factors that make it hard to understand.
First, the first rewrite works not because of the [Morphism]  
declaration for
mor1_morph but because mor1 unfolds to [forall] and hence unifies with  
a previously
declared [Morphism] for the [all] constant. You can test by simply  
removing the
instance declaration (still works) or making the constant opaque using
[Typeclasses Opaque mor1] (doesn't work anymore).

Second, (@eq A ==> R) is not seen as a subrelation of  
[pointwise_relation A R]
by default (my bad) hence your Morphism declarations are mostly  
useless. You
can just add the following Instance to make it work again:

Instance pointwise_eq A B (R : relation B) :
  subrelation (pointwise_relation A R) (@eq _ ==> R)%signature.
Proof. reduce. subst. apply H. Qed.

Rewriting the instances to use [pointwise_relation] instead will work  
too.
Your example also triggers an inefficiency in the search that can only  
be
solved in the library... This is a somewhat experimental feature as  
you may
have guessed, thanks for the report!

-- Matthieu