The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

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. Basically in the current
situation the relations that appear in the goal cannot change (except
if you're actually rewriting with a relation between relations,
like relation equivalence). There is however support for declaring that a 
relation is included in another one through the [subrelation] typeclass,
but that is used only to infer "relaxed" Proper instances from existing
strict ones, for example inferring [Proper (foo ==> le) f] from 
[Proper (foo ==> lt) f].

Best,
-- Matthieu