Ssreflect Users Discussion List

[Ralf Jung <>]

Hi,

>> I was unable to find it in the documentation.
> 
> It depends where you looked. The ability to name an evar is a feature of
> Coq 8.5, not a feature of ssreflect. So your best bet is the
> documentation of Coq. (Disclaimer: I have not checked whether it is
> documented.)

I was not aware this is a Coq feature. Interesting!

> Consider the original example where I want to swap something and 3 (and
> I don't want to use the commutativity lemma for some reason). The
> intuitive way of writing it in ssreflect is to use a wildcard (an "evar"
> in Coq linguo) for "something".
> 
> rewrite (_ : _ + 3 = 3 + _).
> 
> Except that it does not work at all because Coq assumes that the
> rightmost evar is independent from the middle one, so ssreflect
> complains that it has no idea what to use to fill the rightmost evar. By
> using a named evar, you tell Coq (and thus ssreflect) that the rightmost
> evar is the same as the middle one. So, as soon as ssreflect has filled
> the middle evar by matching the left-hand side of the equality with the
> goal, the right-hand side of the equality no longer contains any evar,
> which makes ssreflect happy.

Thanks for the quick and helpful reply :)

So, this is about LHS vs. RHS because ssreflect matches the LHS with
(all subterms of) the goal, and that is guaranteed to leave the third
evar open since nothing is matched against it. If you had written

  rewrite -(_ : 3 + ?[n] = ?n + 3 )

then the sides would have been reversed, but the mechanism and all would
still be the same. Right?

It seems that it's always the first occurrence that has to have the "[",
like that's some kind of binder that completely transcends the AST...
weird. I would have expected that you could just write

  rewrite -(_ : 3 + ?n = ?n + 3 )

like you would in an ltac match expression.

Kind regards,
Ralf