Referencing a specific hypothesis in evalTactic

Stream: new members

[Iva Dashevskii]

Hi everyone, I'm very new to Lean metaprogramming. In one of the toy tactics I'm trying to implement, I have a localDecl from the local context, and want to pass it as an argument to a tactic (e. g. cases). I tried a few things, but I ended up creating a new hypothesis and passing it to the tactic instead. Here's a minimal example:

elab "h_cases" : tactic => do
  withMainContext do
    let context ← getLCtx
    for h in context do
      let name ← h.fvarId.getUserName
      if !name = "h".toName then
        continue
      -- Both of these approaches create a new hypothesis named ``h and try to run the tactic on it,
      -- instead of running the tactic on h

      -- let hExpr := Expr.fvar h.fvarId
      -- let eTerm : TSyntax `Lean.Parser.Tactic.elimTarget := ⟨← PrettyPrinter.delab hExpr⟩
      -- evalTactic (← `(tactic| cases $eTerm))

      -- let eStx : Syntax := Syntax.ident SourceInfo.none userName.toString.toSubstring userName []
      -- evalTactic (← `(tactic| cases $(⟨eStx⟩)))

example (h : α ∨ b) : False := by
  -- If I uncomment one of the code blocks above, h_cases creates a new unnamed hypothesis and fails
  -- with the following error:
  -- Tactic `cases` failed: major premise type is not an inductive type
  -- ?m.4
  h_cases
  sorry

Does anyone know how to do this properly?

[Aaron Liu]

does it need to be an evalTactic?

[Aaron Liu]

if you have the fvarid then for cases for example you can just use docs#Lean.MVarId.cases it

[Aaron Liu]

there's also docs#Lean.Elab.Term.exprToSyntax if you really do need to embed it into syntax

[Aaron Liu]

your first attempt is actually quite close, cases was failing because you had malformed syntax

import Lean

open Lean Elab Tactic

elab "h_cases" : tactic => do
  withMainContext do
    let context ← getLCtx
    for h in context do
      let name ← h.fvarId.getUserName
      if !name = "h".toName then
        continue
      let hExpr := Expr.fvar h.fvarId
      let eTerm : TSyntax `Lean.Parser.Tactic.elimTarget ←
        `(Lean.Parser.Tactic.elimTarget| $(← PrettyPrinter.delab hExpr):term)
      evalTactic (← `(tactic| cases $eTerm))

example (h : α ∨ b) : False := by
  h_cases
  -- it works