Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Apr 02, 2014 at 10:28:31PM +0200, Beta Ziliani wrote:
> Hi list,
> 
> I have a (probably stupid) question regarding ssr tactics.  Say that I
> have the following simple goal:
> 
> (P -> Q) -> R
> 
> and I'd like to get Q with a proof of P.  If I have a proof of P,

It is late, and it is almost black magic... maybe tomorrow I'll find
something simpler than that...

  move=> P Q R h; have [: p] := h p.

If only I had added a different syntax for unlocked abstract variables,
one could have written the more idiomatic:

  move=> P Q R [: p] /(_ p).

That reads: "Introduce P Q R, assume the proof p of a statement I'll
choose later on, then specialize the next hyp (namely P -> Q) using p
(that also choses a type for p, namely P)".

And given the "refiner" we work with, unlocking p on the fly is not
possible I'm afraid.  Damn!  In any case, all of this is 1.5 only.

Ciao
-- 
Enrico Tassi