The Coq mailing list

[Arnaud Spiwack <arnaud AT spiwack.net>]

Yes,

Guillaume's idea is quite clever. We could have a new pseudo-transitivity class of the form R a b -> S b c -> R a c  (borrowing Haskell vocabulary, with a functional dependency of S on R). And then try to use this class rather than Transitivity. I don't know how to do that properly. But it sounds quite possible in theory.


Arnaud

On 13 May 2012 18:04, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

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