mathlib3 documentation

core / init.wf

source
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).

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

source
@[class]
structure has_well_founded (α : Sort u) :
Type u
Instances of this typeclass
Instances of other typeclasses for has_well_founded
  • has_well_founded.has_sizeof_inst
source
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)
source
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
source
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
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
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
theorem empty_wf {α : Sort u} :
well_founded empty_relation

Empty relation is well-founded

Subrelation of a well-founded relation is well-founded

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

less-than is well-founded

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