calling induction from a custom tactic

Stream: new members

[Nada Amin]

I’m trying to define a custom tactic that uses induction. I tried defining it both via elab and via a tactic macro (def with @[tactic ...]), and in both cases I run into the same error when a user applies the tactic:

tactic 'induction' failed, major premise type is not an inductive type
  ?m.6467

Explanation: the 'induction' tactic is for constructor-based reasoning as well as for applying custom induction principles with a 'using' clause or a registered '@[induction_eliminator]' theorem. The above type neither is an inductive type nor has a registered theorem.

Even though I can elaborate the term using elabTerm and confirm that it has the correct type (e.g., Expr), calling induction on it still fails.

Is there a correct way to pass a user-provided term into induction from a tactic definition?

I am on the latest pre-release version of Lean (leanprover/lean4:v4.20.0-rc5).

Thanks!

[Nada Amin]

This got me unstuck:

syntax (name := my_induction) "my_induction" term : tactic

@[tactic my_induction]
def evalMyInduction : Tactic := fun stx => do
  match stx with
  | `(tactic| my_induction $t:term) =>
    evalTactic (← `(tactic| induction $t:term))
  | _ => throwUnsupportedSyntax

[Aaron Liu]

Can you provide a #mwe?

[Nada Amin]

Thanks, I think I got it. The snippet above was the right starting point, but I had many false starts where the argument to induction was not recognized as a term.

I have an example of auto_induction in this repo: https://github.com/namin/LeanSketcher

There might be easier ways to go about this?