Stream: Coq users

Topic: ✔ admit until later


view this post on Zulip 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.
...

view this post on Zulip Gaëtan Gilbert (Aug 31 2022 at 14:40):

shelve? used as

Goal nat -> False.
intro x;induction x.
- shelve.
- assumption.
Unshelve.
(* 1 goal for the 0 case *)

view this post on Zulip James Wood (Aug 31 2022 at 14:41):

Looks good, thanks! I'll give it a go.

view this post on Zulip Notification Bot (Aug 31 2022 at 15:48):

James Wood has marked this topic as resolved.

view this post on Zulip Pierre Courtieu (Sep 07 2022 at 10:03):

You can have a look at https://github.com/Armael/coq-procrastination.


Last updated: Jun 24 2024 at 12:02 UTC