The Coq mailing list

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

Thanks for all your help.

Unfortunately, the instantiate + refine trick doesn't help in my scenario. In 
particular, I don't know the index of the existential variable I want to 
instantiate. Trying it with the expression directly doesn't work:

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

fails with error "Ltac variable x is bound to ?n which cannot be coerced to a 
fresh identifier.". I could imagine using some fancy Ltac to figure out the 
index of the evar I want to instantiate, but given that this doesn't work:

  let x := 1 in instantiate (x := 0).

(failing in a similar manner), I don't think that approach would succeed 
either.

The unshelve suggestions are appreciated, but I don't think it solves my 
grander issue: I want to essentially extend Coq's unification procedure for 
existential variables depending on what the current goal looks like, but this 
could be many proof steps down the line from the initial creation of the 
evar, so just having the evar as a proof goal somewhere doesn't help much 
automation-wise.

It could be the case that my situation is too complicated to use Coq's 
existential variables, and instead I should do some explicit reasoning with 
sigma types. That would be unfortunate, though...
________________________________________
From: 
coq-club-request AT inria.fr
 
[coq-club-request AT inria.fr]
 on behalf of Ralf Jung 
[jung AT mpi-sws.org]
Sent: Thursday, June 28, 2018 1:36 AM
To: 
coq-club AT inria.fr;
 Soegtrop, Michael
Subject: Re: [Coq-Club] Is it possible to perform tactics in an existential's 
context from Ltac?

Hi,

> isn't the problem of John that he can't instantiate the evar in the context 
> of the current goal? It was stated before that an evar can be unified with 
> any term of the same type. But this might not work in practice, because the 
> resulting term might not be well typed in the context, in which the evar 
> was created.
>
> John suggested to focus on the evar itself as goal, because then obviously 
> one would be in the right context to construct a well typed term for the 
> evar. Are there other methods? If not, how can one focus an unnamed evar?

John was asking about something like `only [n]: refine (S _)` for unnamed 
evars,
and the answer is `instantiate (1 := ltac:(refine (S _)))`.
Admittedly, that's still not focusing in the sense of actually bringing the
context on the screen in CoqIDE/ProofGeneral.  I don't know how to do that 
even
for named evars...

Kind regards,
Ralf

>
> Best regards,
>
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928
>