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).

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.

Instances For

    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.

    Instances For

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

      Instances For