Yannick Zakowski (May 10 2020 at 17:28): Yannick Zakowski (May 10 2020 at 17:28):Hello, I have a not very well defined question. Going through the documentation, I am quite confused about control flow operators. Nothing specific to Ltac2 is said about sequencing, iterating or looping, it appears that the same tactical as for Ltac1 are to be used (i.e. ;, repeat, and so on). But the two languages are sufficiently different that I am not entirely sure to understand how it can actually be the same tacticals, or what that would mean for it to have the same semantics when applied to both languages. Am I missing something obvious?
Kenji Maillard (May 10 2020 at 18:04):Ltac2's tacticals are a reimplementation of Ltac1's. Some of them are builtin (e.g. the definitions marked external in this file) and others are defined in standard Ltac2 (for instance repeat is defined here).
Documentation definitely needs to be refined so that you don't need to dive into the code each time you have a question (I guess PR are welcomed).
Yannick Zakowski (May 10 2020 at 18:19):Ah awesome that makes a lot of sense. Thanks Kenji!
I'll submit a PR if I reach a point where I can write a decent one.
Karl Palmskog (May 12 2020 at 14:51):on page 3 in the recent paper on Lean linting (https://arxiv.org/pdf/2004.03673.pdf), they define a linter as follows:
A linter is a wrapper around a metaprogram with type "declaration → tactic (option string)". Given an input declaration d, the test function returns none if d passes the test and some error_msg if it fails. These test functions work within the tactic monad in order to access the elaborator and environment, although some are purely functional and none modify the environment. The type linter bundles such a test function with formatting strings.
Does anyone (e.g., @Pierre-Marie Pédrot ) know how well this transfers to Ltac and Ltac2 and Coq in general? Could one bundle linters like they do, but for Coq?
Background: possibly we could use linters as defined there for reranking formatting suggestions (http://cozy.ece.utexas.edu/~palmskog/coqws20draft.pdf)
Enrico Tassi (May 12 2020 at 17:15):The "difficult" part is to have a description of declaration in the meta programming language.
In Elpi I'm working hard on this since I've a lot of use cases. Version 1.3 has Definition and Record, 1.4 will have also Inductive.
I'm hijacking a little the question, since it is in the Ltac2 stream: as far as I know Ltac2 does not provide a data type for global declarations, but it can surely be added.
Note that depending on the kind of "check" you want to implement the declaration data type may be good or not. For example the one I use in Elpi is an AST in HOAS style: you have already lost the input text and/or the locations of subterms (in terms of text offsets). So you would not be able to check indentation for example, but you could check naming conventions, unused parameters... If you want to access the location, then you would need a different type for declarations in you meta language of choice.
Karl Palmskog (May 12 2020 at 17:20):well, naming suggestions are the most sophisticated ones we have at the moment, so would be interesting to start there. For example, one could check/rerank names against a regexp. The stuff about exposing locations in some language (Elpi or Ltac2) can hopefully be discussed at the workshop or similar venue.
Gregory Malecha (May 20 2020 at 18:13):How would I convert a constr to a pattern? For example, suppose that I have forall a b, a + b = b + a. I would like to convert this to a pattern ?a + ?b and use context to search for that pattern in a term. Then I would like to get the substitution on that pattern and use it to instantiate the right-hand-side. For example, if context unifies my pattern with 1 + 2, I would like to get the substitution back and use it to instantiate the right hande side into 2 + 1.
Gregory Malecha (May 21 2020 at 14:15):Gregory Malecha said:
How would I convert a constr to a pattern? For example, suppose that I have
forall a b, a + b = b + a. I would like to convert this to a pattern?a + ?band usecontextto search for that pattern in a term. Then I would like to get the substitution on that pattern and use it to instantiate the right-hand-side. For example, ifcontextunifies my pattern with1 + 2, I would like to get the substitution back and use it to instantiate the right hande side into2 + 1.
@Janno would this be something easy to do in Mtac?
Janno (May 21 2020 at 14:16):I was actually going to reply with an Mtac solution but I thought it would derail the thread too much. I'll whip something up. It is definitely possible but the exact solution depends a lot on what you want out of it in terms of static guarantees!
Janno (May 21 2020 at 14:19):It would help to know which parts of this procedure are known at compile time. Is it always Nat.plus? If not, is it always something of the same type?
Gregory Malecha (May 21 2020 at 14:20):I'm basically looking for conjuncts in a separation logic assertion. So I have something like A * B * C (where those are like F 1 2, etc) and I'm looking for some pattern F a b or so.
Gregory Malecha (May 21 2020 at 14:21):The head symbols are definitions, so i don't need higher order unification
Gregory Malecha (May 21 2020 at 14:21):but they are not fixed apriori
Gregory Malecha (May 21 2020 at 14:22):it's fine though if you have a simpler version that i could look at though
Janno (May 21 2020 at 14:49):It's a bit longer than expected and it's missing a bunch of dependent types to avoid coercions but here is a prototype: https://gist.github.com/Janno/6cdfbd9fd525824b064092c01e58018c
Janno (May 21 2020 at 15:01):There are also quite a few caveats such as a) backtracking (our version of context doesn't backtrack at all, I think?) and b) the fact that the input pattern cannot be a template polymorphic inductive type (i.e. fun a => list a or just list is not going to work). That last one is probably not an issue here, though.
Théo Zimmermann (Jun 29 2020 at 15:32):It seems like Ltac2 questions at Coq's Discourse have not received many answers :disappointed:
https://coq.discourse.group/tag/ltac2
Irene Yoon (Aug 11 2020 at 21:40):Is there a way to focus on goals using 2 : { } syntax in Ltac2? I could use Focus 2, but 2 : { } only seems to work for "Ltac1 mode" ((ltac1:(2 : { ... }) doesn't seem to work, either)
Pierre-Marie Pédrot (Aug 11 2020 at 21:41):If it doesn't work, it's an oversight, you should probably open a bug.
Pierre-Marie Pédrot (Aug 11 2020 at 21:41):It's a bit strange though because I thought that the bullet syntax was language-agnostic
Irene Yoon (Aug 11 2020 at 21:42):Alright, thanks! I'll open an issue.
Théo Zimmermann (Aug 12 2020 at 08:15):@Pierre-Marie Pédrot Note that I already mentioned this issue in https://github.com/coq/coq/issues/12004, although this was to propose a more general solution.
Karl Palmskog (Aug 12 2020 at 08:18):so 2: is actually a bullet?
Théo Zimmermann (Aug 12 2020 at 11:39):No :confused:
Théo Zimmermann (Aug 12 2020 at 11:39):2: is a goal selector
Théo Zimmermann (Aug 12 2020 at 11:40):BTW, it is normal that ltac1:(2: { .. }) does not work because { } can only be used at top-level (like commands).
Karl Palmskog (Aug 12 2020 at 12:45):I referred to Pierre-Marie's comment:
I thought that the bullet syntax was language-agnostic
Or did he mean the { ... } then? (them being bullets would be even stranger)
Irene Yoon (Aug 12 2020 at 17:09):Given a “higher-order” tactic, what's the simplest way to generalize it to apply to a list of tactics?
For instance, if I have something simple like Ltac2 apply_tac tac := tac () , I wish to take in a list of tacs.
In particular, it looks like if I try pattern matching on "nil" in Ltac2, it gives an error that says Pattern not handled yet.
Pierre-Marie Pédrot (Aug 12 2020 at 17:28):What is not handled yet is complex pattern-matching.
Pierre-Marie Pédrot (Aug 12 2020 at 17:28):That is, with patterns that contain subpatterns.
Pierre-Marie Pédrot (Aug 12 2020 at 17:29):But any complex pattern-matching can be expanded manually (albeit tediously) into a simple one, so it doesn't endanger expressivity.
Pierre-Marie Pédrot (Aug 12 2020 at 17:30):In any case, you can write iter : ('a -> unit) -> list 'a -> unit for your use case.
Pierre-Marie Pédrot (Aug 12 2020 at 17:30):(it's already part of Coq 8.12 if you're using that version as Ltac2.List.iter)
Irene Yoon (Aug 12 2020 at 17:31):Oh neat, thanks!
Last updated: Oct 05 2023 at 02:01 UTC