We can instantiate an existential variable with the
exists tactic, as long as we have an actual
exists in the hypothesis we apply it to. However, tactics like
eexists introduce this other kind of existential. Is there a tactic I can call that sets this existential to whatever I pass it?
Yes, it's the
instantiate tactic: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.instantiate
I'm not sure how to use this? If you have
exists x. x = x and you call
eexists you get the goal
?x = ?x. But
instantiate (?x = ...) is not accepted?
instantiate (1 := t)
Thanks! I'm guessing the
1 stands for the first existential, which makes sense if we only have one. If we have more, can I print their order, or figure it out some other way?
instantiate is annoying that way, I would rather use unshelve
To be honest I don't know…
Note that alternatively and more robustly you can also use
Sometimes named existential variables are also an option:
Goal exists n, n = 6. Proof. eexists ?[six]. instantiate (six := 6).
Thanks for your answers :) Most the existentials I encounter in this way occur because of
eapply H and I am trying to avoid typing
eapply (H _ _ _ _ _ _ thing) so naming it is not really an option as then I might as well instantiate it in the eapply expression
Then you can use
You may want to have a look at library LibHyps, and in particular to the
especialize tactic and its variants. https://github.com/Matafou/LibHyps
especialize H at *. (* create a subgoal for each (dependent) premise of H. Cf "exploit" from CompCert. *) especialize H at 2,3,4 (* up to 7 premise number *) especialize H until 3 (* create goals for the n first (dependent) premises of H. *)
H can be a term.
if you need only the
at * then you may also look at the
exploit tactic in CompCert.
Last updated: Jan 31 2023 at 13:02 UTC