James Wood (Aug 31 2022 at 14:37): James Wood (Aug 31 2022 at 14:37):When I'm in the middle of writing a proof with lots of cases, it will often look like the code below. I've made various amounts of progress in each of the cases, and used admit when it got too difficult to do right away, so that I can carry on with later easier cases. When I come back to fill in the admits, the later completed proofs live in the unchecked part of the buffer. I could keep the completed proofs in the checked part by doing a complex reordering of the subgoals, but this is too faffy. What I'd like is an alternative to admit which defers the goal until some later point, a bit like how Program defers unsolved evars into obligations. Is there such a mechanism?
induction x.
- exact foo.
- admit.
- prove.
by this.
- start.
admit.
...
shelve? used as
Goal nat -> False.
intro x;induction x.
- shelve.
- assumption.
Unshelve.
(* 1 goal for the 0 case *)
Looks good, thanks! I'll give it a go.
Notification Bot (Aug 31 2022 at 15:48):James Wood has marked this topic as resolved.
Pierre Courtieu (Sep 07 2022 at 10:03):You can have a look at https://github.com/Armael/coq-procrastination.
Last updated: Oct 01 2023 at 18:01 UTC