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_to_fun (α : Type u_1) {β : Type u_2} [preorder α] [preorder β] (f : β) (a : α) :

def preorder_hom.const (α : Type u_1) {β : Type u_2} [preorder α] [preorder β] :
β → α →ₘ β

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_to_fun {α : Type u_1} [preorder α] (x : α) :

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

def preorder_hom.prod.map {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] {α' : Type u_5} {β' : Type u_6} [preorder α'] [preorder β'] :
→ₘ β)(α' →ₘ β')α × α' →ₘ β × β'

The prod.map function, as a monotone function.

Equations
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.fst_to_fun {α : Type u_1} {β : Type u_2} [preorder α] [preorder β] (c : α × β) :

@[simp]
theorem preorder_hom.prod.snd_to_fun {α : 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
@[simp]
theorem preorder_hom.prod.zip_to_fun {α : Type u_1} {β : Type u_2} {γ : Type u_3} [preorder α] [preorder β] [preorder γ] (f : α →ₘ β) (g : α →ₘ γ) (a : α) :

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

The prod constructor, as a monotone function.

Equations
def preorder_hom.bind {α : Type u_1} [preorder α] {β γ : Type u_2} :
→ₘ roption β)→ₘ β → roption γ)α →ₘ roption γ

roption.bind as a monotone function

Equations
@[simp]
theorem preorder_hom.bind_to_fun {α : 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 [gunter].

Equations
@[instance]

Equations

map function for chain

Equations
@[simp]
theorem omega_complete_partial_order.chain.map_to_fun {α : Type u} {β : Type v} [preorder α] [preorder β] (c : omega_complete_partial_order.chain α) (f : α →ₘ β) (a : ) :
(c.map f) a = (f c) a

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 : α →ₘ β} :
f gc.map f c.map g

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

Equations
@[class]
structure omega_complete_partial_order  :
Type u_1Type 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 [gunter].

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

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

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 β] :
(α → β) → 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 : α} :
roption.some a croption.some b ca = b

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

Equations
@[simp]
theorem pi.monotone_apply_to_fun {α : 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 : α) :

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

@[instance]

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

Equations

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 : α} :
x = yf 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 : α →𝒄 β) :
f = gα →𝒄 β

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

Equations
@[simp]

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 γ] :
→𝒄 γ)→𝒄 β)α →𝒄 γ

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 : α →𝒄 β) (a : α) :
(f.comp g) a = (f.comp g) a

@[ext]
theorem omega_complete_partial_order.continuous_hom.ext {α : Type u} {β : Type v} [omega_complete_partial_order α] [omega_complete_partial_order β] (f g : α →𝒄 β) :
(∀ (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} :
(α → β →𝒄 γ)β →𝒄 α → γ

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 γ) (a : α) :
(f.bind g) a = (f.bind g) a

def omega_complete_partial_order.continuous_hom.bind {α : Type u} [omega_complete_partial_order α] {β γ : Type v} :
→𝒄 roption β)→𝒄 β → roption γ)α →𝒄 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