Allow Ltac2 notations from within Ltac1

[ppedrot]

This is preliminary work to check that the design aligns with the requirements of the people who asked for this feature.

This PR adds a new Ltac2 vernacular command of the form

Ltac2 Ltac1 Notation ...

which follows the same syntax as the Ltac2 Notation but instead as adding the notation as an Ltac2 syntax, it adds it into the Ltac1 grammar. For instance, the following works.

Require Import Ltac2.Ltac2.

Require Import Ltac2.Printf.

Ltac2 Ltac1 Notation "printme" c(constr) : 5 := printf "%t" c.

Set Default Proof Mode "Classic".

Goal True.
Proof.
printme (nat -> nat). (* prints "nat -> nat" *)
Abort.

Voluntary limitation: no Ltac1 variable can be accessed from the Ltac2 notation. This will never be fixed because Ltac1 variables are a true can of worms, and the only reasonable solution is to reuse the one from the ltac2:(... |- ...) quotation, i.e. explicit quantification, but that defeats the purpose of the notation.

TODO:

• [ ] Bikeshed the syntax
• [ ] Write documentation / tests

[ppedrot]

cc @Janno

[JasonGross]

Voluntary limitation: no Ltac1 variable can be accessed from the Ltac2 notation. This will never be fixed because Ltac1 variables are a true can of worms, and the only reasonable solution is to reuse the one from the ltac2:(... |- ...) quotation, i.e. explicit quantification, but that defeats the purpose of the notation.

I'm a bit confused. Why couldn't we do Ltac2 Ltac1 Notation "printme" c(ltac1val) := ... or some such, such that if you specify that something is an Ltac1 variable it will let you pass Ltac1 variables but nothing else?

[Blaisorblade]

FTR: See https://coq.zulipchat.com/#narrow/stream/278935-Ltac2/topic/Exposing.20Ltac2.20variadic.20notations.20in.20Ltac1 for extra context.

[Blaisorblade]

cc @robbertkrebbers

[ppedrot]

such that if you specify that something is an Ltac1 variable it will let you pass Ltac1 variables but nothing else

I guess we could hack something so that the notation elaborates to let f := ltac2:(VARS |- t) in f ARGS in Ltac1, but there will be the usual caveats with values vs thunks and it might lead to confusing behaviours.

[Janno]

I don't quite understand the limitation around ltac1 variables. Could somebody post an example that isn't accepted but would be useful to have?

Apart from that, my tests show that this MR does exactly what I expected. It's great! It is hard to overstate how much better Ltac2 notations are compared to their Ltac1 counterparts.

I like the current syntax. It feels natural and logical.

[ppedrot]

Could somebody post an example that isn't accepted but would be useful to have?

This means that you can't compose these notations with Ltac1 let-bindings or function arguments. For instance, this will not work:

Ltac2 Ltac1 Notation "foo" c(constr) := ...

Fail Ltac bar x := foo x.

(* with Ltac1 proof mode set *)
Goal True.
Fail match goal with [ |- ?P ] => foo P end. 

[JasonGross]

Does match goal with [ |- ?P ] => foo (P) end. work? (I think this is the standard trick for turning an Ltac1 variable into a constr?)

Edit: also, does match goal with [ |- ?P ] => foo (match P with Q => Q end) end. work?

[ppedrot]

Neither will work. Ltac1 variables live in a different environment from Ltac2 variables. (And most of the time, the Ltac1 runtime does a lot of efforts to recognize that something might be a bound variable even when it's not.)

[Janno]

Thanks for the examples! I personally do not see this as a huge drawback for the use cases I had in mind but I understand that this might affect other developments differently. I am mostly looking for a way to provide the full API of custom Ltac2 tactics in Ltac1 proof scripts without the proof script using ltac2:() everywhere. Right now we have to define a combinatorial number of Ltac1 wrappers for Ltac2 tactics with multiple options and this has made us hesitant to expose more options to clients of the tactic. (Of course there is also the problem of not being able to parse Ltac2 strings, lists, and other types like that in Ltac1 notations which made it practically impossible to expose certain options to clients.)

[Blaisorblade]

The limitation seems hard to avoid — and if only means that when a tactic migrates to Ltac2 + wrapper notations and takes arguments, automation on top should move to ltac2; this still allows migrating "leaf" tactics to ltac2, and those can still use FFI to ltac1. For instance, I hope we could migrate variadic ltac1 Iris tactics like iIntros to use this kind of notation, and add further variadic tactics that wouldn't be feasible to write today; https://gitlab.mpi-sws.org/iris/iris/-/issues/452 had initial ideas.

[Janno]

@ppedrot what needs to happen to get this in?

[ppedrot]

I think that the TODO list from the top post is still pretty much relevant. Help welcome for the doc.

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[SkySkimmer]

Bikeshed the syntax

Would this make sense as an attribute? eg #[in(ltac1)] Ltac2 Notation ... Then maybe we could even have #[in(ltac1, ltac2)] Ltac2 Notation ...

[ppedrot]

No attributitis, please. Attributes are flags to tweak the behaviour of commands that make sense when there can be several of them. That's the reason why they were introduced. Here we definitely want a distinct command.

[SkySkimmer]

Here we definitely want a distinct command.

Do we really though?

[ppedrot]

The semantics is not the same and we may want a different syntax to handle external Ltac1 variables and such.

[coqbot-app[bot]]

The "needs: rebase" label was set more than 30 days ago. If the PR is not rebased in 30 days, it will be automatically closed.

[rlepigre]

@ppedrot is this blocked on anything? This would still be amazing to have!

[ppedrot]

We discussed this a bit yesterday with @SkySkimmer and some parts of the design are still not extremely clear, especially the interaction with the ambient Ltac1 world. I think we need a bit more feedback on the kind of needs from the users before committing to an implementation.