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

Instances For

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

Instances For

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

Instances For

source
theorem Acc.inv {α : Sort u} {r : α → α → Prop} {x y : α} (h₁ : Acc r x) (h₂ : r y x) :
Acc r y
source
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.

Instances For

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

Instances

source
theorem WellFounded.apply {α : Sort u} {r : α → α → Prop} (wf : WellFounded r) (a : α) :
Acc r a
source
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) ⋯

Instances For

source
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
source
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

Instances For

source
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 ⋯
source
@[reducible, inline, deprecated WellFounded.fixF_eq (since := "2025-04-04")]
abbrev WellFounded.fixFEq {α : Sort u_1} {r : α → α → Prop} {C : α → Sort u_2} (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 ⋯
Equations

- @WellFounded.fixFEq = @WellFounded.fixF_eq

Instances For

source
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 ⋯

Instances For

source
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
source
def emptyWf {α : Sort u} :
WellFoundedRelation α
Equations

- emptyWf = { rel := emptyRelation, wf := ⋯ }

Instances For

source
theorem Subrelation.accessible {α : Sort u} {r q : α → α → Prop} {a : α} (h₁ : Subrelation q r) (ac : Acc r a) :
Acc q a
source
theorem Subrelation.wf {α : Sort u} {r q : α → α → Prop} (h₁ : Subrelation q r) (h₂ : WellFounded r) :
WellFounded q
source
theorem InvImage.accAux {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) {b : β} (ac : Acc r b) (x : α) :
f x = b → Acc (InvImage r f) x
source
theorem InvImage.accessible {α : Sort u} {β : Sort v} {r : β → β → Prop} {a : α} (f : α → β) (ac : Acc r (f a)) :
Acc (InvImage r f) a
source
theorem InvImage.wf {α : Sort u} {β : Sort v} {r : β → β → Prop} (f : α → β) (h : WellFounded r) :
WellFounded (InvImage r f)
source
@[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 := ⋯ }

Instances For

source
theorem Acc.transGen {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} {a : α✝} (h : Acc r a) :
Acc (Relation.TransGen r) a
source
theorem acc_transGen_iff {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} {a : α✝} :
Acc (Relation.TransGen r) a ↔ Acc r a
source
theorem WellFounded.transGen {α✝ : Sort u_1} {r : α✝ → α✝ → Prop} (h : WellFounded r) :
WellFounded (Relation.TransGen r)
source
def Nat.lt_wfRel :
WellFoundedRelation Nat
Equations

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

Instances For

source
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

Instances For

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

Instances For

source
@[reducible, inline]
abbrev measure {α : Sort u} (f : α → Nat) :
WellFoundedRelation α
Equations

- measure f = invImage f Nat.lt_wfRel

Instances For

source
@[reducible, inline, instance 100]
instance sizeOfWFRel {α : Sort u} [SizeOf α] :
WellFoundedRelation α
Equations

- sizeOfWFRel = measure sizeOf

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

Instances For

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

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

Instances For

source
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)
source
@[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 := ⋯ }

Instances For

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

- Prod.instWellFoundedRelation = Prod.lex ha hb

source
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
source
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 := ⋯ }

Instances For

source
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₂⟩

Instances For

source
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⟩
source
@[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 := ⋯ }

Instances For

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

- PSigma.instWellFoundedRelation = PSigma.lex ha hb

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

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

Instances For

source
theorem PSigma.lexNdepWf {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :
WellFounded (lexNdep r s)
source
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₂⟩

Instances For

source
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⟩
source
theorem PSigma.revLex {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} (ha : WellFounded r) (hb : WellFounded s) :
WellFounded (RevLex r s)
source
def PSigma.SkipLeft (α : Type u) {β : Type v} (s : β → β → Prop) :
(_ : α) ×' β → (_ : α) ×' β → Prop
Equations

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

Instances For

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

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

Instances For

source
theorem PSigma.mkSkipLeft {α : Type u} {β : Type v} {b₁ b₂ : β} {s : β → β → Prop} (a₁ a₂ : α) (h : s b₁ b₂) :
SkipLeft α s ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
source
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

Instances For

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