Ssreflect Users Discussion List

[Enrico Tassi <>]

On Thu, Apr 03, 2014 at 06:57:21PM +0200, Pierre-Yves Strub wrote:
> On 02/04/2014 23:41, Enrico Tassi wrote:
> 
> >  move=> P Q R h; have [: p] := h p.
> 
> What the [: p] pattern is doing ? I never saw it (and greping all the .v
> gives me very few info...)

This is very new. [: p ] introduces a new abstract variable p.
Technically it is just an evar.

  move=> [: p].

  p : ?24
  =========
  G

  subgoal 2 is:
    ?24

Now, more concretely, image you have a proof that goes like that:

  have H : bla.
    ...
    have W : bar.
      ...
      by ...
    by ...
  ...

Then, later on, in the main proof, you discover you need W (where W may
not even be an extra fact proved with have, but just a proof of a
subgoal that you encountered while proving H).
You want to abstract out the inner have, to reuse this proof.
If it is already a sub proof delimited by an have and if it is your
lucky day you may end up with this:

  have W x (y : T) : bar.
    ...
    by ...
  have H : bla.
    ... (* x and y are created here *)
    by ...
  ...

where x and y are extra context items the proof of H generates before W.
But if these extra fact have complex types (T here) or if the subgoal is
not an have (hence you don't have W, you have to write it) then this
refactoring is tedious and inflates the script.  With this new feature
you can:

  have [: H1] H : bla.
    ...
    have W : bar.
      abstract: H1 x y.
      ...
      by ...
    by ...
  ...

The result is that after the main have tactic you have in your context
and extra H1, whose type is forall x (y : T), W  but you don't have to
reorganize the script and more importantly you don't have to write W or
T by hand:  W is the goal, and the things that needs to be quantified
are specified by name (no T to be written).

Now, having an H1 in the context with a type like ?24 is scary.  The
tactics occurring before the abstract: (that fixes ?24 to be forall x y,W)
may instantiate ?24 by mistake (not the ssreflect primitive tactics,
but if you use a standard coq tactic this may happen).  Hence [: H1]
generates something slightly more robust, and better printed, like

  H1: <hidden 1 >

that hides ?24 and protects it using a lock.  Then, when abstract: fixes
the type of H1, it also unlocks it, so one sees

  H1: forall x (y : T), W  (*1*)

where the (*1*) plays no role, if you rewrite /= in H1  it vanishes.

Abstract variables introduced with [: ] are always locked but for the
case in which they are combined with a have:= so that one can write:
  
  have [: n_lt3 ] @w : 'I_3 := Sub n n_lt3.
    by auto. (* proof of n < 3 *)
  
  n_lt3 : n < 3
  w : 'I_3 := Sub n n_lt3
  ======
  G

Here the @ flag (new in 1.5) tells have to generate a let-in
instead of a regular cut (otherwise said, removing it is like calling
clearbody w afterwards).
Note that one can achieve the same effect with this other form that
works better for bigger term constructions.  In this case, n_lt3 is locked.

  have [: n_lt3 ] @w : 'I_3.
    apply: (Sub n).
    abstract: n_lt3.
    by auto.

In this case you see why abstract: is called like that.  It plays the
role of coq's abstract tactic by hiding the subterm produced by auto,
while making it available later on as a local assumption.

For more details look at the Changes section in the user manual.

Bottom line, if Coq were Matita, move=> [: p ] /(_ p). would have made
Beta's day, but unfortunately, even if I generate p as unlocked, a low
level tactic that is called by move (apply_type) calls (the wrong?)
refiner and fails with the simply beautiful error message:

  Error: Refiner was given an argument "p" of type "?24" instead of "P".

Cheers
-- 
Enrico Tassi