Fail if no progress

This implements the fail_if_no_progress tactic, which fails if no actual progress is made by the following tactic sequence.

"Actual progress" means that either the number of goals has changed, that the number or presence of expressions in the context has changed, or that the type of some expression in the context or the type of the goal is no longer definitionally equal to what it used to be at reducible transparency.

This means that, for example, 1 - 1 changing to 0 does not count as actual progress, since

example : (1 - 1 = 0) := by with_reducible rfl

This tactic is useful in situations where we want to stop iterating some tactics if they're not having any effect, e.g. repeat (fail_if_no_progress simp <;> ring_nf).

def Mathlib.Tactic.failIfNoProgress : Lean.ParserDescr

fail_if_no_progress tacs evaluates tacs, and fails if no progress is made on the main goal or the local context at reducible transparency.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.lctxIsDefEq (l₁ : List (Option Lean.LocalDecl)) (l₂ : List (Option Lean.LocalDecl)) : Lean.MetaM Bool

lctxIsDefEq l₁ l₂ compares two lists of Option LocalDecls (as returned from e.g. (← (← getMainGoal).getDecl).lctx.decls.toList). It returns true if they contain expressions of the same type in the same order (up to defeq), and false otherwise.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.lctxIsDefEq (none :: l₁) (none :: l₂) = Mathlib.Tactic.lctxIsDefEq l₁ l₂
• Mathlib.Tactic.lctxIsDefEq [] [] = pure true
• Mathlib.Tactic.lctxIsDefEq x✝ x = pure false

def Mathlib.Tactic.runAndFailIfNoProgress (goal : Lean.MVarId) (tacs : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM (List Lean.MVarId)

Run tacs : TacticM Unit on goal, and fail if no progress is made.

Equations

• One or more equations did not get rendered due to their size.