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

  The “less-or-equal-to” or “approximates” relation is reflexive.

• rel_trans {x y z : α} : rel x y → rel y z → rel x z

  The “less-or-equal-to” or “approximates” relation is transitive.

• rel_antisymm {x y : α} : rel x y → rel y x → x = y

  The “less-or-equal-to” or “approximates” relation is antisymmetric.

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.

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.

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

  csup c is the least upper bound of the chain c when all elements x that are at least as large as csup c are at least as large as all elements of c, and vice versa.

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.

def Lean.Order.«term⊥» : ParserDescr

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

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

A complete lattice is a partial order where every subset has a least upper bound.

• 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
• sup : (α → Prop) → α

  The least upper bound of an arbitrary subset in the complete_lattice.

• sup_spec {x : α} {c : α → Prop} : PartialOrder.rel (sup c) x ↔ ∀ (y : α), c y → PartialOrder.rel y x

theorem Lean.Order.sup_le {α : Sort u} [CompleteLattice α] {x : α} {c : α → Prop} : (∀ (y : α), c y → PartialOrder.rel y x) → PartialOrder.rel (CompleteLattice.sup c) x

theorem Lean.Order.le_sup {α : Sort u} [CompleteLattice α] {c : α → Prop} {y : α} (hy : c y) : PartialOrder.rel y (CompleteLattice.sup c)

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

theorem Lean.Order.inf_spec {α : Sort u} [CompleteLattice α] {x : α} {c : α → Prop} : PartialOrder.rel x (inf c) ↔ ∀ (y : α), c y → PartialOrder.rel x y

theorem Lean.Order.le_inf {α : Sort u} [CompleteLattice α] {x : α} {c : α → Prop} : (∀ (y : α), c y → PartialOrder.rel x y) → PartialOrder.rel x (inf c)

theorem Lean.Order.inf_le {α : Sort u} [CompleteLattice α] {c : α → Prop} {y : α} (hy : c y) : PartialOrder.rel (inf c) y

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

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

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

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

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

def Lean.Order.lfp {α : Sort u} [CompleteLattice α] (f : α → α) : α

def Lean.Order.lfp_monotone {α : Sort u} [CompleteLattice α] (f : α → α) (hm : monotone f) : α

theorem Lean.Order.lfp_prefixed {α : Sort u} [CompleteLattice α] {f : α → α} {hm : monotone f} : PartialOrder.rel (f (lfp f)) (lfp f)

theorem Lean.Order.lfp_postfixed {α : Sort u} [CompleteLattice α] {f : α → α} {hm : monotone f} : PartialOrder.rel (lfp f) (f (lfp f))

theorem Lean.Order.lfp_fix {α : Sort u} [CompleteLattice α] {f : α → α} (hm : monotone f) : lfp f = f (lfp f)

theorem Lean.Order.lfp_monotone_fix {α : Sort u} [CompleteLattice α] {f : α → α} {hm : monotone f} : lfp_monotone f hm = f (lfp_monotone f hm)

theorem Lean.Order.lfp_le_of_le {α : Sort u} [CompleteLattice α] {x : α} {f : α → α} : PartialOrder.rel (f x) x → PartialOrder.rel (lfp f) x

Park induction principle for least fixpoint. In general, this construction does not require monotonicity of f. Monotonicity is required to show that lfp f is indeed a fixpoint of f.

theorem Lean.Order.lfp_le_of_le_monotone {α : Sort u} [CompleteLattice α] (f : α → α) {hm : monotone f} (x : α) : PartialOrder.rel (f x) x → PartialOrder.rel (lfp_monotone f hm) x

Park induction for least fixpoint of a monotone function f. Takes an explicit witness of f being monotone.

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.

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)

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

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

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

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

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)

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)

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

theorem Lean.Order.PProd.monotone_mk {α : 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.PProd.monotone_fst {α : Sort u} {β : Sort v} {γ : Sort w} [PartialOrder α] [PartialOrder β] [PartialOrder γ] {f : γ → α ×' β} (hf : monotone f) : monotone fun (x : γ) => (f x).fst

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

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

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

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

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

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

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

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

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

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.

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)

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

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

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

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

instance Lean.Order.instMonoBindOption : MonoBind Option

theorem Lean.Order.Option.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 α)

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

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.ImplicationOrder : Type

instance Lean.Order.ImplicationOrder.instOrder : PartialOrder ImplicationOrder

instance Lean.Order.ImplicationOrder.instCompleteLattice : CompleteLattice ImplicationOrder

theorem Lean.Order.implication_order_monotone_exists {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ImplicationOrder) (h : monotone f) : monotone fun (x : α) => Exists (f x)

theorem Lean.Order.implication_order_monotone_forall {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ImplicationOrder) (h : monotone f) : monotone fun (x : α) => ∀ (y : β), f x y

theorem Lean.Order.implication_order_monotone_and {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → ImplicationOrder) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∧ f₂ x

theorem Lean.Order.implication_order_monotone_or {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → ImplicationOrder) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∨ f₂ x

def Lean.Order.ReverseImplicationOrder : Type

instance Lean.Order.ReverseImplicationOrder.instOrder : PartialOrder ReverseImplicationOrder

def Lean.Order.ReverseImplicationOrder.instCompleteLattice : CompleteLattice ReverseImplicationOrder

theorem Lean.Order.coind_monotone_exists {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ReverseImplicationOrder) (h : monotone f) : monotone fun (x : α) => Exists (f x)

theorem Lean.Order.coind_monotone_forall {α : Sort u_1} [PartialOrder α] {β : Sort u_2} (f : α → β → ReverseImplicationOrder) (h : monotone f) : monotone fun (x : α) => ∀ (y : β), f x y

theorem Lean.Order.coind_monotone_and {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → Prop) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∧ f₂ x

theorem Lean.Order.coind_monotone_or {α : Sort u_1} [PartialOrder α] (f₁ f₂ : α → Prop) (h₁ : monotone f₁) (h₂ : monotone f₂) : monotone fun (x : α) => f₁ x ∨ f₂ x

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

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

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