The Coq mailing list

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

Le dimanche 13 mai 2012 à 17:12 +0200, Matthieu Sozeau a écrit :
> Le 13 mai 2012 à 13:43, Guillaume Melquiond a écrit :
> 
> > Hi,
> > 
> > I am trying to get a feel of what can or cannot be done with
> > setoid_rewrite. In particular, is there a way of declaring instances
> > such that rewriting with a relation (R a b) causes a goal to change from
> > (P (f a)) to (Q (f b))? Here is a toy example so that my question makes
> > more sense. Assume that the goal is
> > 
> >  H: (c < d)
> >  ------------
> >  |- (a + c < b)
> > 
> > I would like to rewrite with H so that c is replaced by d, but I don't
> > want the goal to become (a + d < b), which is too strong and possibly
> > unprovable, but (a + d <= b).
> 
> Hi Guillaume,
> 
>   this is not possible at the moment, but if you have an algorithm
> in mind I'd be curious to hear about it.

I wasn't expecting a different algorithm, since the current one succeeds
in doing the "rewrite <- H1" and "now" of my example, which seem to me
like they are the difficult parts. But perhaps I am just being naive
about the implementation.

Basically, on my example, you cross < then + to reach the subterm, so
you have to apply the corresponding morphism, which tells you how to
build (a + c < a + d). The left-hand side of that relation matches the
goal, by construction. So you are left with matching the right-hand
side. So you look for a morphism of signature ((_ ==> impl) lt); there
is one, you are done.

Best regards,

Guillaume