mathlib documentation

core / init.wf

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

A value x : α is accessible from r when every value that's lesser under r is also accessible. Note that any value that's minimal under r is vacuously accessible.

Equivalently, acc r x when there is no infinite chain of elements starting at x that are related under r.

This is used to state the definition of well-foundedness (see well_founded).

theorem acc.inv {α : Sort u} {r : α → α → Prop} {x y : α} (h₁ : acc r x) (h₂ : r y x) :
acc r y
structure well_founded {α : Sort u} (r : α → α → 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. Equivalently, acc r x for all x.

Once you know that a relation is well_founded, you can use it to define fixpoint functions on α.

def well_founded.recursion {α : Sort u} {r : α → α → Prop} (hwf : well_founded r) {C : α → Sort v} (a : α) (h : Π (x : α), (Π (y : α), r y xC y)C x) :
C a
Equations
  • hwf.recursion a h = _.rec_on (λ (x₁ : α) (ac₁ : ∀ (y : α), r y x₁acc r y) (ih : Π (y : α), r y x₁C y), h x₁ ih)
theorem well_founded.induction {α : Sort u} {r : α → α → Prop} (hwf : well_founded r) {C : α → Prop} (a : α) (h : ∀ (x : α), (∀ (y : α), r y xC y)C x) :
C a
def well_founded.fix_F {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : Π (x : α), (Π (y : α), r y xC y)C x) (x : α) (a : 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)
theorem well_founded.fix_F_eq {α : Sort u} {r : α → α → Prop} {C : α → Sort v} (F : Π (x : α), (Π (y : α), r y xC 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 _)
def well_founded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : well_founded r) (F : Π (x : α), (Π (y : α), r y xC y)C x) (x : α) :
C x

Well-founded fixpoint

Equations
theorem well_founded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : well_founded r) (F : Π (x : α), (Π (y : α), r y xC 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

theorem empty_wf {α : Sort u} :

Empty relation is well-founded

theorem subrelation.accessible {α : Sort u} {r Q : α → α → Prop} (h₁ : subrelation Q r) {a : α} (ac : acc r a) :
acc Q a
theorem subrelation.wf {α : Sort u} {r Q : α → α → Prop} (h₁ : subrelation Q r) (h₂ : well_founded r) :
theorem inv_image.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) {a : α} (ac : acc r (f a)) :
acc (inv_image r f) a
theorem inv_image.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) (h : well_founded r) :

less-than is well-founded

def measure {α : Sort u} :
(α → )α → α → Prop
Equations
Instances for measure
theorem measure_wf {α : Sort u} (f : α → ) :
def sizeof_measure (α : Sort u) [has_sizeof α] :
α → α → Prop
Equations
theorem sizeof_measure_wf (α : Sort u) [has_sizeof α] :
@[protected, instance]
Equations
inductive prod.lex {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → 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₂)
Instances for prod.lex
inductive prod.rprod {α : Type u} {β : Type v} (ra : α → α → Prop) (rb : β → β → 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₂)
theorem 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)
theorem prod.lex_wf {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (ha : well_founded ra) (hb : well_founded rb) :
theorem prod.rprod_sub_lex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a b : α × β) :
prod.rprod ra rb a bprod.lex ra rb a b
theorem prod.rprod_wf {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (ha : well_founded ra) (hb : well_founded rb) :
@[protected, instance]
def prod.has_well_founded {α : Type u} {β : Type v} [s₁ : has_well_founded α] [s₂ : has_well_founded β] :
Equations