evaluating induction tactic within a tactic

Stream: metaprogramming / tactics

[Nels Martin]

I am trying to write a tactic that:

1. Loops through local declarations
2. If it finds a declaration h that has an inductive type (with respect to the Lean kernel, so structs included), print the result of calling induction h, and then backtracks.

I've used evalTactic for this before, but I can't get the argument to induction to compile correctly. Here's my best guess:

import Lean
open Lean Elab Tactic Meta

elab "so" : tactic => do
  let lctx ← getLCtx
  let env ← getEnv
  for ldecl in lctx do
    if ldecl.isImplementationDetail then
      continue
    let type ← instantiateMVars ldecl.type
    if let some name := type.getAppFn.constName? then
      if let some ci := env.find? name then
        if ci.isInductive then
          dbg_trace f!"Trying induction on {ldecl.userName} : {← ppExpr type}"
          let identStx : TSyntax `ident := Lean.mkIdent ldecl.userName
          let elimTargetStx : TSyntax `Lean.Parser.Tactic.elimTarget := ⟨identStx⟩
          withoutModifyingState do
            evalTactic (← `(tactic| induction $elimTargetStx))

variable (p q r s : Prop)


theorem test (h : p ∧ q) : p := by
  so
  sorry

But this throws the same error as replacing so in the test theorem with induction with no argument, so I suspect something is going wrong in evalTactic. I just want to see what the goal state would be if I had used induction h in test. Is there a quick fix, or do I just need to understand this whole thing better? If the latter is true, what would you recommend I look at?

Thanks!

[Robin Arnez]

Don't ever try to cast TSyntaxes to different types: It is very common for them to be incompatible because one contains more than the other. Instead, specify the type of the syntax:

let identStx : TSyntax `ident := Lean.mkIdent ldecl.userName
withoutModifyingState do
  evalTactic (← `(tactic| induction $identStx:ident))

[Robin Arnez]

Also, replace dbg_trace with Lean.logInfo:

Lean.logInfo m!"Trying induction on {ldecl.toExpr} : {type}"

(also gives you nice hover)

[Robin Arnez]

Also, most tactics have functions on Lean.MVarId to use instead of using evalTactic:

let subgoals ← (← getMainGoal).induction ldecl.fvarId (name ++ `rec)

[Nels Martin]

Very helpful! Thank you Robin.

[knowaywood]

(deleted)