[Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

[John Grosen]

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

[Jason -Zhong Sheng- Hu]

Hi John,


You can unify them:


Goal exists (n : nat), n = 2.
eexists.
match goal with
| [ |- ?x = _ ] =>
is_evar x;
let y := fresh "y" in
evar (y : nat); unify x (S y)
end.


If it's an existential variable, it should be able to unify with any expression of the same type. Does that deal with your problem?


Sincerely Yours,

Jason Hu
________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of John Grosen <***@mit.edu>
Sent: June 27, 2018 3:58:10 PM
To: coq-***@inria.fr
Subject: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

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

[John M Grosen]

Unfortunately not. In my more complicated actual use case, the existential variables have restricted contexts. As far as I'm aware, there's no exposed mechanism for to creating an existential variable with a context different from that of the goal you're currently in. If there is a way to do that, using unify would work.
________________________________
From: coq-club-***@inria.fr [coq-club-***@inria.fr] on behalf of Jason -Zhong Sheng- Hu [***@hotmail.com]
Sent: Wednesday, June 27, 2018 1:39 PM
To: coq-***@inria.fr
Subject: Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?


Hi John,


You can unify them:


Goal exists (n : nat), n = 2.
eexists.
match goal with
| [ |- ?x = _ ] =>
is_evar x;
let y := fresh "y" in
evar (y : nat); unify x (S y)
end.


If it's an existential variable, it should be able to unify with any expression of the same type. Does that deal with your problem?


Sincerely Yours,

Jason Hu
________________________________
From: coq-club-***@inria.fr <coq-club-***@inria.fr> on behalf of John Grosen <***@mit.edu>
Sent: June 27, 2018 3:58:10 PM
To: coq-***@inria.fr
Subject: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

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

[Ralf Jung]

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

Post by John Grosen
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
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
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

[Yannick Forster]

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

Post by Jason -Zhong Sheng- Hu
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

Post by John Grosen
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
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
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

[Ralf Jung]

Hi,

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

Ah, right, I forgot to add the `ltac:`. What Yannick wrote is what I meant. My
proposal probably parsed as the completely wrong thing.

; Ralf

[Soegtrop, Michael]

Dear Ralf, John,

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?

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commerc

[Ralf Jung]

Hi,

Post by Soegtrop, Michael
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

Post by Soegtrop, Michael
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], 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

[John M Grosen]

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-***@inria.fr [coq-club-***@inria.fr] on behalf of Ralf Jung [***@mpi-sws.org]
Sent: Thursday, June 28, 2018 1:36 AM
To: coq-***@inria.fr; Soegtrop, Michael
Subject: Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

Hi,

Post by Soegtrop, Michael
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

Post by Soegtrop, Michael
Best regards,
Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], 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

[Soegtrop, Michael]

Dear John,

then I don't understand your problem. If you want to instantiate the evar in the context of the current goal (rather than focus another goal in whose context the evar can be instantiated more easily), what is wrong with e.g.:

Goal exists (n : nat), n = 2.
eexists.
reflexivity.

Or maybe

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

Or in case you have an evar in a term:

Goal exists (n m : nat), n + m = 2.
eexists.
eexists.
match goal with
| [ |- ?x + ?y = _ ] => assert(x=0) as H by reflexivity; clear H
end.

The problem with your example is that you cannot possibly instantiate the evar with 0, because this would lead to 0=2. If none of the above works, it would help if you post a minimal sample which actually could work (doesn't lead to False) and whose solution would solve your issue. As is, it is hard to guess what your issue is.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: [phone], 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

[Armaël Guéneau]

Post by John M Grosen
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.

What about:

Goal exists (n : nat), n = 42.
eexists.
match goal with |- ?x = _ =>
pose (foo := x);
instantiate (1 := 42) in (Value of foo)
end.

In short, it looks like you can introduce a local definition for the
evar you just matched, and then the index of that evar will necessarily
be 1 when you instantiate _in that definition_ using Value of.

And you can still do `unshelve instantiate (1 := _) in (Value of foo)`
to get a goal corresponding to instantiating the evar.

[Gaëtan Gilbert]

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

Post by Yannick Forster
Hi all,
  Goal exists (n : nat), n = 2.
    eexists.
    instantiate (1 := ltac:(refine (S _))).
  S ?Goal0 = 2
Does this enable your idea again Ralf?
Best
Yannick

Post by Jason -Zhong Sheng- Hu
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

Post by John Grosen
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
   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
   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

[Robbert Krebbers]

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|].

Post by John Grosen
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
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
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