The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 13 mai 2012 à 18:04, Guillaume Melquiond a écrit :

> 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.

Hi,

  The implementation is slightly different: it will indeed cross < and +
and generate constraints [Proper (? ==> lt ==> ?Rplus) plus] and 
[Proper (?Rplus ==> ? ==> flip impl) lt]. The first one gives Rplus:=lt and
hence we must find a [Proper (lt ==> ? ==> flip impl) lt] (which is inferrable
if you declare [Transitive lt]). Note that we don't look for a 
[Proper (__ ==> flip impl) (lt (a + d))], and we expect to get from the
proof of the second proper a theorem of the form [lt (a + d) b -> lt (a + c) 
b]
to apply to the goal. [le] does not appear anywhere here.

Best,
-- Matthieu