coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Jason Gross <jasongross9 AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] [Show Proof] from Ltac?
- Date: Sun, 24 Jan 2016 05:42:20 +0000
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi0-f51.google.com
- Ironport-phdr: 9a23:E77iNBbGKR2WxASJAMem/Qb/LSx+4OfEezUN459isYplN5qZpcm7bnLW6fgltlLVR4KTs6sC0LqI9fm4Bidavc/JmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipduKO1oD3mbkKZpJbzyI7izp/vEMhoVjLqtjgjDomVBvP9ps+GVzOFiIlAz97MrjtLRq8iBXpu5zv5UYCfayLOwESulTCy1jOGQo7oW/vh7aCACL+3E0U2MMkxMODRKTvz/gWZKkkCLhsew19zOdJta+GbI9QjOk4L1sUwS5oCgCPj89tmrQj5oj3+pgvBu9qkknkMbva4aPOa8mcw==
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
- [Coq-Club] [Show Proof] from Ltac?, Jason Gross, 01/24/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/24/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/24/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jason Gross, 01/26/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/26/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/26/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/26/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jason Gross, 01/26/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/24/2016
- Re: [Coq-Club] [Show Proof] from Ltac?, Jonathan Leivent, 01/24/2016
Archive powered by MHonArc 2.6.18.