The Coq mailing list

[Matthieu Sozeau <(e29315a54f%hidden_head%e29315a54f)mattam(e29315a54f%hidden_at%e29315a54f)mattam.org(e29315a54f%hidden_end%e29315a54f)>]

Le 14 mai 2012 à 10:32, Matthieu Sozeau a écrit :

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

What you can do though is use the Proper instances to prove lemmas of the form
[lt x y]. This is not rewriting though.

Class TransitiveLarge {A} (R S : relation A) := {
  transitivity_large_r : forall x y z, R x y -> S y z -> R x z ;
  transitivity_large_l : forall x y z, S x y -> R y z -> R x z }.

Instance tr_large : TransitiveLarge lt le.
Proof. Admitted.

Lemma proper_proof {A B} {R S} m (P : @Proper (A -> B) (S ==> R) m) x y (H : 
S x y) : 
  R (m x) (m y).
Proof. apply P. apply H. Qed.

Ltac proper_proof :=
  repeat eapply proper_proof; try typeclasses eauto; auto.

Goal forall a b c d, lt c d -> lt (plus a c) b.
intros a b c d H.
apply transitivity_large_r with (plus a d); proper_proof.

Gives you:
 ============================
   le (plus a d) b

Hope this helps,
-- Matthieu