The Coq mailing list

[Guillaume Melquiond <(e29315a54f%hidden_head%e29315a54f)guillaume.melquiond(e29315a54f%hidden_at%e29315a54f)inria.fr(e29315a54f%hidden_end%e29315a54f)>]

Le lundi 14 mai 2012 à 11:25 +0200, Matthieu Sozeau a écrit :

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

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

Thanks a lot. This helps, but it only seems to work only on the
rightmost subterm of an expression. Rather than (R (m x) (m y)), one
would need (R (p x) (q y)) so that it works for any subterm. I guess it
involves point-wise relations, but I can't get it to work. Any
suggestion?

Best regards,

Guillaume