What are the rules for shadowing Ltac2 tactics?

Using Coq
1

First, a bit of background about my motivations. I’m using the -noinit option (with manual loading of certain plugins to re-enable tactics), so certain basic tactics don’t really work. One such set of tactics is reflexivity, symmetry and transitivity. If run (in an otherwise valid proof state), we get something along the lines of

Tactic failure: The relation R is not a declared reflexive relation. Maybe you need to require the Coq.Classes.RelationClasses library.

which obviously doesn’t work very well in a -noinit environment (unless I wanted to pull in a good chunk of the standard library).

What worked with Ltac1 was simply defining new tactics to override these three. I tried doing the same thing with Ltac2, and I came across a situation that I find confusing. This example works without -noinit. For the sake of reproducibility, I’m using the master branch of Coq (commit a5998b06ccf2367f7d1e58dc80e4237754c953bc).

Require Import Ltac2.Ltac2.

Ltac2 reflexivity0 () := Message.print (Message.of_string "Successfully overridden").
Ltac2 Notation reflexivity := reflexivity0 ().
Ltac2 symmetry0 () := Message.print (Message.of_string "Successfully overridden").
Ltac2 Notation symmetry := symmetry0 ().

Goal forall {A: Type} (R: A -> A -> Type) (x: A), R x x.
Proof.
    reflexivity. (* Prints "Successfully overridden" *)
    Fail symmetry. (* Prints the error message from the standard `symmetry` *)
Abort.

As you can see, reflexivity gets overridden with the new tactic, but symmetry still uses the old one. I’ve tried lots of variations here (like directly using Ltac2 symmetry () := Message.print (Message.of_string "Successfully overridden"). and calling it with symmetry ().), but nothing (other than using a different name) seemed to work.

I figured out that the clash comes from Ltac2.Notations.v where we have

Ltac2 Notation reflexivity := Std.reflexivity ().

Ltac2 symmetry0 cl :=
  Std.symmetry (default_on_concl cl).

Ltac2 Notation "symmetry" cl(opt(clause)) := symmetry0 cl.
Ltac2 Notation symmetry := symmetry.

So I’m wondering why this allows reflexivity to be overridden with a notation, but not symmetry. Is it because using Ltac2 Notation "string" := _ puts the string in the grammar (and it can’t be removed)? Is there way to print the current state of the Ltac2 grammar (similar to Print Grammar constr.) so I can check?

2

There are two types of notations in Ltac2, which by design do not rely on the same mechanism.

  • Actual notations, like Ltac2 Notation "symmetry" cl(opt(clause)) := ....
  • So called syntactic notations, like Ltac2 Notation symmetry := ....

The first one extends the Coq parser with a dedicated rule, which is expanded at parsing time, while the second one is just resolved as a special name (similarly to Gallina’s syntactic notations) whose body is expanded a typing time, i.e. after parsing.

The first kind is more powerful, but is much less modular. It’s easy to wreak havoc at a distance by merely introducing a parsing conflict without really realizing. The second kind is weaker, but as it doesn’t mess with the parser, you can use it safely without second thought.

Here, you’re typically encountering a parsing issue. The standard Ltac notations are using the parsing mechanism, so the syntactic notation doesn’t even have time to fire, it doesn’t parse at all.

2 Likes