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?

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

```
unshelve eexists.
```

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 `unshelve eapply`

.

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