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: Sep 30 2023 at 05:01 UTC