Ssreflect Users Discussion List

[t x <>]

Georges: Thanks for the clarification. Pierre's solution of "first 1 [idtac] || by cheap_tactic" makes sense now. Thanks for explaining this.

Guillaume: in the above example, it fails because it binds

x = 1, y = 3. Thus, it ends up with the goals of:

Goal 1:

  3 = 3 + 0

Goal 2: (related to "x=0")
  1 = 0

Then, it fails with "impossible to unify 0 with 1."

This seems consistent with my belief -- "rewrite H by reflexivity" fails because it couldn't solve one of the required premises.

On Tue, Sep 3, 2013 at 4:49 PM, Guillaume Melquiond <> wrote:

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