The Coq mailing list

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

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

Best regards,

Guillaume


Require Import Morphisms Setoid.

Axiom N : Set.
Axiom plus : N -> N -> N.
Axiom le : N -> N -> Prop.
Axiom lt : N -> N -> Prop.

Instance _le_refl : Reflexive le. Admitted.
Instance _le_plus_lt : Proper (le ==> lt ==> lt) plus. Admitted.
Instance _le_lt : Proper (le --> le ==> Basics.impl) lt. Admitted.

Goal forall a b c d, lt c d -> lt (plus a c) b.
intros a b c d H.
Fail rewrite -> H. (* this fails, but the following lines work *)
cut (le (plus a d) b).
intros H1.
rewrite <- H1.
now apply _le_plus_lt.