Invoking tactics from another tactic

Stream: new members

[Isak Colboubrani]

I am writing a tactic that will selectively apply certain existing tactics based on conditions.

Is the following the recommended syntax for invoking a tactic (in this case linarith)?

Lean.Elab.Tactic.evalTactic <|← `(tactic|linarith)

How do I make the tactic name dynamic? In other words, how do I execute tacticToExecute given let tacticToExecute := "some tactic"?

[Alex J. Best]

I'm not sure this is really a recommended way to go about it, probably you only have a fixed list of options, I'd go with something more like this

import Lean
open Lean Meta   Elab Tactic
def a (n : Nat) : MetaM <| TSyntax `tactic := do match n with
| 0 => return ← `(tactic|assumption)
| 1 => return ← `(tactic|simp)
| _ => unreachable!

elab "asd" : tactic => do
  let as := 1
  Lean.Elab.Tactic.evalTactic <| ← a as

example : 1 = 1 := by
  asd

[Alex J. Best]

If you had made a #mwe with an example of your setup it would have been much quicker for me to write this answer btw

[Alex J. Best]

You could also use a string or whatever in place of a nat index here, but fundamentally when using these tactic syntax quotations Lean wants to check that the syntax you are producing corresponds to valid tactic calls, so full dynamism seems ill-advised

[Isak Colboubrani]

@Alex J. Best Thanks Alex! I've resolved the issue by employing both runParserCategory and evalTactic together:

          match Lean.Parser.runParserCategory (← Lean.MonadEnv.getEnv) `tactic tacticToRun with
          | Except.error e => throwError e
          | Except.ok stx => Lean.Elab.Tactic.evalTactic $ ← `(tactic| $(⟨stx⟩))

Does this appear to be correct?

[Kyle Miller]

Lean.Elab.Tactic.evalTactic $ ← `(tactic| $(⟨stx⟩)) can be simply Lean.Elab.Tactic.evalTactic stx.

Could we #xy this? There's almost always a better thing to do than parsing strings. For example, your tactic might have a tactic argument. There are many tactics that take a discharger argument, where you can write something like my_tactic (discharger := linarith), and linarith can be replaced with an arbitrarily complicated tactic script.

[Isak Colboubrani]

@Kyle Miller Thank you! Using Lean.Elab.Tactic.evalTactic stx is indeed much cleaner.

In my logic, I have arrays of strings containing tactics that I wish to execute if certain criteria are met, hence the need to convert strings into tactics (using evalTactic <Lean.Syntax> after getting the Lean.Syntax object via Lean.Parser.runParserCategory). Please let me know if there's a more appropriate method to accomplish this without parsing strings.

I'm required to supply Lean.Syntax objects to Lean.Elab.Tactic.evalTactic. I'm contemplating whether storing Lean syntax objects directly in the array, as opposed to strings, might be a better strategy. Would this approach be advisable? Furthermore, is there an alternative method that enables "compile-time" verification of tactic availability?

[Patrick Massot]

You should definitely try to handle Syntax objects as much as possible.

[Kyle Miller]

Could we #xy more? I'd like to understand what sort of tactic you're writing, and why it's natural for you to have arrays of tactic strings/syntax rather than some other arrangement.

(Is it an array because you want to execute sequences of tactics? A tactic can be a composite of tactics, so there's no need for an array.)

[Kyle Miller]

How dynamic do you need this to be? Is there anything wrong with an if/else chain that does an appropriate Lean.Elab.Tactic.evalTactic <|← `(tactic|linarith) in each case?

[Isak Colboubrani]

@Kyle Miller Here is a #mwe showing what I'm currently doing:

syntax (name := mytactic) "mytactic" : tactic
@[tactic mytactic] def _mytactic : Lean.Elab.Tactic.Tactic := fun _ =>
  let tactics_1 : Array String := #[
    "some tactic 1",
    "some tactic 2",
    "some tactic 3",
    "aesop"
  ]
  -- let tactics_2 : ...
  -- let tactics_3 : ...
  Lean.Elab.Tactic.withMainContext do
    -- some logic determining which of tactics_1, tactics_2, etc should be run
    tactics_1.forM (λ tactic => do
      -- some logic 1
      match Lean.Parser.runParserCategory (← Lean.MonadEnv.getEnv) `tactic tactic with
        | Except.error e => Lean.logInfo m!"Error '{tactic}': {e}"
        | Except.ok s => Lean.Elab.Tactic.evalTactic s
      -- some logic 2
    )
    -- some logic 3

example (h : ∀ n, n = 0) : ∀ n, n ^ n = 0 := by mytactic

If I'm understanding your suggestion correctly it would require me to violate the "Don't repeat yourself" (DRY) principle by repeating the "some logic" blocks in my code, no?

[Eric Wieser]

I think the suggestion is for your array to contain `(tactic| some tactic 1) etc instead

[Kyle Miller]

What's the "some logic 1" and "some logic 2"? Could you give a #mwe that represents the functionality of the tactic that you're working on?

[Isak Colboubrani]

@Kyle Miller It is code analysing and reporting what progress each "subtactic" achieved. Here is an #mwe:

syntax (name := mytactic) "mytactic" : tactic
@[tactic mytactic] def _mytactic : Lean.Elab.Tactic.Tactic := fun _ =>
  let tactics_1 : Array String := #[
    "some tactic 1",
    "some tactic 2",
    "some tactic 3",
    "aesop"
  ]
  -- let tactics_2 : ...
  -- let tactics_3 : ...
  Lean.Elab.Tactic.withMainContext do
    -- some logic determining which of tactics_1, tactics_2, etc should be run
    -- depending on the current state ...
    tactics_1.forM (λ tactic => do
      -- code analyzing the state after before running the subtactic such as ...
      let unsolved ← Lean.Elab.Tactic.getUnsolvedGoals
      Lean.logInfo m!"{unsolved.length} unsolved goal(s) before running subtactic {tactic}"
      match Lean.Parser.runParserCategory (← Lean.MonadEnv.getEnv) `tactic tactic with
        | Except.error e => Lean.logInfo m!"Error '{tactic}': {e}"
        | Except.ok s => Lean.Elab.Tactic.evalTactic s
      -- code analyzing the state after after running the subtactic such as ...
      let unsolved ← Lean.Elab.Tactic.getUnsolvedGoals
      Lean.logInfo m!"{unsolved.length} unsolved goal(s) after running subtactic {tactic}"
    )
    -- code analyzing the state after running all subtactics
    let unsolved ← Lean.Elab.Tactic.getUnsolvedGoals
    Lean.logInfo m!"{unsolved.length} unsolved goal(s) after running tactics"

example (h : ∀ n, n = 0) : ∀ n, n ^ n = 0 := by mytactic

[Mario Carneiro]

@Isak Colboubrani (an important aspect of #mwe's is that they have the correct imports and opens)

[Kyle Miller]

Here's an example of how you can organize this:

open Lean Elab Tactic

def evalTacticWithReport (tactic : TSyntax `tactic) : TacticM Unit := do
  let unsolved ← Lean.Elab.Tactic.getUnsolvedGoals
  Lean.logInfo m!"{unsolved.length} unsolved goal(s) before running subtactic {tactic}"
  evalTactic tactic
  let unsolved ← Lean.Elab.Tactic.getUnsolvedGoals
  Lean.logInfo m!"{unsolved.length} unsolved goal(s) after running subtactic {tactic}"

syntax (name := mytactic) "mytactic" : tactic
@[tactic mytactic] def _mytactic : Lean.Elab.Tactic.Tactic := fun _ =>
  Lean.Elab.Tactic.withMainContext do
    let shouldDoTactics1 := true -- some logic
    if shouldDoTactics1 then
      evalTacticWithReport <| ← `(tactic| simp)
      evalTacticWithReport <| ← `(tactic| linarith)
      evalTacticWithReport <| ← `(tactic| aesop)
    else
      evalTacticWithReport <| ← `(tactic| congr)
    -- code analyzing the state after running all subtactics
    let unsolved ← Lean.Elab.Tactic.getUnsolvedGoals
    Lean.logInfo m!"{unsolved.length} unsolved goal(s) after running tactics"

[Kyle Miller]

Note that withMainContext is only valid for the state right at the beginning. If you need to do some logic after running after tactics, you have to adjust the context.