def tacticSimp_wf : Lean.ParserDescr

Unfold definitions commonly used in well founded relation definitions.

Since Lean 4.12, Lean unfolds these definitions automatically before presenting the goal to the user, and this tactic should no longer be necessary. Calls to simp_wf can be removed or replaced by plain calls to simp.

Equations

• tacticSimp_wf = Lean.ParserDescr.node `tacticSimp_wf 1024 (Lean.ParserDescr.nonReservedSymbol "simp_wf" false)

def tacticClean_wf : Lean.ParserDescr

This tactic is used internally by lean before presenting the proof obligations from a well-founded definition to the user via decreasing_by. It is not necessary to use this tactic manuall.

Equations

• tacticClean_wf = Lean.ParserDescr.node `tacticClean_wf 1024 (Lean.ParserDescr.nonReservedSymbol "clean_wf" false)

def tacticDecreasing_trivial : Lean.ParserDescr

Extensible helper tactic for decreasing_tactic. This handles the "base case" reasoning after applying lexicographic order lemmas. It can be extended by adding more macro definitions, e.g.

macro_rules | `(tactic| decreasing_trivial) => `(tactic| linarith)

Equations

• tacticDecreasing_trivial = Lean.ParserDescr.node `tacticDecreasing_trivial 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_trivial" false)

def tacticDecreasing_trivial_pre_omega : Lean.ParserDescr

Variant of decreasing_trivial that does not use omega, intended to be used in core modules before omega is available.

Equations

• tacticDecreasing_trivial_pre_omega = Lean.ParserDescr.node `tacticDecreasing_trivial_pre_omega 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_trivial_pre_omega" false)

def tacticDecreasing_with_ : Lean.ParserDescr

Constructs a proof of decreasing along a well founded relation, by simplifying, then applying lexicographic order lemmas and finally using ts to solve the base case. If it fails, it prints a message to help the user diagnose an ill-founded recursive definition.

Equations

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

def tacticDecreasing_tactic : Lean.ParserDescr

decreasing_tactic is called by default on well-founded recursions in order to synthesize a proof that recursive calls decrease along the selected well founded relation. It can be locally overridden by using decreasing_by tac on the recursive definition, and it can also be globally extended by adding more definitions for decreasing_tactic (or decreasing_trivial, which this tactic calls).

Equations

• tacticDecreasing_tactic = Lean.ParserDescr.node `tacticDecreasing_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "decreasing_tactic" false)