# Documentation

Init.WFTactics

Unfold definitions commonly used in well founded relation definitions. This is primarily intended for internal use in decreasing_tactic.

Equations

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

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.

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