mathlib docs: core.init.wf

source

inductive acc {α : Sort u} :

(α → α → Prop) → α → Prop

intro : ∀ {α : Sort u} (r : α → α → Prop) (x : α), (∀ (y : α), r y x → acc r y) → acc r x

source

def acc.inv {α : Sort u} {r : α → α → Prop} {x y : α} :

acc r x → r y x → acc r y

Equations

_ = _

source

structure well_founded {α : Sort u} :

(α → α → Prop) → Prop

apply : ∀ (a : α), acc r a

A relation r : α → α → Prop is well-founded when ∀ x, (∀ y, r y x → P y → P x) → P x for all predicates P. Once you know that a relation is well_founded, you can use it to define fixpoint functions on α.

source

@[class]

structure has_well_founded :

Sort u → Type u

r : α → α → Prop
wf : well_founded has_well_founded.r

Instances

source

theorem well_founded.recursion {α : Sort u} {r : α → α → Prop} (hwf : well_founded r) {C : α → Sort v} (a : α) :

(Π (x : α), (Π (y : α), r y x → C y) → C x) → C a

source

theorem well_founded.induction {α : Sort u} {r : α → α → Prop} (hwf : well_founded r) {C : α → Prop} (a : α) :

(∀ (x : α), (∀ (y : α), r y x → C y) → C x) → C a

source

def well_founded.fix_F {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : Π (x : α), (Π (y : α), r y x → C y) → C x) (x : α) :

acc r x → C x

Equations

well_founded.fix_F F x a = a.rec_on (λ (x₁ : α) (ac₁ : ∀ (y : α), r y x₁ → acc r y) (ih : Π (y : α), r y x₁ → C y), F x₁ ih)

source

theorem well_founded.fix_F_eq {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : Π (x : α), (Π (y : α), r y x → C y) → C x) (x : α) (acx : acc r x) :

well_founded.fix_F F x acx = F x (λ (y : α) (p : r y x), well_founded.fix_F F y _)

source

def well_founded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : well_founded r) (F : Π (x : α), (Π (y : α), r y x → C y) → C x) (x : α) :

C x

Well-founded fixpoint

Equations

hwf.fix F x = well_founded.fix_F F x _

source

theorem well_founded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : well_founded r) (F : Π (x : α), (Π (y : α), r y x → C y) → C x) (x : α) :

hwf.fix F x = F x (λ (y : α) (h : r y x), hwf.fix F y)

Well-founded fixpoint satisfies fixpoint equation

source

def empty_wf {α : Sort u} :

well_founded empty_relation

Empty relation is well-founded

Equations

empty_wf = _

source

def subrelation.accessible {α : Sort u} {r Q : α → α → Prop} (h₁ : subrelation Q r) {a : α} :

acc r a → acc Q a

Equations

_ = _

source

def subrelation.wf {α : Sort u} {r Q : α → α → Prop} :

subrelation Q r → well_founded r → well_founded Q

Equations

_ = _

source

def inv_image.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) {a : α} :

acc r (f a) → acc (inv_image r f) a

Equations

_ = _

source

def inv_image.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) :

well_founded r → well_founded (inv_image r f)

Equations

_ = _

source

def tc.accessible {α : Sort u} {r : α → α → Prop} {z : α} :

acc r z → acc (tc r) z

Equations

_ = _

source

def tc.wf {α : Sort u} {r : α → α → Prop} :

well_founded r → well_founded (tc r)

Equations

_ = _

source

def nat.lt_wf :

well_founded nat.lt

less-than is well-founded

Equations

nat.lt_wf = _

source

def measure {α : Sort u} :

(α → ℕ) → α → α → Prop

Equations

measure = inv_image has_lt.lt

source

def measure_wf {α : Sort u} (f : α → ℕ) :

well_founded (measure f)

Equations

_ = _

source

def sizeof_measure (α : Sort u) [has_sizeof α] :

α → α → Prop

Equations

sizeof_measure α = measure sizeof

source

def sizeof_measure_wf (α : Sort u) [has_sizeof α] :

well_founded (sizeof_measure α)

Equations

_ = _

source

@[instance]

def has_well_founded_of_has_sizeof (α : Sort u) [has_sizeof α] :

has_well_founded α

Equations

has_well_founded_of_has_sizeof α = {r := sizeof_measure α _inst_1, wf := _}

source

inductive prod.lex {α : Type u} {β : Type v} :

(α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop

left : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {a₁ : α} (b₁ : β) {a₂ : α} (b₂ : β), ra a₁ a₂ → prod.lex ra rb (a₁, b₁) (a₂, b₂)
right : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) (a : α) {b₁ b₂ : β}, rb b₁ b₂ → prod.lex ra rb (a, b₁) (a, b₂)

source

inductive prod.rprod {α : Type u} {β : Type v} :

(α → α → Prop) → (β → β → Prop) → α × β → α × β → Prop

intro : ∀ {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → Prop) {a₁ : α} {b₁ : β} {a₂ : α} {b₂ : β}, ra a₁ a₂ → rb b₁ b₂ → prod.rprod ra rb (a₁, b₁) (a₂, b₂)

source

def prod.lex_accessible {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} {a : α} (aca : acc ra a) (acb : ∀ (b : β), acc rb b) (b : β) :

acc (prod.lex ra rb) (a, b)

Equations