The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

You can do "unshelve instantiate (1 := _)" to get the evar in your goal 
list, or "instantiate (1 := ?[foo])" to give it a name.

Maybe we could extend the toplevel selector to be able to take names, 
then you could do "[n]: { tac. tac'. ... }" (after giving it a name).

Gaëtan Gilbert

On 28/06/2018 09:41, Yannick Forster wrote:
> Hi all,
>
> Ralf's example works using inline ltac:
>
>    Goal exists (n : nat), n = 2.
>      eexists.
>      instantiate (1 := ltac:(refine (S _))).
>
> This produces:
>
>    S ?Goal0 = 2
>
> Does this enable your idea again Ralf?
>
> Best
> Yannick
>
> On 28/06/18 07:37, Ralf Jung wrote:
> > 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