The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

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.

On Sun, Jan 24, 2016, 11:48 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 01/24/2016 10:52 AM, Jonathan Leivent wrote:
> Hi Jason,
>
> How do you want to select the goal to be shown?  Is it the only one in
> focus?  Also, I noticed the delay between the setup of __Goal and the
> display - do you want that as well, or do you want to be able to show
> the proof at any point without prior setup?  Is that what you meant
> when saying it would be nice if you didn't need the refine?
>
> Note that you don't need the named evar creation below: "_" works in
> place of "?[__Goal2]".
>
> Anyway, I do have a way to do this, and can tailor it per your
> description.  See 4468 for some clues.
>
> -- Jonathan

On second thought, I don't think there is a way if you don't want
setup.  I don't think Ltac can see the past evolution of the proof in
proof terms it hasn't previously "captured".

If you are willing to live with the setup, then perhaps the only
improvement I could offer over what you already have here is that the
secondary "observer" goal would be trivially solvable regardless of the
rest of the proof, instead of being a clone of the original captured goal.

-- Jonathan

>
> On 01/24/2016 12:42 AM, Jason Gross wrote:
>> Is there a nice way to execute [Show Proof] from Ltac?  That is, I
>> want to
>> be able to do something like
>>
>>    let G := show_proof_term in
>>    idtac "Some prefix" G.
>>
>> or
>>
>>    show_proof_term_with_prefix "Some prefix".
>>
>> The best I've been able to come up with on short notice is:
>> Goal True /\ False.
>>    let G := match goal with |- ?G => G end in
>>    simple refine (let __Goal := _ : G in ?[__Goal2]); [ | shelve ].
>>    split.
>>    Unshelve.
>>    all: cycle -1.
>>    let G := (eval cbv delta [__Goal] in __Goal) in
>>    idtac "Some prefix" G.
>>
>> but I'm guessing that there's something fancy I can do with named
>> evars and
>> [instantiate] to execute the [idtac] in the context of __Goal2, but
>> I'm not
>> sure what it is.  (I'm basically fine with needing the [refine] at the
>> beginning of the proof, though it'd be nice if I didn't need it; I
>> mostly
>> want this so I can minimize a bug that depends on the output of [Show
>> Proof].)
>>
>> Thanks,
>> Jason
>>
>