## Stream: Coq users

### Topic: Instantiating eapply existential?

#### 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?

#### 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

#### 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?

#### Théo Winterhalter (Jun 29 2021 at 09:19):

`instantiate (1 := t)`

#### 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?

#### Gaëtan Gilbert (Jun 29 2021 at 09:22):

instantiate is annoying that way, I would rather use unshelve

#### 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.
``````

#### 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).
``````

#### 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

#### Théo Winterhalter (Jun 29 2021 at 09:48):

Then you can use `unshelve eapply`.

#### 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.

#### 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: Jun 18 2024 at 08:01 UTC