The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/26/2016 02:45 PM, Jonathan Leivent wrote:
> On 01/26/2016 02:13 PM, Jason Gross wrote:
> > Right, I think I do need the setup.  I was mainly wondering if I 
> > could get
> > rid of the Unshelve.  I think I saw a comment by you on some bug report
> > mentioning that instantiate works with named evars?  That seems like 
> > it'd
> > be enough to wrap the whole thing up into pre_show_goal, show_goal, and
> > post_show_goal tactics, with no vernacular needed.
>
> Oh, so you want the "observer" goal to remain hidden after the setup, 
> but to be recoverable later, correct?  So you are trying to make the 
> observer goal be a named evar, so that it is recoverable later by 
> name?  Here is an Ltac hack that can do that:
>
> Variable F : Type.
> Goal F.
> (*setup and shelve observer with evar name __Observer*)
> lazymatch goal with
> |- ?G => simple refine (let x := _ : G in ?[__Observer]); [|shelve]
> end.
> (*evolution of observed goal*)
> pose (x:=1).
> destruct x.
> (*recovery of observer*)
> unshelve instantiate (__Observer := _).
>
> Warning: this type of Ltac hackery is bound to incur the ire of the 
> devs.  Use at your own risk.
>
> -- Jonathan

If you also want the observer to be trivially solvable (so you can 
easily dispose of it later), you can do this:

Variable F : Type.
Goal F.
assert True as _;
[let E:=fresh in (*should have done this above, too*)
 simple refine (let E := ?[__Observed] in ?[__Observer])
|exact ?__Observed];
[|shelve].
pose (x:=1).
destruct x.
unshelve instantiate (__Observer := _).

(same warning, only more so)

-- Jonathan