Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hi Robbert,

Robbert Krebbers 
<>
 writes:

> I often make use of "rewrite foo in hyp", which does not work well in
> ssreflect: it changes the order of the hypotheses, and it does not
> work with setoids. See the attached example.

I'm not expert in the inner workings of the rewrite tactic and likely
others will answer more accurately; here are a couple of comments
however:

8<--------------------------------------------------8<
  H1 : P x
  H2 : x = y
  ============================
   True
8<--------------------------------------------------8<

> rewrite H2 in H1.
> (* flips the order of H1 and H2 *)

This is expected, if I recall correctly from the manual, rewrite A in B
this is roughly equivalent to:

move: B; rewrite A; move=> B.

However it has some particularities, as your next example shows:

> rewrite H1 in H2.
> (* Error: tampering with discharged assumptions of "in" tactical *)

This may be avoided using:

> rewrite H1 in H2 *.

The manual does a better job than I could ever do in explaining "in *".

Best regards,
Emilio