macro_rules with an argument

Stream: mathlib4

[Heather Macbeth]

I'm trying to write a tactic rel which calls several other tactics in turn, like the code in Lean core which makes trivial call assumption, rfl etc:

macro_rules | `(tactic| trivial) => `(tactic| assumption)
macro_rules | `(tactic| trivial) => `(tactic| rfl)
macro_rules | `(tactic| trivial) => `(tactic| contradiction)
macro_rules | `(tactic| trivial) => `(tactic| decide)
macro_rules | `(tactic| trivial) => `(tactic| apply True.intro)
macro_rules | `(tactic| trivial) => `(tactic| apply And.intro <;> trivial)

In my case all the tactics I want to combine take a single list of arguments [h1, h2, h3]. How do I adapt macro_rules to pass these to my super-tactic rel? I tried copying blindly and hoping the arguments would be passed automatically, but the tactic fails on the arguments with

unexpected syntax
  rel [ha]

[David Renshaw]

what does your syntax declaration look like?

[Heather Macbeth]

syntax (name := RelSyntax) "rel" (args)? : tactic

[Heather Macbeth]

Sorry, that's hiding something in a namespace. One sec, I'll make a mwe.

[Heather Macbeth]

syntax (name := RelSyntax) "rel" (" [" term,* "] ")? : tactic

macro_rules | `(tactic| rel) => `(tactic| simp)

-- works
example (x : Nat) (hx : x = 3) : x ^ 2 = 9 := by simp [hx]

/-
unexpected syntax
  rel [hx]
-/
example (x : Nat) (hx : x = 3) : x ^ 2 = 9 := by rel [hx]

[Thomas Murrills]

I think the problem here might be that you’ve given a rule for rel appearing by itself, but not for rel appearing with arguments—and when there are arguments, the whole thing is parsed as a tactic syntax node (and rel appearing by itself isn’t a tactic node in that case)

[Thomas Murrills]

(Haven’t tested, though!)

[Heather Macbeth]

That seems plausible! How do I give a rule for rel appearing with arguments?

[Thomas Murrills]

Hmm, the way you’ve got it set up, does something like

macro_rules | `(tactic|rel $[ [$x:term,*] ]?) => `(tactic|simp $[ [$x,*] ]?)

work? (untested, on mobile)

[Thomas Murrills]

(If I’ve messed up the syntax, the section of the metaprogramming book on antiquotations might be helpful!)

[Heather Macbeth]

Thanks, this should get me started anyway. I'll have a look at the book! Your current version fails with

application type mismatch
  x.elemsAndSeps
argument
  x
has type
  Lean.Syntax.TSepArray `term "," : Type
but is expected to have type
  Lean.Syntax.TSepArray `Lean.Parser.Tactic.simpStar "," : Type

[Thomas Murrills]

ah, ok—I think this is a sign that simp doesn’t like the fact that it’s being passed terms! Try using simpStar instead of term in the definition of rel syntax, maybe?

[Thomas Murrills]

Or, maybe we can just leave off the syntax category annotation: $x,* instead of $x:term,* in the macro rules

[Heather Macbeth]

In my case the simp is a bit of a red herring, because as you note it seems to use its own special syntax for arguments, whereas I am using custom tactics which use the same syntax $[ [$x:term,*] ]?. So that problem isnt actually occurring for me.

[Heather Macbeth]

I seem to have the arguments working, but am encountering another issue, where when I try to make multiple macro_rules for rel, it tries only one of them, not all of them. I'll see if I can make a MWE for that.

[Thomas Murrills]

Hmm, how do the syntax matches distinguish themselves from each other in each rule? (If you want to post a not-quite-minimized example in this case that’s fine too!)

[Heather Macbeth]

OK, here's a reasonably complete but not minimal example:

import Mathlib.Data.Int.ModEq
import Mathlib.Tactic.SolveByElim
import OtherFile

open Lean Meta Elab Mathlib Tactic

def RelConfig : SolveByElim.Config :=
{ discharge := fun _ => pure none
  failAtMaxDepth := false
  maxDepth := 50 }

syntax (name := ineqRelSyntax) "ineq_rel" " [" term,* "] " : tactic
syntax (name := modRelSyntax) "mod_rel" " [" term,* "] " : tactic
syntax (name := RelSyntax) "rel" " [" term,* "] " : tactic

elab_rules : tactic | `(tactic| ineq_rel [$t,*]) => do
  liftMetaTactic <|
    fun g => SolveByElim.solveByElim.processSyntax
      RelConfig true false t.getElems.toList [] #[mkIdent `ineq_rules] [g]

elab_rules : tactic | `(tactic| mod_rel [$t,*]) => do
  liftMetaTactic <|
    fun g => SolveByElim.solveByElim.processSyntax
      RelConfig true false t.getElems.toList [] #[mkIdent `mod_rules] [g]

macro_rules | `(tactic| rel [$t,*]) => `(tactic| ineq_rel [$t,*])
macro_rules | `(tactic| rel [$t,*]) => `(tactic| mod_rel [$t,*])

attribute [ineq_rules] le_refl
attribute [mod_rules] Int.ModEq.refl

-- works
example (a : ℤ) : a ≡ a [ZMOD 3] := by rel []

-- fails
-- works if the `mod_rel` branch of the `rel` `macro_rules` is removed
example (a : ℤ) : a ≤ a := by rel []

[Heather Macbeth]

The OtherFile needs to declare the two attributes,

import Mathlib.Tactic.TagAttr

register_tag_attr ineq_rules
register_tag_attr mod_rules

[Heather Macbeth]

Thomas Murrills said:

Hmm, how do the syntax matches distinguish themselves from each other in each rule?

From what Thomas says, maybe there's a subtlety I missed here: you need to tell macro_rules which option to choose? I didn't know you had to do that (and am not sure how to).

[Thomas Murrills]

So, macro_rules is turning syntax into syntax, and macros in general only backtrack if you use Macro.throwUnsupported (I think), which tells the macro to try a different match. Tactic failure won’t cause backtracking in syntax processing, so after modifying the rel syntax you’ll just be stuck with e.g. an ineq_rel tactic as syntax, which then fails. (depending on whether Lean prioritizes rules that are defined first or last, I’m not sure.)

Is it true that your goal is to backtrack on tactic failure? If so, then I don’t think having different macro rules is the way to go (and thus we wouldn’t need Macro.throwUnsupported). Depending on how complete this example is, a simple solution might be to instead do something like using the first tactic in the resulting syntax: something like

macro_rules | `(tactic| rel [$t,*]) => `(tactic| first | ineq_rel [$t,*] | mod_rel [$t,*])

[Thomas Murrills]

(I think this is true, anyway. I haven’t tested so I could be wrong!)

[Heather Macbeth]

I think my point of confusion is, why does this work for trivial? In the code I quoted at the top of the thread
https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/macro_rules.20with.20an.20argument/near/324330390
it really seems like trivial is being set up with a series of macro_rules to try one tactic after another.

[Thomas Murrills]

Oh, I think I’m entirely wrong then, sorry!

[Thomas Murrills]

Hmm. I wasn’t aware you could do that (and apparently missed the first message in this thread, whoops). Interesting…

[Thomas Murrills]

My guess right now is that since mod_rel doesn't actually fail—it just leaves unsolved goals—the tactic never backtracks.

[Thomas Murrills]

If you want ineq_rel and mod_rel to not return subgoals (and only try to close the goal) you can change the definitions to the following (we check that the result of processSyntax matches an empty list, else we throw an error; then we return that empty list)

elab_rules : tactic | `(tactic| ineq_rel [$t,*]) => do
  liftMetaTactic <|
    fun g => do
    let [] ← SolveByElim.solveByElim.processSyntax
      RelConfig true false t.getElems.toList [] #[mkIdent `ineq_rules] [g]
      | throwError "failed to close the goal"
    return []

elab_rules : tactic | `(tactic| mod_rel [$t,*]) => do
  liftMetaTactic <|
    fun g => do
    let [] ← SolveByElim.solveByElim.processSyntax
      RelConfig true false t.getElems.toList [] #[mkIdent `mod_rules] [g]
      | throwError "failed to close the goal"
    return []

[Thomas Murrills]

And this works! If we add a trace to our macro rules, we can see that we try both tactics in the second example (and it closes the goal):

macro_rules | `(tactic| rel [$t,*]) => `(tactic| dbg_trace "hi ineq"; ineq_rel [$t,*])
macro_rules | `(tactic| rel [$t,*]) => `(tactic| dbg_trace "hi mod"; mod_rel [$t,*])

attribute [ineq_rules] le_refl
attribute [mod_rules] Int.ModEq.refl

example (a : ℤ) : a ≡ a [ZMOD 3] := by rel [] -- hi mod

example (a : ℤ) : a ≤ a := by rel [] -- hi mod hi ineq

[Thomas Murrills]

(So, even the first | ... suggestion earlier wouldn't have worked here, because mod_rel/ineq_rel was "succeeding" even when leaving subgoals, and thus first wouldn't have backtracked either)

[Heather Macbeth]

Awesome! That makes sense, I'll try it out. Thank you!