detect termination proof obligations in TacticM

Stream: metaprogramming / tactics

[llllvvuu]

Does TacticM contain any info about whether there are termination proof obligations?

Suppose I want to ban tactics that create termination proof obligations. This would be possible if I can query this info before and after.

[Robin Arnez]

No, not directly. But you can detect whether the proof that a tactic produced refers to the current declaration recursively:

import Lean.Elab.Tactic

open Lean Meta Elab Tactic

elab "ban_termination" t:tactic : tactic => do
  let goals ← getUnsolvedGoals
  evalTactic t
  for goal in goals do
    let some expr ← getExprMVarAssignment? goal | continue
    let expr ← instantiateMVars expr
    goal.withContext do
      let recFVars : FVarIdSet := (← getLCtx).foldl
        (fun set decl => if decl.isAuxDecl then set.insert decl.fvarId else set) ∅
      if expr.hasAnyFVar recFVars.contains then
        Meta.throwTacticEx `ban_termination goal "tactic used recursion"

theorem testing : 3 = 3 := by
  ban_termination exact testing -- error: tactic 'ban_termination' failed, tactic used recursion