Documentation

Mathlib.Order.OmegaCompletePartialOrder

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 OmegaCompletePartialOrder #

References #

@[simp]
theorem OrderHom.bind_coe {α : Type u_1} [inst : Preorder α] {β : Type u_2} {γ : Type u_2} (f : α →o Part β) (g : α →o βPart γ) (x : α) :
↑(OrderHom.bind f g) x = f x >>= g x
def OrderHom.bind {α : Type u_1} [inst : Preorder α] {β : Type u_2} {γ : Type u_2} (f : α →o Part β) (g : α →o βPart γ) :
α →o Part γ

Part.bind as a monotone function

Equations
  • OrderHom.bind f g = { toFun := fun x => f x >>= g x, monotone' := (_ : ∀ ⦃x y : α⦄, x y∀ (a : γ), a (fun x => f x >>= g x) xa (fun x => f x >>= g x) y) }

A chain is a monotone sequence.

See the definition on page 114 of [gunter1992].

Equations
Equations
  • OmegaCompletePartialOrder.Chain.instCoeFunChainForAllNat = { coe := OrderHom.toFun }
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • OmegaCompletePartialOrder.Chain.instMembershipChain = { mem := fun a c => i, a = c i }
Equations
  • OmegaCompletePartialOrder.Chain.instLEChain = { le := fun x y => ∀ (i : ), j, x i y j }
@[simp]
theorem OmegaCompletePartialOrder.Chain.map_coe {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (c : OmegaCompletePartialOrder.Chain α) (f : α →o β) :
theorem OmegaCompletePartialOrder.Chain.mem_map {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (x : α) :
theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} :
b OmegaCompletePartialOrder.Chain.map c fa, a c f a = b
theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} :
@[simp]
theorem OmegaCompletePartialOrder.Chain.zip_coe {α : Type u} {β : Type v} [inst : Preorder α] [inst : Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) (x : ) :
↑(OmegaCompletePartialOrder.Chain.zip c₀ c₁) x = (c₀ x, c₁ x)

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

Equations
class OmegaCompletePartialOrder (α : Type u_1) extends PartialOrder :
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 [gunter1992].

Instances
    def OmegaCompletePartialOrder.lift {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : PartialOrder β] (f : β →o α) (ωSup₀ : OmegaCompletePartialOrder.Chain ββ) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : OmegaCompletePartialOrder.Chain β), f (ωSup₀ c) = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.map c f)) :

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

    Equations
    • One or more equations did not get rendered due to their size.
    def OmegaCompletePartialOrder.subtype {α : Type u_1} [inst : OmegaCompletePartialOrder α] (p : αProp) (hp : (c : OmegaCompletePartialOrder.Chain α) → ((i : α) → i cp i) → p (OmegaCompletePartialOrder.ωSup c)) :

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

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

    A monotone function f : α →o β 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
    • One or more equations did not get rendered due to their size.
    def OmegaCompletePartialOrder.Continuous' {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : αβ) :

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

    Equations
    theorem Part.eq_of_chain {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} {b : α} (ha : Part.some a c) (hb : Part.some b c) :
    a = b
    noncomputable def Part.ωSup {α : Type u} (c : OmegaCompletePartialOrder.Chain (Part α)) :
    Part α

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

    Equations
    theorem Part.ωSup_eq_none {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} (h : ¬a, Part.some a c) :
    Part.ωSup c = Part.none
    Equations
    • One or more equations did not get rendered due to their size.
    instance Pi.instOmegaCompletePartialOrderForAll {α : Type u_1} {β : αType u_2} [inst : (a : α) → OmegaCompletePartialOrder (β a)] :
    OmegaCompletePartialOrder ((a : α) → β a)
    Equations
    • One or more equations did not get rendered due to their size.
    theorem Pi.OmegaCompletePartialOrder.flip₁_continuous' {α : Type u_2} {β : αType u_3} {γ : Type u_1} [inst : (x : α) → OmegaCompletePartialOrder (β x)] [inst : OmegaCompletePartialOrder γ] (f : (x : α) → γβ x) (a : α) (hf : OmegaCompletePartialOrder.Continuous' fun x y => f y x) :
    theorem Pi.OmegaCompletePartialOrder.flip₂_continuous' {α : Type u_3} {β : αType u_2} {γ : Type u_1} [inst : (x : α) → OmegaCompletePartialOrder (β x)] [inst : OmegaCompletePartialOrder γ] (f : γ(x : α) → β x) (hf : ∀ (x : α), OmegaCompletePartialOrder.Continuous' fun g => f g x) :
    def Prod.ωSup {α : Type u_1} {β : Type u_2} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (c : OmegaCompletePartialOrder.Chain (α × β)) :
    α × β

    The supremum of a chain in the product ω-CPO.

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

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

    Equations
    • One or more equations did not get rendered due to their size.
    theorem CompleteLattice.supᵢ_continuous {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : CompleteLattice β] {ι : Sort u_1} {f : ια →o β} (h : ∀ (i : ι), OmegaCompletePartialOrder.Continuous (f i)) :
    theorem CompleteLattice.supₛ_continuous' {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : CompleteLattice β] (s : Set (αβ)) (hc : ∀ (f : αβ), f sOmegaCompletePartialOrder.Continuous' f) :

    The ωSup operator for monotone functions.

    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    • One or more equations did not get rendered due to their size.
    structure OmegaCompletePartialOrder.ContinuousHom (α : Type u) (β : Type v) [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] extends OrderHom :
    Type (maxuv)

    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 OrderHom.continuous.

    Instances For

      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 OrderHom.continuous.

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

      todo: should we make this a OrderHomClass instead of a CoeFun?

      instance OmegaCompletePartialOrder.instCoeFunContinuousHomForAll (α : Type u) (β : Type v) [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] :
      CoeFun (α →𝒄 β) fun x => αβ
      Equations
      Equations
      • One or more equations did not get rendered due to their size.

      See Note [custom simps projection]. We specify this explicitly because we don't have a FunLike instance.

      Equations
      theorem OmegaCompletePartialOrder.ContinuousHom.congr_fun {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] {f : α →𝒄 β} {g : α →𝒄 β} (h : f = g) (x : α) :
      f.toOrderHom x = g.toOrderHom x
      theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : α →𝒄 β) {x : α} {y : α} (h : x = y) :
      f.toOrderHom x = f.toOrderHom y
      theorem OmegaCompletePartialOrder.ContinuousHom.apply_mono {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] {f : α →𝒄 β} {g : α →𝒄 β} {x : α} {y : α} (h₁ : f g) (h₂ : x y) :
      f.toOrderHom x g.toOrderHom y
      def OmegaCompletePartialOrder.ContinuousHom.ofFun {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : αβ) (g : α →𝒄 β) (h : f = g.toOrderHom) :
      α →𝒄 β

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

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

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.id_apply {α : Type u} [inst : OmegaCompletePartialOrder α] (a : α) :
      OmegaCompletePartialOrder.ContinuousHom.id.toOrderHom a = a

      The identity as a continuous function.

      Equations
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.comp_apply {α : Type u} {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] [inst : OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) :
      ∀ (a : α), (OmegaCompletePartialOrder.ContinuousHom.comp f g).toOrderHom a = f.toOrderHom (g.toOrderHom a)
      def OmegaCompletePartialOrder.ContinuousHom.comp {α : Type u} {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] [inst : OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) :
      α →𝒄 γ

      The composition of continuous functions.

      Equations
      • One or more equations did not get rendered due to their size.
      theorem OmegaCompletePartialOrder.ContinuousHom.ext {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) (h : ∀ (x : α), f.toOrderHom x = g.toOrderHom x) :
      f = g
      theorem OmegaCompletePartialOrder.ContinuousHom.coe_inj {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) (h : f.toOrderHom = g.toOrderHom) :
      f = g
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.comp_id {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder β] [inst : OmegaCompletePartialOrder γ] (f : β →𝒄 γ) :
      OmegaCompletePartialOrder.ContinuousHom.comp f OmegaCompletePartialOrder.ContinuousHom.id = f
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.id_comp {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder β] [inst : OmegaCompletePartialOrder γ] (f : β →𝒄 γ) :
      OmegaCompletePartialOrder.ContinuousHom.comp OmegaCompletePartialOrder.ContinuousHom.id f = f
      Equations
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.toMono_coe {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : α →𝒄 β) :
      OmegaCompletePartialOrder.ContinuousHom.toMono f = f.toOrderHom

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

      Equations
      • OmegaCompletePartialOrder.ContinuousHom.toMono = { toFun := fun f => f.toOrderHom, monotone' := (_ : ∀ (x x_1 : α →𝒄 β), x x_1x x_1) }
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β) :
      (∀ (i j : ), (c₀ i).toOrderHom (c₁ j) z) ∀ (i : ), (c₀ i).toOrderHom (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 OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge' {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β) :
      (∀ (j i : ), (c₀ i).toOrderHom (c₁ j) z) ∀ (i : ), (c₀ i).toOrderHom (c₁ i) z

      The ωSup operator for continuous functions, which takes the pointwise countable supremum of the functions in the ω-chain.

      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply {α : Type u} {β : Type v} [inst : OmegaCompletePartialOrder α] [inst : OmegaCompletePartialOrder β] (f : (α →𝒄 β) × α) :
      OmegaCompletePartialOrder.ContinuousHom.Prod.apply.toOrderHom f = f.fst.toOrderHom f.snd

      The application of continuous functions as a continuous function.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.flip_apply {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder β] [inst : OmegaCompletePartialOrder γ] {α : Type u_2} (f : αβ →𝒄 γ) (x : β) (y : α) :
      (OmegaCompletePartialOrder.ContinuousHom.flip f).toOrderHom x y = (f y).toOrderHom x
      def OmegaCompletePartialOrder.ContinuousHom.flip {β : Type v} {γ : Type u_1} [inst : OmegaCompletePartialOrder β] [inst : OmegaCompletePartialOrder γ] {α : Type u_2} (f : αβ →𝒄 γ) :
      β →𝒄 αγ

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

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.bind_apply_Dom {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) (x : α) :
      ((OmegaCompletePartialOrder.ContinuousHom.bind f g).toOrderHom x).Dom = h, (g.toOrderHom x (Part.get (f.toOrderHom x) h)).Dom
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.bind_apply_get {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) (x : α) (ha : h, ((fun b => g.toOrderHom x (Part.get (f.toOrderHom x) b)) h).Dom) :
      Part.get ((OmegaCompletePartialOrder.ContinuousHom.bind f g).toOrderHom x) ha = Part.get (g.toOrderHom x (Part.get (f.toOrderHom x) (_ : (f.toOrderHom x).Dom))) (_ : (g.toOrderHom x (Part.get (f.toOrderHom x) (_ : (f.toOrderHom x).Dom))).Dom)
      noncomputable def OmegaCompletePartialOrder.ContinuousHom.bind {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) :

      Part.bind as a continuous function.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.map_apply {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : βγ) (g : α →𝒄 Part β) (x : α) :
      (OmegaCompletePartialOrder.ContinuousHom.map f g).toOrderHom x = f <$> g.toOrderHom x
      noncomputable def OmegaCompletePartialOrder.ContinuousHom.map {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : βγ) (g : α →𝒄 Part β) :

      Part.map as a continuous function.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) (x : α) :
      (OmegaCompletePartialOrder.ContinuousHom.seq f g).toOrderHom x = Seq.seq (f.toOrderHom x) fun x => g.toOrderHom x
      noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u} [inst : OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) :

      Part.seq as a continuous function.

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