mathlib documentation

order.omega_complete_partial_order

Omega Complete Partial Orders #

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

The concept of an omega-complete partial order (ωCPO) is useful for the formalization of the semantics of programming languages. Its notion of supremum helps define the meaning of recursive procedures.

Main definitions #

Instances of omega_complete_partial_order #

References #

@[simp]
theorem preorder_hom.const_coe (α : Type u_1) {β : Type u_2} [preorder α] [preorder β] (f : β) (ᾰ : α) :
def preorder_hom.const (α : Type u_1) {β : Type u_2} [preorder α] [preorder β] (f : β) :
α →ₘ β

The constant function, as a monotone function.

Equations
def preorder_hom.prod.diag {α : Type u_1} [preorder α] :
α →ₘ α × α

The diagonal function, as a monotone function.

Equations
@[simp]
theorem preorder_hom.prod.diag_coe {α : Type u_1} [preorder α] (x : α) :
def preorder_hom.prod.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {α' : Type u_5} {β' : Type u_6} [preorder α'] [preorder β'] (f : α →ₘ β) (f' : α' →ₘ β') :
α × α' →ₘ β × β'

The prod.map function, as a monotone function.

Equations
@[simp]
theorem preorder_hom.prod.map_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {α' : Type u_5} {β' : Type u_6} [preorder α'] [preorder β'] (f : α →ₘ β) (f' : α' →ₘ β') (x : α × α') :
@[simp]
theorem preorder_hom.prod.fst_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (c : α × β) :
def preorder_hom.prod.fst {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α × β →ₘ α

The prod.fst projection, as a monotone function.

Equations
@[simp]
theorem preorder_hom.prod.snd_coe {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (c : α × β) :
def preorder_hom.prod.snd {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] :
α × β →ₘ β

The prod.snd projection, as a monotone function.

Equations
def preorder_hom.prod.zip {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) :
α →ₘ β × γ

The prod constructor, as a monotone function.

Equations
@[simp]
theorem preorder_hom.prod.zip_coe {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) (ᾰ : α) :
(preorder_hom.prod.zip f g) = (f ᾰ, g ᾰ)
def preorder_hom.bind {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →ₘ roption β) (g : α →ₘ β → roption γ) :

roption.bind as a monotone function

Equations
@[simp]
theorem preorder_hom.bind_coe {α : Type u_1} [preorder α] {β γ : Type u_2} (f : α →ₘ roption β) (g : α →ₘ β → roption γ) (x : α) :
(f.bind g) x = f x >>= g x
def omega_complete_partial_order.chain (α : Type u) [preorder α] :
Type u

A chain is a monotonically increasing sequence.

See the definition on page 114 of [Gun92].

Equations
@[instance]
Equations

map function for chain

Equations
@[simp]
theorem omega_complete_partial_order.chain.map_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) (f : α →ₘ β) :
(c.map f) = f c
theorem omega_complete_partial_order.chain.mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} (x : α) :
x cf x c.map f
theorem omega_complete_partial_order.chain.exists_of_mem_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} {b : β} :
b c.map f(∃ (a : α), a c f a = b)
theorem omega_complete_partial_order.chain.mem_map_iff {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} {b : β} :
b c.map f ∃ (a : α), a c f a = b
theorem omega_complete_partial_order.chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [preorder α] [preorder β] [preorder γ] (c : omega_complete_partial_order.chain α) {f : α →ₘ β} (g : β →ₘ γ) :
(c.map f).map g = c.map (g.comp f)
theorem omega_complete_partial_order.chain.map_le_map {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) {f g : α →ₘ β} (h : f g) :
c.map f c.map g

chain.zip pairs up the elements of two chains that have the same index

Equations
@[simp]
theorem omega_complete_partial_order.chain.zip_coe {α : Type u} {β : Type v} [preorder α] [preorder β] (c₀ : omega_complete_partial_order.chain α) (c₁ : omega_complete_partial_order.chain β) (ᾰ : ) :
(c₀.zip c₁) = (c₀ ᾰ, c₁ ᾰ)
@[class]
structure omega_complete_partial_order (α : Type u_1) :
Type u_1

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

See the definition on page 114 of [Gun92].

Instances
def omega_complete_partial_order.lift {α : Type u} {β : Type v} [omega_complete_partial_order α] [partial_order β] (f : β →ₘ α) (ωSup₀ : omega_complete_partial_order.chain β → β) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : omega_complete_partial_order.chain β), f (ωSup₀ c) = omega_complete_partial_order.ωSup (c.map f)) :

Transfer a omega_complete_partial_order on β to a omega_complete_partial_order on α using a strictly monotone function f : β →ₘ α, a definition of ωSup and a proof that f is continuous with regard to the provided ωSup and the ωCPO on α.

Equations
def omega_complete_partial_order.subtype {α : Type u_1} [omega_complete_partial_order α] (p : α → Prop) (hp : ∀ (c : omega_complete_partial_order.chain α), (∀ (i : α), i cp i)p (omega_complete_partial_order.ωSup c)) :

A subset p : α → Prop of the type closed under ωSup induces an omega_complete_partial_order on the subtype {a : α // p a}.

Equations

A monotone function f : α →ₘ β is continuous if it distributes over ωSup.

In order to distinguish it from the (more commonly used) continuity from topology (see topology/basic.lean), the present definition is often referred to as "Scott-continuity" (referring to Dana Scott). It corresponds to continuity in Scott topological spaces (not defined here).

Equations
def omega_complete_partial_order.continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) :
Prop

continuous' f asserts that f is both monotone and continuous.

Equations
theorem roption.eq_of_chain {α : Type u} {c : omega_complete_partial_order.chain (roption α)} {a b : α} (ha : roption.some a c) (hb : roption.some b c) :
a = b

The (noncomputable) ωSup definition for the ω-CPO structure on roption α.

Equations
@[simp]
theorem pi.monotone_apply_coe {α : Type u_1} {β : α → Type u_2} [Π (a : α), partial_order (β a)] (a : α) (f : Π (a : α), β a) :
def pi.monotone_apply {α : Type u_1} {β : α → Type u_2} [Π (a : α), partial_order (β a)] (a : α) :
(Π (a : α), β a) →ₘ β a

Function application λ f, f a is monotone with respect to f for fixed a.

Equations
@[instance]
def pi.omega_complete_partial_order {α : Type u_1} {β : α → Type u_2} [Π (a : α), omega_complete_partial_order (β a)] :
omega_complete_partial_order (Π (a : α), β a)
Equations
theorem pi.omega_complete_partial_order.flip₁_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : Π (x : α), γ → β x) (a : α) (hf : omega_complete_partial_order.continuous' (λ (x : γ) (y : α), f y x)) :
theorem pi.omega_complete_partial_order.flip₂_continuous' {α : Type u_1} {β : α → Type u_2} {γ : Type u_3} [Π (x : α), omega_complete_partial_order (β x)] [omega_complete_partial_order γ] (f : γ → Π (x : α), β x) (hf : ∀ (x : α), omega_complete_partial_order.continuous' (λ (g : γ), f g x)) :
@[instance]

Any complete lattice has an ω-CPO structure where the countable supremum is a special case of arbitrary suprema.

Equations
theorem complete_lattice.Sup_continuous' {α : Type u} {β : Type v} [omega_complete_partial_order α] [complete_lattice β] (s : set (α → β)) :

Function application λ f, f a (for fixed a) is a monotone function from the monotone function space α →ₘ β to β.

Equations

The "forgetful functor" from α →ₘ β to α → β that takes the underlying function, is monotone.

Equations
@[instance]
Equations
structure omega_complete_partial_order.continuous_hom (α : Type u) (β : Type v) [omega_complete_partial_order α] [omega_complete_partial_order β] :
Type (max u v)

A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of preorder_hom.continuous.

theorem omega_complete_partial_order.continuous_hom.congr_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] {f g : α →𝒄 β} (h : f = g) (x : α) :
f x = g x
theorem omega_complete_partial_order.continuous_hom.congr_arg {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α →𝒄 β) {x y : α} (h : x = y) :
f x = f y
def omega_complete_partial_order.continuous_hom.of_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (g : α →𝒄 β) (h : f = g) :
α →𝒄 β

Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.of_fun_to_fun {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f : α → β) (g : α →𝒄 β) (h : f = g) (ᾰ : α) :

Construct a continuous function from a monotone function with a proof of continuity.

Equations

The identity as a continuous function.

Equations
def omega_complete_partial_order.continuous_hom.comp {α : Type u} {β : Type v} {γ : Type u_3} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) (g : α →𝒄 β) :
α →𝒄 γ

The composition of continuous functions.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_to_fun {α : Type u} {β : Type v} {γ : Type u_3} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] (f : β →𝒄 γ) (g : α →𝒄 β) (ᾰ : α) :
(f.comp g) = f (g ᾰ)
@[ext]
theorem omega_complete_partial_order.continuous_hom.ext {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) (h : ∀ (x : α), f x = g x) :
f = g
@[simp]
theorem omega_complete_partial_order.continuous_hom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} [omega_complete_partial_order α] [omega_complete_partial_order β] [omega_complete_partial_order γ] [omega_complete_partial_order φ] (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) :
f.comp (g.comp h) = (f.comp g).comp h
@[simp]
theorem omega_complete_partial_order.continuous_hom.coe_apply {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (a : α) (f : α →𝒄 β) :
f a = f a

The application of continuous functions as a monotone function.

(It would make sense to make it a continuous function, but we are currently constructing a omega_complete_partial_order instance for α →𝒄 β, and we cannot use it as the domain or image of a continuous function before we do.)

Equations

The map from continuous functions to monotone functions is itself a monotone function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.forall_forall_merge {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c₀ : omega_complete_partial_order.chain →𝒄 β)) (c₁ : omega_complete_partial_order.chain α) (z : β) :
(∀ (i j : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z

When proving that a chain of applications is below a bound z, it suffices to consider the functions and values being selected from the same index in the chains.

This lemma is more specific than necessary, i.e. c₀ only needs to be a chain of monotone functions, but it is only used with continuous functions.

@[simp]
theorem omega_complete_partial_order.continuous_hom.forall_forall_merge' {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (c₀ : omega_complete_partial_order.chain →𝒄 β)) (c₁ : omega_complete_partial_order.chain α) (z : β) :
(∀ (j i : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z
@[instance]
Equations
def omega_complete_partial_order.continuous_hom.flip {β : Type v} {γ : Type u_3} [omega_complete_partial_order β] [omega_complete_partial_order γ] {α : Type u_1} (f : α → β →𝒄 γ) :
β →𝒄 α → γ

A family of continuous functions yields a continuous family of functions.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.flip_to_fun {β : Type v} {γ : Type u_3} [omega_complete_partial_order β] [omega_complete_partial_order γ] {α : Type u_1} (f : α → β →𝒄 γ) (x : β) (y : α) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.bind_to_fun {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α →𝒄 roption β) (g : α →𝒄 β → roption γ) (ᾰ : α) :
(f.bind g) = (f.bind g)
def omega_complete_partial_order.continuous_hom.bind {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α →𝒄 roption β) (g : α →𝒄 β → roption γ) :

roption.bind as a continuous function.

Equations
@[simp]
theorem omega_complete_partial_order.continuous_hom.map_to_fun {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : β → γ) (g : α →𝒄 roption β) (x : α) :
@[simp]
theorem omega_complete_partial_order.continuous_hom.seq_to_fun {α : Type u} [omega_complete_partial_order α] {β γ : Type v} (f : α →𝒄 roption (β → γ)) (g : α →𝒄 roption β) (x : α) :
(f.seq g) x = f x <*> g x