mathlib documentation

core.init.meta.well_founded_tactics

theorem nat.lt_add_of_zero_lt_left (a b : ℕ) (h : 0 < b) :

a < a + b

theorem nat.zero_lt_one_add (a : ℕ) :

0 < 1 + a

theorem nat.lt_add_right (a b c : ℕ) (a_1 : a < b) :

a < b + c

theorem nat.lt_add_left (a b c : ℕ) (a_1 : a < b) :

a < c + b

meta def well_founded_tactics.clear_internals :

meta def well_founded_tactics.unfold_wf_rel :

meta def well_founded_tactics.is_psigma_mk (a : expr) :

tactic (expr × expr)

meta def well_founded_tactics.process_lex (a : tactic unit) :

meta def well_founded_tactics.unfold_sizeof :

meta def well_founded_tactics.cancel_nat_add_lt :

meta def well_founded_tactics.check_target_is_value_lt :

meta def well_founded_tactics.trivial_nat_lt :

meta def well_founded_tactics.default_dec_tac :

meta structure well_founded_tactics :

Type

rel_tac : expr → list expr → tactic unit
dec_tac : tactic unit

Argument for using_well_founded

The tactic rel_tac has to synthesize an element of type (has_well_founded A). The two arguments are: a local representing the function being defined by well founded recursion, and a list of recursive equations. The equations can be used to decide which well founded relation should be used.

The tactic dec_tac has to synthesize decreasing proofs.

meta def well_founded_tactics.default :

well_founded_tactics