Stream: Coq users

Topic: Instantiating eapply existential?


view this post on Zulip Roger Bosman (Jun 29 2021 at 08:45):

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 eapply or eexists introduce this other kind of existential. Is there a tactic I can call that sets this existential to whatever I pass it?

view this post on Zulip Yannick Forster (Jun 29 2021 at 08:49):

Yes, it's the instantiate tactic: https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.instantiate

view this post on Zulip Roger Bosman (Jun 29 2021 at 09:18):

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?

view this post on Zulip Théo Winterhalter (Jun 29 2021 at 09:19):

instantiate (1 := t)

view this post on Zulip Roger Bosman (Jun 29 2021 at 09:21):

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?

view this post on Zulip Gaëtan Gilbert (Jun 29 2021 at 09:22):

instantiate is annoying that way, I would rather use unshelve

view this post on Zulip Théo Winterhalter (Jun 29 2021 at 09:23):

To be honest I don't know…
Note that alternatively and more robustly you can also use

unshelve eexists.

view this post on Zulip Yannick Forster (Jun 29 2021 at 09:42):

Sometimes named existential variables are also an option:

Goal exists n, n = 6.
Proof.
  eexists ?[six].
  instantiate (six := 6).

view this post on Zulip Roger Bosman (Jun 29 2021 at 09:45):

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

view this post on Zulip Théo Winterhalter (Jun 29 2021 at 09:48):

Then you can use unshelve eapply.

view this post on Zulip Pierre Courtieu (Jul 01 2021 at 11:05):

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.

view this post on Zulip Pierre Courtieu (Jul 01 2021 at 11:07):

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