Locally extending/overriding tactics

Stream: lean4

[Joachim Breitner]

TIL that you can locally extend a tactic, e.g. (here changing the tactic used by wf-recursion)

macro_rules | `(tactic|decreasing_tactic) => `(tactic|fail "foo") in
mutual
def foo (n : Nat) : Nat := foo (n - 1)
end
termination_by foo n => n

Is there a way to _override_ a tactic? I tried

macro "decreasing_tactic" : tactic => `(tactic| fail "foo") in
mutual
def foo (n : Nat) : Nat := foo (n - 1)
end
termination_by foo n => n

but that doesn't seem to work.

[Damiano Testa]

I think that the general structure is that if one fails, it tries the previously defined one, stopping as soon as it finds a working tactic, throwing the very first error otherwise. So, while what you observe is what I expect, I do not know how to do what you want!

[Joachim Breitner]

Right, that’s expected for extending with macro_rules, but sometimes you may want more control and prevent the backtracking.

[Mac Malone]

@Joachim Breitner Part of the problem is that macro doesn't work because it creates a new syntax and adds an expander for that. Another part of the problem is that tactics are evaluated differently from other syntax. In normal syntax, you can prevent other macros from being tried by throw a proper error via Macro.throwError rather than Macro.throwUnsupported. For example:

import Lean
open Lean

syntax (name := decreasingTerm) "decreasing_term" (&"foo" <|> &"bar") : term

macro_rules | `(term|decreasing_term foo) => `(term|by admit)
macro_rules | `(term|decreasing_term bar) => `(term|by fail "bar")
def bar1 : Nat := decreasing_term foo -- declaration uses sorry
def bar2 : Nat := decreasing_term bar -- bar

@[macro decreasingTerm]
def skippedDecreasingTerm : Macro
| _ => Macro.throwUnsupported -- signals Lean should try earlier expanders
def bar4 : Nat := decreasing_term foo -- declaration uses sorry

@[macro decreasingTerm]
def newDecreasingTerm : Macro
| _ => Macro.throwError "hard error" -- will prevent trying earlier expanders
def bar5 : Nat := decreasing_term foo -- hard error

Tactics; however, will keep looking for a successful run no matter what error is produced.