Ssreflect Users Discussion List

[Georges Gonthier <>]

I hope not; HO unification in Coq is already complex enough, it doesn't need extra code to defer assignment to certain evar occurrences.

Sent from Windows Mail

From: Pierre-Yves Strub
Sent: ‎Monday‎, ‎22‎ ‎February‎ ‎2016 ‎20‎:‎03
To: Georges Gonthier
Cc: ssreflect mailing list, Guillaume Melquiond

But in Guillaume's mail, it seems that there is a dissymmetry between
the 2 evars (namely ?[n] and ?n). Is only one is subject to
instantiation ?

Best,
-- Pierre-Yves.

2016-02-22 20:58 GMT+01:00 Georges Gonthier <>:
> Strictly speaking, this isn't entirely new, since you could already write
>    rewrite (_ : let n := _ in n + 3 = 3 + n).
> The new syntax is, of course, more concise (but it's new syntax …).
>   Georges
>
> Sent from Windows Mail
>
> From: Guillaume Melquiond
> Sent: ‎Monday‎, ‎22‎ ‎February‎ ‎2016 ‎18‎:‎39
> To: ssreflect mailing list
>
> 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