Tactics using elaborators🔗

Contributors: ajay-k-nair, Anirudh Gupta

Let's start by writing a basic elaborator that retrieves and displays the expression representing the type of the main goal.

elab "goalExpr" : tactic => do
  let goalExpr ← getMainTarget
  logInfo m!"Main Target Expression: {goalExpr}"

example: 2 + 3 = 5 := by⊢ 2 + 3 = 5
  Main Target Expression: 2 + 3 = 5goalExpr⊢ 2 + 3 = 5
  simpAll goals completed! 🐙

If you formalize mathematics in Lean, you are likely familiar with the sorry tactic. We use it frequently as a placeholder for proofs yet to be written. The sorry tactic artificially closes the current main goal but leaves a warning in the Infoview.

declaration uses `sorry`example : 847 + 153 = 1000 := by⊢ 847 + 153 = 1000 sorryAll goals completed! 🐙

Under the hood, the sorry tactic works by creating a term of the main goal's type using the sorryAx axiom. You can inspect these internal components directly:

sorryAx.{u} (α : Sort u) (synthetic : Bool) : α#check sorryAx
-- sorryAx.{u} (α : Sort u) (synthetic :  Bool) : α

Now, let's write a custom tactic called toDo using elab and sorryAx. The toDo tactic will close the main goal just like sorry, but it will also accept a string argument to log a custom reminder to the Infoview.

elab "toDo" s: str : tactic => do
  withMainContext do
  logInfo m!"Message:{s}"
  let targetExpr ← getMainTarget
  let sorryExpr ←
      mkAppM ``sorryAx #[targetExpr, mkConst ``false]
  closeMainGoal `todo sorryExpr

declaration uses `sorry`example : 34 ≤ 47 := by⊢ 34 ≤ 47
  Message:"This should be easy to do"toDo "This should be easy to do"All goals completed! 🐙

Let's break down the specific metaprogramming functions used to make this work:

getMainTarget retrieves the expression for the type of the current main goal.
mkAppM is a highly useful function that constructs a function application expression. It takes the Name of the function, in this case sorryAx, and an array of expressions representing the arguments you want to pass to it.