Ssreflect Users Discussion List

[Guillaume Melquiond <>]

Le 03/09/2013 14:01, Georges Gonthier a écrit :
>     Hi,
> The bracketing isn't quite right: this should read
>      rewrite some_rule; first 1 [idtac] || by cheap_tactic.
> Note that you can write this using plain Coq tacticals, as
>      rewrite some_rule; [| by cheap_tactic..]
> The two lines above are equivalent, but not quite equivalent to rewrite .. 
> by, which you can still get while using ssreflect by writing
>      rewrite -> some_rule by cheap_tactic.
> I believe the above can use the success of cheap_tactic to decide which 
> occurrence to rewrite, while the top two only control whether the rewrite 
> proceeds at all.

Is that so? If Coq was using cheap_tactic, I would expect the following 
script to succeed:

Goal (forall x y, x = 0 -> y + x = y) -> 3 + 1 = 3 + 0.
intros H.
rewrite H by reflexivity. (* fails because rewrite matched 3 + 1 *)

As far as I understand, there is no difference between "rewrite by" and 
"rewrite ;".

Best regards,

Guillaume