Ssreflect Users Discussion List

[Guillaume Melquiond <>]

On 22/02/2016 17:56, Ralf Jung wrote:
> Hi,
> 
>> Have you ever wanted to rewrite using wildcards not only on the
>> left-hand side but also on the right-hand side of an equality? Are you
>> using Coq 8.5? Then the following trick might be of help to you:
>>
>> Lemma foo x y : x + 3 + y = 3 + x + y.
>> rewrite (_ : ?[n] + 3 = 3 + ?n).
> 
> Consider me confused. Is this "?[n]" business a feature available for
> all pattern matching, e.g. also for "rewrite [?[n] + n]lemma" to find an
> application of plus with twice the same argument?

Hopefully yes.

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

> Also, what does this have to do with left-hand side vs. right-hand side?

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.

Best regards,

Guillaume