The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 10/12/2014 23:49, Vadim Zaliva wrote:
> > On Dec 10, 2014, at 14:03 , Guillaume Melquiond 
> > <guillaume.melquiond AT inria.fr>
> >  wrote:
> >
> > You presumably simplified your example too much, because this is a case of 
> > eta-conversion. So the "change" tactic will happily do the replacement. You 
> > do not need any setoid rewriting there.
>
> I just want to show the rewriting which I want to use in the different 
> context.
> Suppose I do want to do rewrite as shown, how can I do this?

Unfortunately, you have never explained what kind of equivalence you 
need on your functions. Your example showed an equivalence based on 
eta-convertibility, so I gave you a way to do it.

Now you are telling me you are not interested in an equivalence based on 
eta-convertibility, but without explaining what kind of equivalence you 
need instead. So perhaps you want a pointwise equivalence?

Instance foobar :
  forall A B HB,
  Proper (pointwise_relation A (@equiv B HB) ==> eq) (testF A B).

Best regards,

Guillaume