Ssreflect Users Discussion List

[Enrico Tassi <>]

On Sat, Apr 19, 2014 at 12:15:31PM +0200, Ralf Jung wrote:
> That's surprising to me. After all, even the current version creates a
> new existential with the apply. Why does it even do that at all then?
> Having a goal that just says "world" (where world is not a Prop) is
> nothing I would ever expect to see from applying a lemma. If apply: does
> not support evars, shouldn't it complain (like plain-Coq apply does)
> instead of behaving a bit like eapply, but then not really?

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.
You say one could just compute the sort and display only goals that live
in Prop, but this is not sufficient since one may want to put his
predicates in Type (all Homotopy Type Theory is done this way, for example).  
Coq 8.3 had data structures to represent the proof other than the list
of evars (assigned and not).  Coq 8.4 has only the list of evars, and a
sort of invariant is threaded along by tactics, so that only a subset of
the goals is shown.  Coq trunk is better, for example it is very
easy to hide the goal for ?midpoint (since ?midpoint occurs in the type
of other, not hidden, goals, and hence can be instantiated by side
effect).

My personal opinion is that one should have goals=evars, and eventually
have a tactic to hide (or better postpone) goals that may be solved
indirectly, like ?midpoint.  At least at the OCaml level, coq trunk is
like that.

>   Anomaly: Evd.define: cannot define an evar twice. Please report.

Sorry, I did not investigate that issue.

> >   apply: Pmono HP _ _.  (* that is expanded to apply: Pmono _ HP _ _. *)
> 
> 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.

> In this case, I can see how formulating the lemma slightly differently
> works out niceley. However, when dealing with lemmas that have much more
> premises, I will probably just fall back to using eapply - I used it a
> lot in my pre-SSReflect proofs, and I came to really enjoy the comfort
> of having to instantiate less variables. After my first experiments with
> SSReflect, I noticed that apply: behaves more like eapply than like
> apply, and I liked that a lot, so I was surprised to see that change
> after the update.

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

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

> Oh, views. During my first read through the documentation I did not
> really get what they were doing, so I'm afraid that so far, I simply do

Well, views are usually used to link a boolean concept with a Prop
concept, like andP that links && with /\.  Here I'm suggesting to use
the view application mechanism to apply arbitrary lemmas, that may not
be a good idea if you are not yet acquainted with views.

> > One last thing: the leading "by" applies to the whole line, and "by
> > apply" is very much like "exists". 
> 
> Sorry, I do not understand this part. Did you mean "exact"?

yes

ciao
-- 
Enrico Tassi