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 < b → a < b + c

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

a < b → a < c + b

@[protected]

def psum.alt.sizeof {α : Type u} {β : Type v} [has_sizeof α] [has_sizeof β] :

psum α β → ℕ

Equations

psum.alt.sizeof (psum.inr b) = sizeof b
psum.alt.sizeof (psum.inl a) = sizeof a

@[protected, reducible]

def psum.has_sizeof_alt (α : Type u) (β : Type v) [has_sizeof α] [has_sizeof β] :

has_sizeof (psum α β)

Equations

psum.has_sizeof_alt α β = {sizeof := psum.alt.sizeof _inst_2}

def well_founded_tactics.id_tag.wf :

Equations

well_founded_tactics.id_tag.wf = unit.star()

meta def well_founded_tactics.mk_alt_sizeof :

meta def well_founded_tactics.default_rel_tac (e : expr) (eqns : list expr) :

meta def well_founded_tactics.clear_internals :

meta def well_founded_tactics.unfold_wf_rel :

meta def well_founded_tactics.is_psigma_mk :

expr → tactic (expr × expr)

meta def well_founded_tactics.process_lex :

tactic unit → 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 :

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