This module contains some basic definitions and results from domain theory, intended to be used as the underlying construction of the partial_fixpoint feature. It is not meant to be used as a general purpose library for domain theory, but can be of interest to users who want to extend the partial_fixpoint machinery (e.g. mark more functions as monotone or register more monads).

This follows the corresponding Isabelle development, as also described in Alexander Krauss: Recursive Definitions of Monadic Functions.

class Lean.Order.PartialOrder (α : Sort u) : Sort (max 1 u)

A partial order is a reflexive, transitive and antisymmetric relation.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• rel : α → α → Prop

  A “less-or-equal-to” or “approximates” relation.

  This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y

def Lean.Order.«term_⊑_» : TrailingParserDescr

A “less-or-equal-to” or “approximates” relation.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.«term_⊑_» = Lean.ParserDescr.trailingNode `Lean.Order.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

theorem Lean.Order.PartialOrder.rel_of_eq {α : Sort u} [PartialOrder α] {x y : α} (h : x = y) : rel x y

def Lean.Order.chain {α : Sort u} [PartialOrder α] (c : α → Prop) : Prop

A chain is a totally ordered set (representing a set as a predicate).

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.chain c = ∀ (x y : α), c x → c y → Lean.Order.PartialOrder.rel x y ∨ Lean.Order.PartialOrder.rel y x

class Lean.Order.CCPO (α : Sort u) extends Lean.Order.PartialOrder α : Sort (max 1 u)

A chain-complete partial order (CCPO) is a partial order where every chain a least upper bound.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• csup : (α → Prop) → α

  The least upper bound of a chain.

  This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• csup_spec {x : α} {c : α → Prop} (hc : chain c) : PartialOrder.rel (csup c) x ↔ ∀ (y : α), c y → PartialOrder.rel y x

theorem Lean.Order.csup_le {α : Sort u} [CCPO α] {x : α} {c : α → Prop} (hchain : chain c) : (∀ (y : α), c y → PartialOrder.rel y x) → PartialOrder.rel (CCPO.csup c) x

theorem Lean.Order.le_csup {α : Sort u} [CCPO α] {c : α → Prop} (hchain : chain c) {y : α} (hy : c y) : PartialOrder.rel y (CCPO.csup c)

def Lean.Order.bot {α : Sort u} [CCPO α] : α

The bottom element is the least upper bound of the empty chain.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.bot = Lean.Order.CCPO.csup fun (x : α) => False

def Lean.Order.«term⊥» : ParserDescr

Equations

• Lean.Order.«term⊥» = Lean.ParserDescr.node `Lean.Order.«term⊥» 1024 (Lean.ParserDescr.symbol "⊥")

theorem Lean.Order.bot_le {α : Sort u} [CCPO α] (x : α) : PartialOrder.rel bot x

def Lean.Order.monotone {α : Sort u} [PartialOrder α] {β : Sort v} [PartialOrder β] (f : α → β) : Prop

A function is monotone if if it maps related elements to releated elements.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.monotone f = ∀ (x y : α), Lean.Order.PartialOrder.rel x y → Lean.Order.PartialOrder.rel (f x) (f y)

theorem Lean.Order.monotone_const {α : Sort u} [PartialOrder α] {β : Sort v} [PartialOrder β] (c : β) : monotone fun (x : α) => c

theorem Lean.Order.monotone_id {α : Sort u} [PartialOrder α] : monotone fun (x : α) => x

theorem Lean.Order.monotone_compose {α : Sort u} [PartialOrder α] {β : Sort v} [PartialOrder β] {γ : Sort w} [PartialOrder γ] {f : α → β} {g : β → γ} (hf : monotone f) (hg : monotone g) : monotone fun (x : α) => g (f x)

def Lean.Order.admissible {α : Sort u} [CCPO α] (P : α → Prop) : Prop

A predicate is admissable if it can be transferred from the elements of a chain to the chains least upper bound. Such predicates can be used in fixpoint induction.

This definition implies P ⊥. Sometimes (e.g. in Isabelle) the empty chain is excluded from this definition, and P ⊥ is a separate condition of the induction predicate.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.admissible P = ∀ (c : α → Prop), Lean.Order.chain c → (∀ (x : α), c x → P x) → P (Lean.Order.CCPO.csup c)

theorem Lean.Order.admissible_const_true {α : Sort u} [CCPO α] : admissible fun (x : α) => True

theorem Lean.Order.admissible_and {α : Sort u} [CCPO α] (P Q : α → Prop) (hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible fun (x : α) => P x ∧ Q x

theorem Lean.Order.chain_conj {α : Sort u} [CCPO α] (c P : α → Prop) (hchain : chain c) : chain fun (x : α) => c x ∧ P x

theorem Lean.Order.csup_conj {α : Sort u} [CCPO α] (c P : α → Prop) (hchain : chain c) (h : ∀ (x : α), c x → ∃ (y : α), c y ∧ PartialOrder.rel x y ∧ P y) : CCPO.csup c = CCPO.csup fun (x : α) => c x ∧ P x

theorem Lean.Order.admissible_or {α : Sort u} [CCPO α] (P Q : α → Prop) (hadm₁ : admissible P) (hadm₂ : admissible Q) : admissible fun (x : α) => P x ∨ Q x

def Lean.Order.admissible_pi {α : Sort u} [CCPO α] {β : Sort u_1} (P : α → β → Prop) (hadm₁ : ∀ (y : β), admissible fun (x : α) => P x y) : admissible fun (x : α) => ∀ (y : β), P x y

Equations

• ⋯ = ⋯

inductive Lean.Order.iterates {α : Sort u} [CCPO α] (f : α → α) : α → Prop

The transfinite iteration of a function f is a set that is ⊥ and is closed under application of f and csup.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• step {α : Sort u} [CCPO α] {f : α → α} {x : α} : iterates f x → iterates f (f x)
• sup {α : Sort u} [CCPO α] {f : α → α} {c : α → Prop} (hc : chain c) (hi : ∀ (x : α), c x → iterates f x) : iterates f (CCPO.csup c)

theorem Lean.Order.chain_iterates {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) : chain (iterates f)

theorem Lean.Order.rel_f_of_iterates {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) {x : α} (hx : iterates f x) : PartialOrder.rel x (f x)

def Lean.Order.fix {α : Sort u} [CCPO α] (f : α → α) (hmono : monotone f) : α

The least fixpoint of a monotone function is the least upper bound of its transfinite iteration.

The monotone f assumption is not strictly necessarily for the definition, but without this the definition is not very meaningful and it simplifies applying theorems like fix_eq if every use of fix already has the monotonicty requirement.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.fix f hmono = Lean.Order.CCPO.csup (Lean.Order.iterates f)

theorem Lean.Order.fix_eq {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) : fix f hf = f (fix f hf)

The main fixpoint theorem for fixedpoints of monotone functions in chain-complete partial orders.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

theorem Lean.Order.fix_induct {α : Sort u} [CCPO α] {f : α → α} (hf : monotone f) (motive : α → Prop) (hadm : admissible motive) (h : ∀ (x : α), motive x → motive (f x)) : motive (fix f hf)

The fixpoint induction theme: An admissible predicate holds for a least fixpoint if it is preserved by the fixpoint's function.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

instance Lean.Order.instOrderPi {α : Sort u} {β : α → Sort v} [(x : α) → PartialOrder (β x)] : PartialOrder ((x : α) → β x)

Equations

• Lean.Order.instOrderPi = { rel := fun (f g : (x : α) → β x) => ∀ (x : α), Lean.Order.PartialOrder.rel (f x) (g x), rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

theorem Lean.Order.monotone_of_monotone_apply {α : Sort u} {β : α → Sort v} {γ : Sort w} [PartialOrder γ] [(x : α) → PartialOrder (β x)] (f : γ → (x : α) → β x) (h : ∀ (y : α), monotone fun (x : γ) => f x y) : monotone f

theorem Lean.Order.monotone_apply {α : Sort u} {β : α → Sort v} {γ : Sort w} [PartialOrder γ] [(x : α) → PartialOrder (β x)] (a : α) (f : γ → (x : α) → β x) (h : monotone f) : monotone fun (x : γ) => f x a

theorem Lean.Order.chain_apply {α : Sort u} {β : α → Sort v} [(x : α) → PartialOrder (β x)] {c : ((x : α) → β x) → Prop} (hc : chain c) (x : α) : chain fun (y : β x) => ∃ (f : (x : α) → β x), c f ∧ f x = y

def Lean.Order.fun_csup {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (c : ((x : α) → β x) → Prop) (x : α) : β x

Equations

• Lean.Order.fun_csup c x = Lean.Order.CCPO.csup fun (y : β x) => ∃ (f : (x : α) → β x), c f ∧ f x = y

instance Lean.Order.instCCPOPi {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] : CCPO ((x : α) → β x)

Equations

• Lean.Order.instCCPOPi = Lean.Order.CCPO.mk Lean.Order.fun_csup ⋯

def Lean.Order.admissible_apply {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (P : (x : α) → β x → Prop) (x : α) (hadm : admissible (P x)) : admissible fun (f : (x : α) → β x) => P x (f x)

Equations

• ⋯ = ⋯

def Lean.Order.admissible_pi_apply {α : Sort u} {β : α → Sort v} [(x : α) → CCPO (β x)] (P : (x : α) → β x → Prop) (hadm : ∀ (x : α), admissible (P x)) : admissible fun (f : (x : α) → β x) => ∀ (x : α), P x (f x)

Equations

• ⋯ = ⋯

theorem Lean.Order.monotone_letFun {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] (v : γ) (k : α → γ → β) (hmono : ∀ (y : γ), monotone fun (x : α) => k x y) : monotone fun (x : α) => letFun v (k x)

theorem Lean.Order.monotone_ite {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (c : Prop) [Decidable c] (k₁ k₂ : α → β) (hmono₁ : monotone k₁) (hmono₂ : monotone k₂) : monotone fun (x : α) => if c then k₁ x else k₂ x

theorem Lean.Order.monotone_dite {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] (c : Prop) [Decidable c] (k₁ : α → c → β) (k₂ : α → ¬c → β) (hmono₁ : monotone k₁) (hmono₂ : monotone k₂) : monotone fun (x : α) => dite c (k₁ x) (k₂ x)

instance Lean.Order.instPartialOrderPProd {α : Sort u} {β : Sort v} [PartialOrder α] [PartialOrder β] : PartialOrder (α ×' β)

Equations

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

theorem Lean.Order.monotone_pprod {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α} {g : γ → β} (hf : monotone f) (hg : monotone g) : monotone fun (x : γ) => ⟨f x, g x⟩

theorem Lean.Order.monotone_pprod_fst {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone fun (x : γ) => (f x).fst

theorem Lean.Order.monotone_pprod_snd {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone fun (x : γ) => (f x).snd

def Lean.Order.chain_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) : α → Prop

Equations

• Lean.Order.chain_pprod_fst c a = ∃ (b : β), c ⟨a, b⟩

def Lean.Order.chain_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) : β → Prop

Equations

• Lean.Order.chain_pprod_snd c b = ∃ (a : α), c ⟨a, b⟩

theorem Lean.Order.chain.pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : chain (chain_pprod_fst c)

theorem Lean.Order.chain.pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (c : α ×' β → Prop) (hchain : chain c) : chain (chain_pprod_snd c)

instance Lean.Order.instCCPOPProd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] : CCPO (α ×' β)

Equations

• Lean.Order.instCCPOPProd = Lean.Order.CCPO.mk (fun (c : α ×' β → Prop) => ⟨Lean.Order.CCPO.csup (Lean.Order.chain_pprod_fst c), Lean.Order.CCPO.csup (Lean.Order.chain_pprod_snd c)⟩) ⋯

theorem Lean.Order.admissible_pprod_fst {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : α → Prop) (hadm : admissible P) : admissible fun (x : α ×' β) => P x.fst

theorem Lean.Order.admissible_pprod_snd {α : Sort u} {β : Sort v} [CCPO α] [CCPO β] (P : β → Prop) (hadm : admissible P) : admissible fun (x : α ×' β) => P x.snd

def Lean.Order.FlatOrder {α : Sort u} (b : α) : Sort u

FlatOrder b wraps the type α with the flat partial order generated by ∀ x, b ⊑ x.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

Equations

• Lean.Order.FlatOrder b = α

inductive Lean.Order.FlatOrder.rel {α : Sort u} {b : α} (x y : FlatOrder b) : Prop

The flat partial order generated by ∀ x, b ⊑ x.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• bot {α : Sort u} {b : α} {x : FlatOrder b} : rel b x
• refl {α : Sort u} {b : α} {x : FlatOrder b} : x.rel x

instance Lean.Order.FlatOrder.instOrder {α : Sort u} {b : α} : PartialOrder (FlatOrder b)

Equations

• Lean.Order.FlatOrder.instOrder = { rel := Lean.Order.FlatOrder.rel, rel_refl := ⋯, rel_trans := ⋯, rel_antisymm := ⋯ }

noncomputable def Lean.Order.flat_csup {α : Sort u} {b : α} (c : FlatOrder b → Prop) : FlatOrder b

Equations

• Lean.Order.flat_csup c = if h : ∃ (x : Lean.Order.FlatOrder b), c x ∧ x ≠ b then Classical.choose h else b

noncomputable instance Lean.Order.FlatOrder.instCCPO {α : Sort u} {b : α} : CCPO (FlatOrder b)

Equations

• Lean.Order.FlatOrder.instCCPO = Lean.Order.CCPO.mk Lean.Order.flat_csup ⋯

theorem Lean.Order.admissible_flatOrder {α : Sort u} {b : α} (P : FlatOrder b → Prop) (hnot : P b) : admissible P

class Lean.Order.MonoBind (m : Type u → Type v) [Bind m] [(α : Type u) → PartialOrder (m α)] : Prop

The class MonoBind m indicates that every m α has a PartialOrder, and that the bind operation on m is monotone in both arguments with regard to that order.

This is intended to be used in the construction of partial_fixpoint, and not meant to be used otherwise.

• bind_mono_left {α b : Type u} {a₁ a₂ : m α} {f : α → m b} (h : PartialOrder.rel a₁ a₂) : PartialOrder.rel (a₁ >>= f) (a₂ >>= f)
• bind_mono_right {α b : Type u} {a : m α} {f₁ f₂ : α → m b} (h : ∀ (x : α), PartialOrder.rel (f₁ x) (f₂ x)) : PartialOrder.rel (a >>= f₁) (a >>= f₂)

theorem Lean.Order.monotone_bind (m : Type u → Type v) [Bind m] [(α : Type u) → PartialOrder (m α)] [MonoBind m] {α β : Type u} {γ : Type w} [PartialOrder γ] (f : γ → m α) (g : γ → α → m β) (hmono₁ : monotone f) (hmono₂ : monotone g) : monotone fun (x : γ) => f x >>= g x

instance Lean.Order.instPartialOrderOption {α : Type u_1} : PartialOrder (Option α)

Equations

• Lean.Order.instPartialOrderOption = inferInstanceAs (Lean.Order.PartialOrder (Lean.Order.FlatOrder none))

noncomputable instance Lean.Order.instCCPOOption {α : Type u_1} : CCPO (Option α)

Equations

• Lean.Order.instCCPOOption = inferInstanceAs (Lean.Order.CCPO (Lean.Order.FlatOrder none))

instance Lean.Order.instMonoBindOption : MonoBind Option

theorem Lean.Order.admissible_eq_some {α : Type u_1} (P : Prop) (y : α) : admissible fun (x : Option α) => x = some y → P

instance Lean.Order.instPartialOrderExceptTOfMonad {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] [inst : (α : Type u_1) → PartialOrder (m α)] : PartialOrder (ExceptT ε m α)

Equations

• Lean.Order.instPartialOrderExceptTOfMonad = inst (Except ε α)

instance Lean.Order.instCCPOExceptTOfMonadOfPartialOrder {m : Type u_1 → Type u_2} {ε α : Type u_1} [Monad m] [(α : Type u_1) → PartialOrder (m α)] [inst : (α : Type u_1) → CCPO (m α)] : CCPO (ExceptT ε m α)

Equations

• Lean.Order.instCCPOExceptTOfMonadOfPartialOrder = inst (Except ε α)

instance Lean.Order.instMonoBindExceptTOfCCPO {m : Type u_1 → Type u_2} {ε : Type u_1} [Monad m] [(α : Type u_1) → PartialOrder (m α)] [(α : Type u_1) → CCPO (m α)] [MonoBind m] : MonoBind (ExceptT ε m)

def Lean.Order.Example.findF (P : Nat → Bool) (rec : Nat → Option Nat) (x : Nat) : Option Nat

Equations

• Lean.Order.Example.findF P rec x = if P x = true then some x else rec (x + 1)

noncomputable def Lean.Order.Example.find (P : Nat → Bool) : Nat → Option Nat

Equations

• Lean.Order.Example.find P = Lean.Order.fix (Lean.Order.Example.findF P) ⋯

theorem Lean.Order.Example.find_eq {P : Nat → Bool} : find P = findF P (find P)

theorem Lean.Order.Example.find_spec {P : Nat → Bool} (n m : Nat) : find P n = some m → n ≤ m ∧ P m = true