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

  If all elements are accessible via r, then r is well-founded.

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

A type that has a standard well-founded relation.

Instances are used to prove that functions terminate using well-founded recursion by showing that recursive calls reduce some measure according to a well-founded relation. This relation can combine well-founded relations on the recursive function's parameters.

• rel : α → α → Prop

  A well-founded relation on α.

• wf : WellFounded rel

  A proof that rel is, in fact, well-founded.

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

A well-founded fixpoint. If satisfying the motive C for all values that are smaller according to a well-founded relation allows it to be satisfied for the current value, then it is satisfied for all values.

This function is used as part of the elaboration of well-founded recursion.

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 α

The inverse image of a well-founded relation is well-founded.

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)

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

Strong induction on the natural numbers.

The induction hypothesis is that all numbers less than a given number satisfy the motive, which should be demonstrated for the given number.

Equations

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

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

Case analysis based on strong induction for the natural numbers.

Equations

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

@[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

A lexicographical order based on the orders ra and rb for the elements of pairs.

• 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₂)

  If the first projections of two pairs are ordered, then they are lexicographically ordered.

• right {α : Type u} {β : Type v} {ra : α → α → Prop} {rb : β → β → Prop} (a : α) {b₁ b₂ : β} (h : rb b₁ b₂) : Prod.Lex ra rb (a, b₁) (a, b₂)

  If the first projections of two pairs are equal, then they are lexicographically ordered if the second projections are ordered.

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.