James Wood (May 26 2022 at 14:36): 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.
unshelve eexists (or unshelve esplit but generally people use eexists for this)
James Wood (May 26 2022 at 14:38):Thanks (and so quick)!
Notification Bot (May 26 2022 at 14:39):James Wood has marked this topic as resolved.
Last updated: Sep 26 2023 at 11:01 UTC