# 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.

Instances For
@[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
Instances For
@[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
Instances For
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”.

• intro: ∀ {α : Sort u} {r : ααProp}, (∀ (a : α), Acc r a)
Instances For
class WellFoundedRelation (α : Sort u) :
Sort (max 1 u)
Instances
theorem WellFoundedRelation.wf {α : Sort u} [self : ] :
WellFounded WellFoundedRelation.rel
theorem WellFounded.apply {α : Sort u} {r : ααProp} (wf : ) (a : α) :
Acc r a
noncomputable def WellFounded.recursion {α : Sort u} {r : ααProp} (hwf : ) {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)
Instances For
theorem WellFounded.induction {α : Sort u} {r : ααProp} (hwf : ) {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
• = Acc.rec (fun (x₁ : α) (h : ∀ (y : α), r y x₁Acc r y) (ih : (y : α) → r y x₁C y) => F x₁ ih) a
Instances For
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) =>
noncomputable def WellFounded.fix {α : Sort u} {C : αSort v} {r : ααProp} (hwf : ) (F : (x : α) → ((y : α) → r y xC y)C x) (x : α) :
C x
Equations
• hwf.fix F x =
Instances For
theorem WellFounded.fix_eq {α : Sort u} {C : αSort v} {r : ααProp} (hwf : ) (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
def emptyWf {α : Sort u} :
Equations
• emptyWf = { rel := emptyRelation, wf := }
Instances For
theorem Subrelation.accessible {α : Sort u} {r : ααProp} {q : ααProp} {a : α} (h₁ : ) (ac : Acc r a) :
Acc q a
theorem Subrelation.wf {α : Sort u} {r : ααProp} {q : ααProp} (h₁ : ) (h₂ : ) :
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 : ) :
@[reducible]
def invImage {α : Sort u_1} {β : Sort u_2} (f : αβ) (h : ) :
Equations
Instances For
theorem Acc.transGen :
∀ {α : Sort u_1} {r : ααProp} {a : α}, Acc r aAcc a
theorem acc_transGen_iff :
∀ {α : Sort u_1} {r : ααProp} {a : α}, Acc a Acc r a
theorem WellFounded.transGen :
∀ {α : Sort u_1} {r : ααProp},
@[reducible, inline, deprecated Acc.transGen]
abbrev TC.accessible :
∀ {α : Sort u_1} {r : ααProp} {a : α}, Acc r aAcc a
Equations
Instances For
@[reducible, inline, deprecated WellFounded.transGen]
abbrev TC.wf :
∀ {α : Sort u_1} {r : ααProp},
Equations
Instances For
Equations
Instances For
noncomputable def Nat.strongRecOn {motive : NatSort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < nmotive m)motive n) :
motive n
Equations
Instances For
@[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
Instances For
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.
Instances For
@[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
Instances For
@[reducible, inline]
abbrev measure {α : Sort u} (f : αNat) :
Equations
Instances For
@[reducible, inline]
abbrev sizeOfWFRel {α : Sort u} [] :
Equations
Instances For
@[instance 100]
instance instWellFoundedRelationOfSizeOf {α : Sort u_1} [] :
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 : ] {r : ααProp} [rDec : ] {s : ββProp} [sDec : ] :
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₂)
Instances For
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 : ) (hb : ) :
Equations
• Prod.lex ha hb = { rel := Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel, wf := }
Instances For
instance Prod.instWellFoundedRelation {α : Type u} {β : Type v} [ha : ] [hb : ] :
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 : ) (hb : ) :
Equations
Instances For
inductive PSigma.Lex {α : Sort u} {β : αSort v} (r : ααProp) (s : (a : α) → β aβ aProp) :
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 : ) (hb : (a : α) → WellFoundedRelation (β a)) :
Equations
• PSigma.lex ha hb = { rel := PSigma.Lex WellFoundedRelation.rel fun (a : α) => WellFoundedRelation.rel, wf := }
Instances For
instance PSigma.instWellFoundedRelation {α : Sort u} {β : αSort v} [ha : ] [hb : (a : α) → WellFoundedRelation (β a)] :
Equations
def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : ααProp) (s : ββProp) :
(_ : α) ×' β(_ : α) ×' βProp
Equations
Instances For
theorem PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : ααProp} {s : ββProp} (ha : ) (hb : ) :
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₂
Instances For
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 : ) (hb : ) :
def PSigma.SkipLeft (α : Type u) {β : Type v} (s : ββProp) :
(_ : α) ×' β(_ : α) ×' βProp
Equations
Instances For
def PSigma.skipLeft (α : Type u) {β : Type v} (hb : ) :
WellFoundedRelation ((_ : α) ×' β)
Equations
Instances For
theorem PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ : β} {b₂ : β} {s : ββProp} (a₁ : α) (a₂ : α) (h : s b₁ b₂) :
PSigma.SkipLeft α s a₁, b₁ a₂, b₂