The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

I am not sure if this is what you are looking for, but just in case:

  Goal exists (n : nat), n = 2.
  unshelve eexists; [refine (S _); shelve|].

On 06/27/2018 09:58 PM, John Grosen wrote:
> 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