Rodolphe Lepigre (May 28 2021 at 21:57): Rodolphe Lepigre (May 28 2021 at 21:57):Is it possible to check, in Ltac, that a term is closed (i.e., does not depend on any variable of the context)?
After talking a bit with @Janno earlier, I suspect the answer is no. My most promising attempt (or at least I thought so) was to create a fresh evar using evar (x : T) in an empty context, and then try to set it with instantiate (x := t), hoping that this would fail if variables escape there scope. However that does not work, since instantiate is perfectly happy to let variables escape their scope (you get an error at Qed time though).
According to @Janno I should be able to use Ltac2 (called from Ltac) to do what I want, but I have not been very successful in doing that yet. I must say that, so far, I have found the documentation of Ltac2 to be pretty unhelpful: it seems to have a high cost of entry. I'd really appreciate pointers to examples of code I could take inspiration from, or any tips Ltac2 experts could give me. Of course, I would not mind someone sharing an existing solutions to the problem!
Michael Soegtrop (May 29 2021 at 04:54):For Ltac2 there is a small tutorial here: (https://github.com/tchajed/ltac2-tutorial). I didn't go through it since it didn't exist when I learned it - I would be interested in your feedback. IMHO it doesn't take that long, a few days maybe, to learn the basics of Ltac2. I agree that it is not that obvious from the start, but I think it is much better than Ltac, which looks fairly obvious from the beginning and when you dig deeper it becomes very non obvious. Ltac2 is more the other way around. Please also note that there is a separate Zulip stream for Ltac2 questions.
Regarding your question: doing this in Ltac is complicated and slow, but possible. I did it a few years back but it requires concepts like a "quod libet sandbox": you run the script under the assumption that you can instantiate any type - a world from which you cannot return terms but boolean information about a term like the information if a term is closed. This is an invention of Jason Gross if I remember right. The quod libet helps to look at terms in the various ways you need to answer the question, e.g. it allows to supply arguments to a lambda so that you can do beta reduction and look into the function term.
In Ltac2 I would use Import Ltac2.Constr.Unsafe. which gives you a function kind which converts a Coq term into a Coq AST type you can go through in a recursive function and analyze it. Despite its name this is not unsafe, unless you go the other way around. For the deep analysis of terms, I think this is the way to go.
To get you started, I put a small gist with some code out of my Ltac2 learning phase here: (https://gist.github.com/MSoegtropIMC/cab461aa21b193cac06f5b6fdfa16e2b)
Please note that in Coq master, Ltac2 has a much nicer printing function - if you are bound to 8.13, I can send you my collection of "ad hoc ltac2 printing helpers".
Michael Soegtrop (May 29 2021 at 04:59):P.S.: the code in the gist is very old Ltac2 code before there was something like an if in Ltac2. The clumsy matches of booleans one would do with an if now.
Rodolphe Lepigre (May 29 2021 at 14:53):OK great, thanks! I'll have a look when I have a moment.
Jason Gross (Jun 01 2021 at 01:28):You can test whether or not exfalso; pose term as x; revert x; repeat match goal with H : _ |- _ => clear H end leaves any hypotheses in the context
Jason Gross (Jun 01 2021 at 01:30):And the sandbox tactic is assert_succeeds, and was indeed my contribution, refined over the years with the help of others
Michael Soegtrop (Jun 01 2021 at 09:55):Jason Gross said:
You can test whether or not
exfalso; pose term as x; revert x; repeat match goal with H : _ |- _ => clear H endleaves any hypotheses in the context
neat - I have to remember this!
And the sandbox tactic is
assert_succeeds, and was indeed my contribution, refined over the years with the help of others
I would say assert_succeeds is a building block for your quod libet method, but without an example it is far from obvious how to use it - maybe the reference manual should give a small example.
Last updated: Apr 16 2024 at 05:01 UTC