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.

@[irreducible]

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 have the same local declarations in the same order (up to defeq, without setting mvars), and false otherwise.

Assumption: this function is run with one of the local contexts as the current MetaM local context, and one of the two lists consists of the LocalDecls of that context.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.lctxIsDefEq (none :: l₁) x = Mathlib.Tactic.lctxIsDefEq l₁ x
• Mathlib.Tactic.lctxIsDefEq x (none :: l₂) = Mathlib.Tactic.lctxIsDefEq x 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.