mathlib3 documentation

core / init.wf

inductive acc {α : Sort u} (r : α α Prop) :
α Prop

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 x C 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 x C y) C x) :
C a
def well_founded.fix_F {α : Sort u} {r : α α Prop} {C : α Sort v} (F : Π (x : α), (Π (y : α), r y x C y) C x) (x : α) (a : acc r x) :
C x
Equations
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 _)
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
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

Empty relation is well-founded

Subrelation of a well-founded 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
@[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 b prod.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