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

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

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

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

theorem WellFounded.fixF_eq {α : 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 ⋯

def WellFounded.wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : { x : α // Acc r x }

Attaches to x the proof that x is accessible in the given well-founded relation. This can be used in recursive function definitions to explicitly use a different relation than the one inferred by default:

def otherWF : WellFounded Nat := …
def foo (n : Nat) := …
termination_by otherWF.wrap n

@[simp]

theorem WellFounded.val_wrap {α : Sort u} {r : α → α → Prop} (h : WellFounded r) (x : α) : (h.wrap x).val = x

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.

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

@[implicit_reducible]

def emptyWf {α : Sort u} : WellFoundedRelation α

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.accAux {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) {b : β} (ac : Acc r b) (x : α) : f x = b → Acc (InvImage r f) x

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.

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 Acc.inv_of_transGen {α : Sort u_1} {r : α → α → Prop} {x y : α} (h₁ : Acc r x) (h₂ : Relation.TransGen r y x) : Acc r y

If Acc r x holds and y is transitively related to x, then Acc r y holds, too.

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

@[implicit_reducible]

def Nat.lt_wfRel : WellFoundedRelation Nat

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.

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.

@[reducible, inline]

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

@[reducible, inline, instance 100]

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

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

@[implicit_reducible]

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)

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 (α × β)

@[implicit_reducible]

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

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

@[implicit_reducible]

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

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 β)

@[implicit_reducible]

instance PSigma.instWellFoundedRelation {α : Sort u} {β : α → Sort v} [ha : WellFoundedRelation α] [hb : (a : α) → WellFoundedRelation (β a)] : WellFoundedRelation (PSigma β)

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

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

@[implicit_reducible]

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

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

def WellFounded.Nat.eager (n : Nat) : Nat

Helper gadget that prevents reduction of Nat.eager n unless n evaluates to a ground term.

theorem WellFounded.Nat.eager_eq (n : Nat) : eager n = n

def WellFounded.Nat.fix {α : Sort u} {motive : α → Sort v} (h : α → Nat) (F : (x : α) → ((y : α) → InvImage (fun (x1 x2 : Nat) => x1 < x2) h y x → motive y) → motive x) (x : α) : motive x

A well-founded fixpoint operator specialized for Nat-valued measures. Given a measure h, it expects its higher order function argument F to invoke its argument only on values y that are smaller than x with regard to h.

In contrast to WellFounded.fix, this fixpoint operator reduces on closed terms. (More precisely: when h x evaluates to a ground value)

def WellFounded.Nat.fix.go {α : Sort u} {motive : α → Sort v} (h : α → Nat) (F : (x : α) → ((y : α) → InvImage (fun (x1 x2 : Nat) => x1 < x2) h y x → motive y) → motive x) (fuel : Nat) (x : α) : h x < fuel → motive x

theorem WellFounded.Nat.fix.go_congr {α : Sort u} {motive : α → Sort v} (h : α → Nat) (F : (x : α) → ((y : α) → InvImage (fun (x1 x2 : Nat) => x1 < x2) h y x → motive y) → motive x) (x : α) (fuel₁ fuel₂ : Nat) (h₁ : h x < fuel₁) (h₂ : h x < fuel₂) : go h F fuel₁ x h₁ = go h F fuel₂ x h₂

theorem WellFounded.Nat.fix_eq {α : Sort u} {motive : α → Sort v} (h : α → Nat) (F : (x : α) → ((y : α) → InvImage (fun (x1 x2 : Nat) => x1 < x2) h y x → motive y) → motive x) (x : α) : fix h F x = F x fun (y : α) (x : InvImage (fun (x1 x2 : Nat) => x1 < x2) h y x) => fix h F y

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.

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.