The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi John,

I was going to suggest something like

  Goal exists (n : nat), n = 2.
    eexists.
    instantiate (1 := refine (S _)).

because "instantiate" can actually run tactics.  However, the above does not
work, saying

  Instance is not well-typed in the environment of ?n.

I am not sure how to get around that.  It's certainly possible to refine an 
evar
using new evars, just not this way I guess...

Kind regards,
Ralf

On 27.06.2018 21:58, 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
>