The Coq mailing list

[Yannick Forster <yannick AT yforster.de>]

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