Ltac2

Stream: iris-lean

[Bas Spitters]

Parts of the iris proof mode are already implemented in the new Ltac2 tactic language. Has anyone considered porting Ltac2 to Lean? Something similar was done for the SSR tactic language already.
This might facilitate future porting.

[Shreyas Srinivas]

From a tactic programming point of view, the current lean framework seems better than the Ltac family

[Shreyas Srinivas]

Source : I played with both
Caveat : My "experience" with Rocq is less than with lean, although in iris, it is the other way around.

[Shreyas Srinivas]

Basically you program all the neatly typed stuff inside the MetaM monad after collecting arguments from the TacticM monad as metavariables. If you want quoting, there's Qq.

[Bas Spitters]

Ltac2 is very different from Ltac2. It's very close to ML.
https://rocq-prover.org/docs/metaprogramming-ltac2

If you have concrete suggestions on where Lean's tactic language is better, that would be useful. Rocq has several other possibilities of tactic programming, precise evaluation between them has started, but not concluded.

[Shreyas Srinivas]

The links for tutorials on that page all seem to link to github issues

[Shreyas Srinivas]

and some of those issues lead to broken links like this one : https://github.com/rocq-prover/platform-docs/blob/main/src/Tutorial_Ltac2_types_and_thunking.v

[Bas Spitters]

Here's a structural comparison:
https://hal.science/hal-05024207v3/preview/main.pdf#page=8.69

[Bas Spitters]

Shreyas Srinivas said:

The links for tutorials on that page all seem to link to github issues

Thanks. I'll report that.

[Shreyas Srinivas]

I am not sure I understand these lines in the lean section below:

Meta-programs can thus only build recursive functions using
primitive recursors. In practice recursors for nested inductives quickly become unwieldy. Generating
concrete syntax (instead of abstract syntax) solves this particular issue with fixpoints and case
expressions, but concrete syntax is very difficult to manipulate, and most functions in the Lean
meta-programming API (such as unification or type inference) do not work with concrete syntax

[Shreyas Srinivas]

One can easily work with TSyntax in the lean metaprogramming API. Is that what they mean by abstract syntax (I always thought that was Expr)

[Shreyas Srinivas]

CC : @Arthur Adjedj and @Henrik Böving

[Bas Spitters]

I don't know the details, but likely related to this recent article about an approved treatment of nested inductives in type theory https://hal.science/hal-05366368v1

[Shreyas Srinivas]

For context there is ongoing work on a mutual_induction tactic

[Shreyas Srinivas]

and I am not sure about nested inductives, but I never ran into issues with those (to be fair I didn't metaprogram with those).

[Shreyas Srinivas]

But I think it's best someone who knows these tactic languages deeply responds. I am more like an end-user of them (and more lean than Rocq), hence the CC.

[Shreyas Srinivas]

Found a good explanation of how nested inductive type recursors are compiled here : https://lean-lang.org/doc/reference/latest/The-Type-System/Inductive-Types/#nested-inductive-types

[Shreyas Srinivas]

They are translated to mutual inductive types

[Henrik Böving]

Bas Spitters said:

Here's a structural comparison:
https://hal.science/hal-05024207v3/preview/main.pdf#page=8.69

Their main complaint seems to be that Lean compiles pattern matching down to casesOn and match decls and there is no primitive in Expr if I'm seeing that correctly? While that is true this doesn't really strike me as an issue that occurs much in practice. I cannot recall people on this Zulip ever asking how to do this from the top of my head (doesn't mean it didn't happen, just to give an indicator of how often this is necessary). But it is indeed true that the API for getting your own PreDefinition in (from which these casesOn and friends are derived) is lacking, this might change in the future.

Regarding the porting of Rocq's tactic DSLs to Lean, the SSR tactic language port to Lean was done and, to the best of my knowledge, completely rejected by the community. Even the group that built the port (Ilya Sergey's team) has stopped using it for future projects. It feels rather likely that a hypothetical Ltac2 port would meet a similar fate. The comfort from just being able to write Lean all the time is far too compelling. The case study also understates how important this is IMHO. The fact that Lean tactics are written in Lean causes countless synergy effects:

• you get amazing editor support for free when writing a tactic. People porting Ltac2 would have to invest a ton of effort into integrating the language with all of this
• all of the work done by the FRO stdlib team directly benefits you in your tactic writing, you get all the latest and greatest convenience APIs for free
• all of the work done by the FRO on optimization, in the elaborator, the compiler etc. also directly benefits your work for free
• you get logging, profiling etc. all for free

In summary, the decision to have Lean be extensible with Lean is not because core was too lazy to develop another DSL or something like that, it is a calculated decision that has benefited Lean 4 tremendously over the years.

Also, just from a glance at the Lean section I'm a bit wary of this case study, e.g. the claim that Option.casesOn is a primitive recursor is wrong (check the output of #print Option.casesOn), there might be more things I didn't catch at first sight:
image.png

[Bas Spitters]

Thanks!
I wasn't suggesting Ltac2 as a replacement for the Lean tactic language, just as a possibility to facilitate porting Rocq code to Lean.
Having said that, Ltac2 is still not widely used, so it's unclear how much it would help right now, but it may be convenient for parallel Rocq/lean development, as in iris.

Alternatively, maybe there should be a direct translation from Ltac2 to lean's tactic language.

[Yannick Forster]

Henrik Böving said:

I cannot recall people on this Zulip ever asking how to do this from the top of my head

I think the main questions asked about this aspect of the work were in #lean4 > Recursive definition in `Expr` (but I might be wrong, I just searched for questions @Mathis Bouverot-Dupuis asked here)

[Yannick Forster]

Also I / we agree with your list of pros Henrik :) One clear conclusion of the case study was that one definitely wants to work in the language of the ITP itself -- in Lean that means one wants to use Lean as meta-programming language, no external language or DSL

[Yannick Forster]

If we actually got something wrong about the treatment of PreDefinition / Expr / casesOn we're more than happy to fix it :)

[Henrik Böving]

Bas Spitters said:

Thanks!
I wasn't suggesting Ltac2 as a replacement for the Lean tactic language, just as a possibility to facilitate porting Rocq code to Lean.
Having said that, Ltac2 is still not widely used, so it's unclear how much it would help right now, but it may be convenient for parallel Rocq/lean development, as in iris.

I think the needs of a good Lean tactic diverge quite a bit from what you can reasonably express in an auto translation from ltac. You will want to have logging/profiling nodes, in particular also proper management of contexts for that logging, potentially managing error locations etc. It might be good if you want to get a prototype in Lean but if you really want to build something that works well it will have to be lean specific. In which case, why not use Lean anyway.

Yannick Forster said:

Also I / we agree with your list of pros Henrik :) One clear conclusion of the case study was that one definitely wants to work in the language of the ITP itself -- in Lean that means one wants to use Lean as meta-programming language, no external language or DSL

That's great to hear!

Yannick Forster said:

If we actually got something wrong about the treatment of PreDefinition / Expr / casesOn we're more than happy to fix it :)

Nothing apart from the fact that Option.casesOn is not a primitive recursor jumped at me right away.

[Shreyas Srinivas]

Shreyas Srinivas said:

I am not sure I understand these lines in the lean section below:

Meta-programs can thus only build recursive functions using
primitive recursors. In practice recursors for nested inductives quickly become unwieldy. Generating
concrete syntax (instead of abstract syntax) solves this particular issue with fixpoints and case
expressions, but concrete syntax is very difficult to manipulate, and most functions in the Lean
meta-programming API (such as unification or type inference) do not work with concrete syntax

@Yannick Forster : for me the question is, what does it mean to be difficult to work with concrete syntax here. Like what's the typical example that's easier in a different tactic language than lean

[Henrik Böving]

You can build non trivial recursive functions in Rocq easier than in Lean because its Expr equivalent has a fixpoint operator

[Shreyas Srinivas]

Off the top of my head, it seems correct if you mean I can't just, 1. get the goal 2. match is syntactically without quoting and lifting monads, then it seems right.

[Shreyas Srinivas]

Henrik Böving said:

You can build non trivial recursive functions in Rocq easier than in Lean because its Expr equivalent has a fixpoint operator

Oh okay, so the concern is less with superficial syntax, specifically the bit about "but concrete syntax is very difficult to manipulate, and most functions in the Lean
meta-programming API (such as unification or type inference) do not work with concrete syntax"

[Mathis Bouverot-Dupuis]

Henrik Böving said:

Nothing apart from the fact that Option.casesOn is not a primitive recursor jumped at me right away.

Indeed it's a wrapper around the actual recursor Option.rec! Thanks for pointing this out.