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 : α) (h : ∀ (y : α), r y x → Acc 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 x → Acc r y) → ((y : α) → r y x → C y) → C x) {a : α} (n : Acc r a) : C a

Equations

• Acc.ndrec m n = Acc.rec m n

@[reducible, inline]

noncomputable abbrev Acc.ndrecOn {α : Sort u2} {r : α → α → Prop} {C : α → Sort u1} {a : α} (n : Acc r a) (m : (x : α) → (∀ (y : α), r y x → Acc r y) → ((y : α) → r y x → C y) → C x) : C a

Equations

• n.ndrecOn m = Acc.rec m n

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) : 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} (h : ∀ (a : α), Acc r a) : WellFounded r

class WellFoundedRelation (α : Sort u) : Sort (max 1 u)

• rel : α → α → Prop
• wf : WellFounded rel

Instances

• PSigma.instWellFoundedRelation
• Prod.instWellFoundedRelation
• instWellFoundedRelationOfSizeOf

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 x → C 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 x → C y) → C x) : C a

noncomputable def WellFounded.fixF {α : 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

• 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 x → C y) → C x) (x : α) (acx : Acc r x) : fixF F x acx = F x fun (y : α) (p : r y x) => fixF F y ⋯

noncomputable def WellFounded.fix {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : C x

Equations

• hwf.fix F x = WellFounded.fixF F x ⋯

theorem WellFounded.fix_eq {α : Sort u} {C : α → Sort v} {r : α → α → Prop} (hwf : WellFounded r) (F : (x : α) → ((y : α) → r y x → C y) → C x) (x : α) : hwf.fix F x = F x fun (y : α) (x : r y x) => hwf.fix F y

def emptyWf {α : Sort u} : WellFoundedRelation α

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) : WellFounded q

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) : WellFounded (InvImage r f)

@[reducible]

def invImage {α : Sort u_1} {β : Sort u_2} (f : α → β) (h : WellFoundedRelation β) : WellFoundedRelation α

Equations

• invImage f h = { rel := InvImage WellFoundedRelation.rel f, wf := ⋯ }

theorem Acc.transGen {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} {a : α✝} (h : Acc r a) : Acc (Relation.TransGen r) a

theorem acc_transGen_iff {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} {a : α✝} : Acc (Relation.TransGen r) a ↔ Acc r a

theorem WellFounded.transGen {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} (h : WellFounded r) : WellFounded (Relation.TransGen r)

@[reducible, inline, deprecated Acc.transGen (since := "2024-07-16")]

abbrev TC.accessible {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} {a : α✝} (h : Acc r a) : Acc (Relation.TransGen r) a

Equations

• @TC.accessible = @Acc.transGen

@[reducible, inline, deprecated WellFounded.transGen (since := "2024-07-16")]

abbrev TC.wf {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} (h : WellFounded r) : WellFounded (Relation.TransGen r)

Equations

• @TC.wf = @WellFounded.transGen

def Nat.lt_wfRel : WellFoundedRelation Nat

Equations

• Nat.lt_wfRel = { rel := fun (x1 x2 : Nat) => x1 < x2, wf := Nat.lt_wfRel.proof_1 }

noncomputable def Nat.strongRecOn {motive : Nat → Sort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) : motive n

Equations

• Nat.strongRecOn n ind = ⋯.fix ind n

@[deprecated Nat.strongRecOn (since := "2024-08-27")]

noncomputable def Nat.strongInductionOn {motive : Nat → Sort u} (n : Nat) (ind : (n : Nat) → ((m : Nat) → m < n → motive m) → motive n) : motive n

Equations

• Nat.strongInductionOn n ind = Nat.strongRecOn n ind

noncomputable def Nat.caseStrongRecOn {motive : Nat → Sort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m ≤ n → motive m) → motive n.succ) : motive a

Equations

• One or more equations did not get rendered due to their size.

@[deprecated Nat.caseStrongRecOn (since := "2024-08-27")]

noncomputable def Nat.caseStrongInductionOn {motive : Nat → Sort u} (a : Nat) (zero : motive 0) (ind : (n : Nat) → ((m : Nat) → m ≤ n → motive m) → motive n.succ) : motive a

Equations

• Nat.caseStrongInductionOn a zero ind = Nat.caseStrongRecOn a zero ind

@[reducible, inline]

abbrev measure {α : Sort u} (f : α → Nat) : WellFoundedRelation α

Equations

• measure f = invImage f Nat.lt_wfRel

@[reducible, inline]

abbrev sizeOfWFRel {α : Sort u} [SizeOf α] : WellFoundedRelation α

Equations

• sizeOfWFRel = measure sizeOf

@[instance 100]

instance instWellFoundedRelationOfSizeOf {α : Sort u_1} [SizeOf α] : WellFoundedRelation α

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₂ : β) (h : ra a₁ a₂) : Prod.Lex ra rb (a₁, b₁) (a₂, b₂)
• right {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β} (h : rb b₁ b₂) : Prod.Lex ra rb (a, b₁) (a, b₂)

Instances For

• Prod.Lex.instDecidableRelOfDecidableEq

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] : DecidableRel (Prod.Lex r 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₂ : β} (h₁ : ra a₁ a₂) (h₂ : rb b₁ b₂) : 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 β) : WellFoundedRelation (α × β)

Equations

• Prod.lex ha hb = { rel := Prod.Lex WellFoundedRelation.rel WellFoundedRelation.rel, wf := ⋯ }

instance Prod.instWellFoundedRelation {α : Type u} {β : Type v} [ha : WellFoundedRelation α] [hb : WellFoundedRelation β] : WellFoundedRelation (α × β)

Equations

• Prod.instWellFoundedRelation = Prod.lex ha hb

theorem Prod.RProdSubLex {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a b : α × β) (h : RProd ra rb a b) : Prod.Lex ra rb a b

def Prod.rprod {α : Type u} {β : Type v} (ha : WellFoundedRelation α) (hb : WellFoundedRelation β) : WellFoundedRelation (α × β)

Equations

• Prod.rprod ha hb = { rel := Prod.RProd WellFoundedRelation.rel WellFoundedRelation.rel, wf := ⋯ }

inductive PSigma.Lex {α : Sort u} {β : α → Sort v} (r : α → α → Prop) (s : (a : α) → β a → β a → Prop) : PSigma β → PSigma β → Prop

• left {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a₁ : α} (b₁ : β a₁) {a₂ : α} (b₂ : β a₂) : r a₁ a₂ → Lex r s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
• right {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} (a : α) {b₁ b₂ : β a} : s a b₁ b₂ → Lex r s ⟨a, b₁⟩ ⟨a, b₂⟩

theorem PSigma.lexAccessible {α : Sort u} {β : α → Sort v} {r : α → α → Prop} {s : (a : α) → β a → β a → Prop} {a : α} (aca : Acc r a) (acb : ∀ (a : α), WellFounded (s a)) (b : β a) : Acc (Lex r s) ⟨a, b⟩

@[reducible]

def PSigma.lex {α : Sort u} {β : α → Sort v} (ha : WellFoundedRelation α) (hb : (a : α) → WellFoundedRelation (β a)) : WellFoundedRelation (PSigma β)

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)] : WellFoundedRelation (PSigma β)

Equations

• PSigma.instWellFoundedRelation = PSigma.lex ha hb

def PSigma.lexNdep {α : Sort u} {β : Sort v} (r : α → α → Prop) (s : β → β → Prop) : (_ : α) ×' β → (_ : α) ×' β → Prop

Equations

• PSigma.lexNdep r s = PSigma.Lex r fun (x : α) => s

theorem PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (lexNdep r 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₂ → RevLex r s ⟨a₁, b⟩ ⟨a₂, b⟩
• right {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (a₁ : α) {b₁ : β} (a₂ : α) {b₂ : β} : s b₁ b₂ → 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 (RevLex r s) ⟨a, b⟩

theorem PSigma.revLex {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) : WellFounded (RevLex r s)

def PSigma.SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) : (_ : α) ×' β → (_ : α) ×' β → Prop

Equations

• PSigma.SkipLeft α s = PSigma.RevLex emptyRelation s

def PSigma.skipLeft (α : Type u) {β : Type v} (hb : WellFoundedRelation β) : WellFoundedRelation ((_ : α) ×' β)

Equations

• PSigma.skipLeft α hb = { rel := PSigma.SkipLeft α WellFoundedRelation.rel, wf := ⋯ }

theorem PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) : SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩

def wfParam {α : Sort u} (a : α) : α

The wfParam gadget is used internally during the construction of recursive functions by wellfounded recursion, to keep track of the parameter for which the automatic introduction of List.attach (or similar) is plausible.

Equations

• wfParam a = a

theorem ite_eq_dite {P : Prop} {α✝ : Sort u_1} {a b : α✝} [Decidable P] : (if P then a else b) = if h : P then binderNameHint h () a else binderNameHint h () b

Reverse direction of dite_eq_ite. Used by the well-founded definition preprocessor to extend the context of a termination proof inside if-then-else with the condition.