The Coq mailing list

[John M Grosen <jmgrosen AT mit.edu>]

Unfortunately not. In my more complicated actual use case, the existential variables have restricted contexts. As far as I'm aware, there's no exposed mechanism for to creating an existential variable with a context different from that of the goal you're currently in. If there is a way to do that, using unify would work.

---

From: coq-club-request AT inria.fr [coq-club-request AT inria.fr] on behalf of Jason -Zhong Sheng- Hu [fdhzs2010 AT hotmail.com]
Sent: Wednesday, June 27, 2018 1:39 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

Hi John,

You can unify them:

  Goal exists (n : nat), n = 2.
    eexists.
    match goal with
    | [ |- ?x = _ ] =>
      is_evar x;
      let y := fresh "y" in
      evar (y : nat); unify x (S y)
    end.

If it's an existential variable, it should be able to unify with any _expression_ of the same type. Does that deal with your problem?

Sincerely Yours,

Jason Hu

---

From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of John Grosen <jmgrosen AT mit.edu>
Sent: June 27, 2018 3:58:10 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

 

I am currently dealing with a problem in which I have an existential
variable in the goal and want to apply a lemma to the goal, but Coq's
unifier is not powerful enough to automatically unify the relevant part
of the lemma with the evar. However, in this particular case, it is
programatically obvious how to unify them, so I would like to write some
Ltac to do so. Imagine this (greatly simplified) example:

  Goal exists (n : nat), n = 2.
    evar (n : nat).
    exists n.
    only [n]: refine (S _).

This works, but I usually don't have a name for the existential
variables I'm dealing with and the automation certainly doesn't know
about any. So what I'd like to do is this:

  Goal exists (n : nat), n = 2.
    eexists.
    match goal with
    | [ |- ?x = _ ] =>
      only [x]: refine (S _)
    end.

However, Coq complains with "No such goal." As far as I can tell, this
is because the argument in "only [_]" is a syntactic identifier.

Then, is there any way to select a goal with a non-syntactic identifier,
like I have in this situation?

Thanks,
John