Unfold definitions commonly used in well founded relation definitions.
This is primarily intended for internal use in decreasing_tactic.
Equations
- tacticSimp_wf = Lean.ParserDescr.node `tacticSimp_wf 1024 (Lean.ParserDescr.nonReservedSymbol "simp_wf" false)
Instances For
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)
Instances For
Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and 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.
Instances For
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)