Ssreflect Users Discussion List

[Ralf Jung <>]

Hi Enrico,

> It may seem odd, but goals and evars are the same thing: an evar stands
> for a missing term.  For example when you state a lemma
> 
>   Lemma foo : forall n, n >= 0.
>  
> you are morally doing
> 
>   Definition foo := ( ?1 : forall n, n >= 0 ).
> 
> and then the goal you see is the type of the only uninstantiated
> evar ?1.  Now, if you eapply the transitivity of the order relation, what
> you are doing is giving a partial solution for ?1, something like
> 
>   leq_trans ?midpoint n 0 ?h1 ?h2
> 
> where (?h1 : n >= ?midpoint) and (?h2 : ?midpoint >= 0).  So you have 3
> goals, one is the natural number (?midpont : nat), plus the two
> inequalities you expect.

I see, that makes a lot of sense.
Thanks for the explanation.

>> So the first three examples make perfect sense for me, and one of them
>> is probably what I would use if I had to use apply: to get the goal done.
>> However, I do not understand the last one. In my understanding, "apply:
>> A B C D" pushes D, C, B, A (in that order) from the context onto the
>> goal, then uses the topmost one (A) to apply it to the rest of the goal.
>> In other words, I assumed "apply: <list of names>" is the same as "move:
>> <list of names>; apply." (and, in general, I expected this to hold for
>> any tactic where I can use ":").
> 
> This is unfortunately not true.  The ":" for apply and exact is just
> a marker to distinguish between the SSR version from the coq version:
> it is not the colon tactical as you (and many others would) expect.
> In practice:
> 
>   apply: a b c.
> 
> is a synonym for
> 
>   apply (a b c) || apply (a _ b c) || apply (a _ _ b c) ...
> 
> not for
> 
>   move: c b a; apply.
> 
> it leaves the possibility of calling standard coq apply tactic, but is
> misleading.  I think it is like that for historical reasons.
> Georges can explain better this choice I guess.

Oh, that explains my confusion ;-) . So it has this special-case magic
to guess some of the first arguments applied to a. Good to know :)

> I think that what you want is to be able to write
> 
>   apply: ...; something.
> 
> where "something" hides a class of subgoals.  This something is called
> "shelve_unifiables" in coq trunk (at the OCaml level, dunno if it is
> exported as a tactic).

Something like that would be great, yes . and maybe some way to do this
per default, as personally I don't see a reason to ever not "shelve"
these evars which appear in other goals - but it seems you disagree on that.

> As of today, I'm afraid you have to play with "first last" or, as I
> suggested, reformulate your lemmas.

Okay.

Kind regards
Ralf