coq-club AT inria.fr
Subject: The Coq mailing list
List archive
RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?
Chronological Thread
- From: John M Grosen <jmgrosen AT mit.edu>
- To: "coq-club AT inria.fr" <coq-club AT inria.fr>
- Subject: RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?
- Date: Wed, 27 Jun 2018 21:37:33 +0000
- Accept-language: en-US
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jmgrosen AT mit.edu; spf=Pass smtp.mailfrom=jmgrosen AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-1.mit.edu
- Ironport-phdr: 9a23:56uIDR9oVAHEjv9uRHKM819IXTAuvvDOBiVQ1KB41ugcTK2v8tzYMVDF4r011RmVBduds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55zebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRh/2hikaKz43/mLZisJyg6JavB2uqAdyzJTIbIyRLvdyYr/Rcc4cSGFcXshRTStBAoakYoULCOoBPeBYpJT6qVATrBW+Hw6sBPjxxT9Om3T72q860+EuEQHc2wwgBMwBsHLPodXwNacSTfq5w7fVwjXedv5b3yr25ovQch05vP2BXqh8fM7LxUUxFw7JlEicpZL9Mz+I1ekBqWqW4/BiWO6ykWIqqwV8riCyysotjoTFnJwZx1DL+Clj3oo5P8C0RUxlbdOiDZBerTuVN5FsTcMnW2xouDg1yrkBuZOjYScKzZUmywfaa/OdcoiI5gnjW/iNLjthn3JqZKiwhxC08Ue+0O3wT9S43ExPripEjtnArG4C2AHO6sSfS/t9+Fmu2SqX2gzO6exIO0Q5mbDFJ5Mh2LI8i4QfvVzGHiDsmUX2iKGWdl8j+uit8+nnYLDmppCGN49zkQHxLKIul9e6AeQ5LggCRXaU9vmh1LH75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKWMNbr4R57JM3LrkbH7fL875VQWgF44yska7JZJAJkAJujyUwn/roqLIAU+NlmWxObhQPA1+ZkZQm+JSvubNazItkSF4MoqIvXKaYMI7mWuY8M57uLj2Cdq0WQWerOkiMNOOSKIW89+KkDcWkLCx9IIEGMEpA07Hb7viUHEXDJONS/rA/AMowojAYfjNr/tA5i3ie3T2SanWJBaezIeUw3eITLTb4yBHsw0RmeSL8tmyWVWWb2zDooo1BW1uQS/0LFuKOzZ4GhB85fiyJ546/CBzRw=
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-request AT inria.fr [coq-club-request AT inria.fr] on behalf of Jason -Zhong Sheng- Hu [fdhzs2010 AT hotmail.com]
Sent: Wednesday, June 27, 2018 1:39 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?
Sent: Wednesday, June 27, 2018 1:39 PM
To: coq-club AT 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.
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?
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of John Grosen <jmgrosen AT mit.edu>
Sent: June 27, 2018 3:58:10 PM
To: coq-club AT inria.fr
Subject: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?
Sent: June 27, 2018 3:58:10 PM
To: coq-club AT 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
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
- [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John Grosen, 06/27/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Jason -Zhong Sheng- Hu, 06/27/2018
- RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John M Grosen, 06/27/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Yannick Forster, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
- RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Soegtrop, Michael, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
- RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John M Grosen, 06/29/2018
- RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Soegtrop, Michael, 06/30/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Armaël Guéneau, 06/30/2018
- RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John M Grosen, 06/29/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
- RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Soegtrop, Michael, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Gaëtan Gilbert, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Yannick Forster, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Robbert Krebbers, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Jason -Zhong Sheng- Hu, 06/27/2018
Archive powered by MHonArc 2.6.18.