Stream: Coq users

Topic: ✔ Creating subgoals with dependencies


view this post on Zulip James Wood (May 26 2022 at 14:36):

If I do something like Goal exists n, n < 2. then esplit., I get one goal with type ?n < 2. I can instantiate ?n up front by instead doing split with (x:=1).. Is there a tactic that will leave me with two subgoals: one being ?n : nat and the other being accessible when I have instantiated ?n with some expression n' via Ltac, with type n' < 2? A proof could then look like:

Goal exists n, n < 2.
  esplit'.  (* I'm asking what should go here. *)
  - exact 1.  (* Or I could have a more complex tactic script producing `1`. *)
  - auto.  (* Continue to prove `1 < 2`. *)
Qed.

view this post on Zulip Gaëtan Gilbert (May 26 2022 at 14:37):

unshelve eexists (or unshelve esplit but generally people use eexists for this)

view this post on Zulip James Wood (May 26 2022 at 14:38):

Thanks (and so quick)!

view this post on Zulip Notification Bot (May 26 2022 at 14:39):

James Wood has marked this topic as resolved.


Last updated: Feb 08 2023 at 22:03 UTC