Documentation

Init.WF

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

Acc is the accessibility predicate. Given some relation r (e.g. <) and a value x, Acc r x means that x is accessible through r:

x is accessible if there exists no infinite sequence ... < y₂ < y₁ < y₀ < x.

  • intro: ∀ {α : Sort u} {r : ααProp} (x : α), (∀ (y : α), r y xAcc r y)Acc r x

    A value is accessible if for all y such that r y x, y is also accessible. Note that if there exists no y such that r y x, then x is accessible. Such an x is called a base case.

@[reducible, inline]
noncomputable abbrev Acc.ndrec {α : Sort u2} {r : ααProp} {C : αSort u1} (m : (x : α) → (∀ (y : α), r y xAcc r y)((y : α) → r y xC y)C x) {a : α} (n : Acc r a) :
C a
Equations
@[reducible, inline]
noncomputable abbrev Acc.ndrecOn {α : Sort u2} {r : ααProp} {C : αSort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y xAcc r y)((y : α) → r y xC y)C x) :
C a
Equations
theorem Acc.inv {α : Sort u} {r : ααProp} {x y : α} (h₁ : Acc r x) (h₂ : r y x) :
Acc r y
inductive WellFounded {α : Sort u} (r : ααProp) :

A relation r is WellFounded if all elements of α are accessible within r. If a relation is WellFounded, it does not allow for an infinite descent along the relation.

If the arguments of the recursive calls in a function definition decrease according to a well founded relation, then the function terminates. Well-founded relations are sometimes called Artinian or said to satisfy the “descending chain condition”.

theorem WellFounded.apply {α : Sort u} {r : ααProp} (wf : WellFounded r) (a : α) :
Acc r a
noncomputable def WellFounded.recursion {α : Sort u} {r : ααProp} (hwf : WellFounded r) {C : αSort v} (a : α) (h : (x : α) → ((y : α) → r y xC y)C x) :
C a
Equations
  • hwf.recursion a h = Acc.rec (fun (x₁ : α) (h_1 : ∀ (y : α), r y x₁Acc r y) (ih : (y : α) → r y x₁C y) => h x₁ ih)
theorem WellFounded.induction {α : Sort u} {r : ααProp} (hwf : WellFounded r) {C : αProp} (a : α) (h : ∀ (x : α), (∀ (y : α), r y xC y)C x) :
C a
noncomputable def WellFounded.fixF {α : Sort u} {r : ααProp} {C : αSort v} (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) (a : Acc r x) :
C x
Equations
  • WellFounded.fixF F x a = Acc.rec (fun (x₁ : α) (h : ∀ (y : α), r y x₁Acc r y) (ih : (y : α) → r y x₁C y) => F x₁ ih) a
theorem WellFounded.fixFEq {α : Sort u} {r : ααProp} {C : αSort v} (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) (acx : Acc r x) :
WellFounded.fixF F x acx = F x fun (y : α) (p : r y x) => WellFounded.fixF F y
noncomputable def WellFounded.fix {α : Sort u} {C : αSort v} {r : ααProp} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
C x
Equations
theorem WellFounded.fix_eq {α : Sort u} {C : αSort v} {r : ααProp} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
hwf.fix F x = F x fun (y : α) (x : r y x) => hwf.fix F y
Equations
  • emptyWf = { rel := emptyRelation, wf := }
theorem Subrelation.accessible {α : Sort u} {r q : ααProp} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :
Acc q a
theorem Subrelation.wf {α : Sort u} {r q : ααProp} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
theorem InvImage.accessible {α : Sort u} {β : Sort v} {r : ββProp} {a : α} (f : αβ) (ac : Acc r (f a)) :
Acc (InvImage r f) a
theorem InvImage.wf {α : Sort u} {β : Sort v} {r : ββProp} (f : αβ) (h : WellFounded r) :
@[reducible]
def invImage {α : Sort u_1} {β : Sort u_2} (f : αβ) (h : WellFoundedRelation β) :
Equations
theorem Acc.transGen {α✝ : Sort u_1} {r : α✝α✝Prop} {a : α✝} (h : Acc r a) :
theorem acc_transGen_iff {α✝ : Sort u_1} {r : α✝α✝Prop} {a : α✝} :
theorem WellFounded.transGen {α✝ : Sort u_1} {r : α✝α✝Prop} (h : WellFounded r) :
@[reducible, inline, deprecated Acc.transGen]
abbrev TC.accessible {α✝ : Sort u_1} {r : α✝α✝Prop} {a : α✝} (h : Acc r a) :
Equations
@[reducible, inline, deprecated WellFounded.transGen]
abbrev TC.wf {α✝ : Sort u_1} {r : α✝α✝Prop} (h : WellFounded r) :
Equations
Equations
noncomputable def Nat.strongRecOn {motive : NatSort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
motive n
Equations
@[deprecated Nat.strongRecOn]
noncomputable def Nat.strongInductionOn {motive : NatSort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
motive n
Equations
noncomputable def Nat.caseStrongRecOn {motive : NatSort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m nmotive m)motive n.succ) :
motive a
Equations
  • One or more equations did not get rendered due to their size.
@[deprecated Nat.caseStrongRecOn]
noncomputable def Nat.caseStrongInductionOn {motive : NatSort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m nmotive m)motive n.succ) :
motive a
Equations
@[reducible, inline]
abbrev measure {α : Sort u} (f : αNat) :
Equations
@[reducible, inline]
abbrev sizeOfWFRel {α : Sort u} [SizeOf α] :
Equations
@[instance 100]
Equations
  • instWellFoundedRelationOfSizeOf = sizeOfWFRel
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
theorem Prod.lex_def {α : Type u} {β : Type v} {r : ααProp} {s : ββProp} {p q : α × β} :
Prod.Lex r s p q r p.fst q.fst p.fst = q.fst s p.snd q.snd
instance Prod.Lex.instDecidableRelOfDecidableEq {α : Type u} {β : Type v} [αeqDec : DecidableEq α] {r : ααProp} [rDec : DecidableRel r] {s : ββProp} [sDec : DecidableRel s] :
Equations
  • One or more equations did not get rendered due to their size.
theorem Prod.Lex.right' {β : Type v} (rb : ββProp) {a₂ : Nat} {b₂ : β} {a₁ : Nat} {b₁ : β} (h₁ : a₁ a₂) (h₂ : rb b₁ b₂) :
Prod.Lex Nat.lt rb (a₁, b₁) (a₂, b₂)
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.lexAccessible {α : 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)
@[reducible]
def Prod.lex {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
Equations
  • Prod.lex ha hb = { rel := Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel, wf := }
Equations
  • Prod.instWellFoundedRelation = Prod.lex ha hb
theorem Prod.RProdSubLex {α : Type u} {β : Type v} {ra : ααProp} {rb : ββProp} (a b : α × β) (h : Prod.RProd ra rb a b) :
Prod.Lex ra rb a b
def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) :
Equations
inductive PSigma.Lex {α : Sort u} {β : αSort v} (r : ααProp) (s : (a : α) → β aβ aProp) :
PSigma βPSigma βProp
  • left: ∀ {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂), r a₁ a₂PSigma.Lex r s a₁, b₁ a₂, b₂
  • right: ∀ {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} (a : α) {b₁ b₂ : β a}, s a b₁ b₂PSigma.Lex r s a, b₁ a, b₂
Instances For
theorem PSigma.lexAccessible {α : Sort u} {β : αSort v} {r : ααProp} {s : (a : α) → β aβ aProp} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) :
Acc (PSigma.Lex r s) a, b
@[reducible]
def PSigma.lex {α : Sort u} {β : αSort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) :
Equations
  • PSigma.lex ha hb = { rel := PSigma.Lex WellFoundedRelation.rel fun (a : α) => WellFoundedRelation.rel, wf := }
instance PSigma.instWellFoundedRelation {α : Sort u} {β : αSort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] :
Equations
def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : ααProp) (s : ββProp) :
(_ : α) ×' β(_ : α) ×' βProp
Equations
theorem PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
inductive PSigma.RevLex {α : Sort u} {β : Sort v} (r : ααProp) (s : ββProp) :
(_ : α) ×' β(_ : α) ×' βProp
  • left: ∀ {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} {a₁ a₂ : α} (b : β), r a₁ a₂PSigma.RevLex r s a₁, b a₂, b
  • right: ∀ {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β}, s b₁ b₂PSigma.RevLex r s a₁, b₁ a₂, b₂
theorem PSigma.revLexAccessible {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} {b : β} (acb : Acc s b) (aca : ∀ (a : α), Acc r a) (a : α) :
Acc (PSigma.RevLex r s) a, b
theorem PSigma.revLex {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : WellFounded r) (hb : WellFounded s) :
def PSigma.SkipLeft (α : Type u) {β : Type v} (s : ββProp) :
(_ : α) ×' β(_ : α) ×' βProp
Equations
def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) :
WellFoundedRelation ((_ : α) ×' β)
Equations
theorem PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : ββProp} (a₁ a₂ : α) (h : s b₁ b₂) :
PSigma.SkipLeft α s a₁, b₁ a₂, b₂