{-# OPTIONS --type-in-type --no-positivity-check #-}
open import NeilPrelude
open import Properties
open import Extensionality
open import SubSet
module CPO where
infix 3 _≣_ _⊑_ _⊑⊥_
infixr 4 _$_
infixr 10 _⇒_
infixr 11 _⊕_
infixr 12 _⊗_ _,_
data _-⊥ (A : Set) : Set where
bot : A -⊥
val : A → A -⊥
data _⊑⊥_ {A : Set} : Rel (A -⊥) where
⊑⊥-refl : Reflexive _⊑⊥_
⊑⊥-botval : {a : A} → bot ⊑⊥ val a
⊑⊥-bot : {A : Set} → Initial bot (_⊑⊥_ {A})
⊑⊥-bot {_} {bot} = ⊑⊥-refl
⊑⊥-bot {_} {val _} = ⊑⊥-botval
⊑⊥-trans : {A : Set} → Transitive {A -⊥} _⊑⊥_
⊑⊥-trans ⊑⊥-refl ⊑⊥-refl = ⊑⊥-refl
⊑⊥-trans ⊑⊥-refl ⊑⊥-botval = ⊑⊥-botval
⊑⊥-trans ⊑⊥-botval ⊑⊥-refl = ⊑⊥-botval
⊑⊥-antisym : {A : Set} → Antisymmetric {A -⊥} _⊑⊥_
⊑⊥-antisym ⊑⊥-refl ⊑⊥-refl = refl
⊑⊥-antisym ⊑⊥-botval ()
data Type : Set where
Base : Set → Type
_⊗_ : Type → Type → Type
_⇒_ : Type → Type → Type
_⊕_ : Type → Type → Type
mutual
data CPO : (τ : Type) → Set where
base : {A : Set} → A -⊥ → CPO (Base A)
_,_ : {σ τ : Type} → CPO σ → CPO τ → CPO (σ ⊗ τ)
fun : {σ τ : Type} → (f : CPO σ → CPO τ) → Continuous f → CPO (σ ⇒ τ)
inl : {σ τ : Type} → CPO σ → CPO (σ ⊕ τ)
inr : {σ τ : Type} → CPO τ → CPO (σ ⊕ τ)
bot : {σ τ : Type} → CPO (σ ⊕ τ)
data _⊑_ : {τ : Type} → Rel (CPO τ) where
⊑-base : {A : Set} → {a₁ a₂ : A -⊥} → a₁ ⊑⊥ a₂ → base a₁ ⊑ base a₂
⊑-prod : {σ τ : Type} → {x₁ x₂ : CPO σ} → {y₁ y₂ : CPO τ} → x₁ ⊑ x₂ → y₁ ⊑ y₂ → (x₁ , y₁) ⊑ (x₂ , y₂)
⊑-fun : {σ τ : Type} → {f g : CPO σ → CPO τ} → {cf : Continuous f} → {cg : Continuous g} → ({x : CPO σ} → f x ⊑ g x) → fun f cf ⊑ fun g cg
⊑-inl : {σ τ : Type} → {x₁ x₂ : CPO σ} → x₁ ⊑ x₂ → inl {σ} {τ} x₁ ⊑ inl x₂
⊑-inr : {σ τ : Type} → {y₁ y₂ : CPO τ} → y₁ ⊑ y₂ → inr {σ} {τ} y₁ ⊑ inr y₂
⊑-sum : {σ τ : Type} → {xy : CPO (σ ⊕ τ)} → bot ⊑ xy
Monotonic : {σ τ : Type} → (CPO σ → CPO τ) → Set
Monotonic {σ} f = {x y : CPO σ} → x ⊑ y → f x ⊑ f y
Chain : Type → Set
Chain τ = SubSet (CPO τ) × CPO τ
_∈_ : {τ : Type} → CPO τ → Chain τ → Set
x ∈ (P , _) = P x
⨆ : {τ : Type} → Chain τ → CPO τ
⨆ (_ , ⨆X) = ⨆X
IsTotalOrder : {τ : Type} → Chain τ → Set
IsTotalOrder {τ} X = (x₁ x₂ : CPO τ) → x₁ ∈ X → x₂ ∈ X → (x₁ ⊑ x₂) ⊎ (x₂ ⊑ x₁)
IsUB : {τ : Type} → Chain τ → Set
IsUB {τ} X = (x : CPO τ) → x ∈ X → x ⊑ ⨆ X
IsLUB : {τ : Type} → Chain τ → Set
IsLUB {τ} X = (y : CPO τ) → ((x : CPO τ) → x ∈ X → x ⊑ y) → ⨆ X ⊑ y
IsChain : {τ : Type} → Chain τ → Set
IsChain X = IsTotalOrder X × IsUB X × IsLUB X
IsNonEmptyChain : {τ : Type} → Chain τ → Set
IsNonEmptyChain {τ} (P , ⨆X) = IsChain (P , ⨆X) × Σ (CPO τ) P
chainImage' : {σ τ : Type} → (CPO σ → CPO τ) → Chain σ → Chain τ
chainImage' f (P , ⨆X) = SubImage f P , f ⨆X
PreservesLUB : {σ τ : Type} → (CPO σ → CPO τ) → Set
PreservesLUB {σ} f = ((X : Chain σ) → IsNonEmptyChain X → IsLUB (chainImage' f X))
Continuous : {σ τ : Type} → (f : CPO σ → CPO τ) → Set
Continuous {σ} f = Monotonic f × PreservesLUB f
_$_ : {σ τ : Type} → CPO (σ ⇒ τ) → CPO σ → CPO τ
fun f _ $ x = f x
continuous : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → Continuous (_$_ f)
continuous (fun f cf) = cf
monotonic : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → Monotonic (_$_ f)
monotonic (fun f (mf , _)) = mf
preservesLUB : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → PreservesLUB (_$_ f)
preservesLUB (fun f (_ , plubf)) = plubf
chainImage : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → Chain σ → Chain τ
chainImage f = chainImage' (_$_ f)
monotonic⇒ImageTotalOrder : {σ τ : Type} → (f : CPO σ → CPO τ) → Monotonic f → (X : Chain σ) → IsTotalOrder X → IsTotalOrder (chainImage' f X)
monotonic⇒ImageTotalOrder f monf (P , ⨆X) tot ._ ._ (x₁ , Px₁ , refl) (x₂ , Px₂ , refl) with tot x₁ x₂ Px₁ Px₂
... | inl lt = inl (monf lt)
... | inr gt = inr (monf gt)
monotonic⇒ImageUB : {σ τ : Type} → (f : CPO σ → CPO τ) → Monotonic f → (X : Chain σ) → IsUB X → IsUB (chainImage' f X)
monotonic⇒ImageUB f monf (P , ⨆X) ub ._ (x , Px , refl) = monf (ub x Px)
imageIsTotalOrder : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → IsTotalOrder X → IsTotalOrder (chainImage f X)
imageIsTotalOrder (fun f (monf , _)) = monotonic⇒ImageTotalOrder f monf
imageIsUB : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → IsUB X → IsUB (chainImage f X)
imageIsUB (fun f (monf , _)) = monotonic⇒ImageUB f monf
imageIsNonEmptyChain : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → IsNonEmptyChain X → IsNonEmptyChain (chainImage f X)
imageIsNonEmptyChain (fun f conf) X ((tot , ub , lub) , x , Px) = (imageIsTotalOrder (fun f conf) X tot , imageIsUB (fun f conf) X ub , preservesLUB (fun f conf) X ((tot , ub , lub) , x , Px)) , (f x , (x , (Px , refl)))
ultp' : {A : Set} → {a₁ a₂ : A -⊥} → (p q : a₁ ⊑⊥ a₂) → p ≡ q
ultp' ⊑⊥-refl ⊑⊥-refl = refl
ultp' ⊑⊥-botval ⊑⊥-botval = refl
ultp : {{_ : Extensionality}} → {τ : Type} → {x y : CPO τ} → (p q : x ⊑ y) → p ≡ q
ultp (⊑-base p) (⊑-base q) = cong ⊑-base (ultp' p q)
ultp (⊑-prod p₁ q₁) (⊑-prod p₂ q₂) = cong2 ⊑-prod (ultp p₁ p₂) (ultp q₁ q₂)
ultp (⊑-fun p) (⊑-fun q) = cong ⊑-fun (ext-implicit (ultp p q))
ultp (⊑-inl p) (⊑-inl q) = cong ⊑-inl (ultp p q)
ultp (⊑-inr p) (⊑-inr q) = cong ⊑-inr (ultp p q)
ultp ⊑-sum ⊑-sum = refl
ump : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO σ → CPO τ) → (p q : Monotonic f) → _≡_ {_} {Monotonic f} p q
ump {σ} f p q = ext-implicit (ext-implicit (ext (λ lt → ultp (p lt) (q lt))))
ulubp : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO σ → CPO τ) → (p q : PreservesLUB f) → _≡_ {_} {PreservesLUB f} p q
ulubp f p q = ext (λ X → ext (λ pX → ext (λ y → ext (λ ubY → ultp (p X pX y ubY) (q X pX y ubY)))))
ucp : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO σ → CPO τ) → (p q : Continuous f) → _≡_ {_} {Continuous f} p q
ucp {σ} f (monp , conp) (monq , conq) = ×-cong (ump f monp monq) (ulubp f conp conq)
injective-$ : {{_ : Extensionality}} → {σ τ : Type} → Injective {CPO (σ ⇒ τ)} _$_
injective-$ {_} {_} {fun f cf} {fun .f cg} refl rewrite ucp f cf cg = refl
⊑-refl : {τ : Type} → Reflexive (_⊑_ {τ})
⊑-refl {Base _} {base _} = ⊑-base ⊑⊥-refl
⊑-refl {σ ⊗ τ} {_ , _} = ⊑-prod ⊑-refl ⊑-refl
⊑-refl {σ ⇒ τ} {fun _ _} = ⊑-fun ⊑-refl
⊑-refl {σ ⊕ τ} {inl _} = ⊑-inl ⊑-refl
⊑-refl {σ ⊕ τ} {inr _} = ⊑-inr ⊑-refl
⊑-refl {σ ⊕ τ} {bot} = ⊑-sum
⊑-eq : {τ : Type} → {x y : CPO τ} → x ≡ y → x ⊑ y
⊑-eq refl = ⊑-refl
⊑-trans : {τ : Type} → Transitive {CPO τ} _⊑_
⊑-trans (⊑-base {_} {bot} _) (⊑-base _) = ⊑-base ⊑⊥-bot
⊑-trans (⊑-base {_} {val _} ⊑⊥-refl) q = q
⊑-trans (⊑-prod a₁ a₂) (⊑-prod b₁ b₂) = ⊑-prod (⊑-trans a₁ b₁) (⊑-trans a₂ b₂)
⊑-trans (⊑-fun p) (⊑-fun q) = ⊑-fun (⊑-trans p q)
⊑-trans (⊑-inl p) (⊑-inl q) = ⊑-inl (⊑-trans p q)
⊑-trans (⊑-inr p) (⊑-inr q) = ⊑-inr (⊑-trans p q)
⊑-trans ⊑-sum _ = ⊑-sum
⊑-split : {σ τ : Type} → {x₁ x₂ : CPO σ} → {y₁ y₂ : CPO τ} → (x₁ , y₁) ⊑ (x₂ , y₂) → x₁ ⊑ x₂ × y₁ ⊑ y₂
⊑-split (⊑-prod lt₁ lt₂) = lt₁ , lt₂
⊑-antisym : {{_ : Extensionality}} → {τ : Type} → Antisymmetric {CPO τ} _⊑_
⊑-antisym (⊑-base p) (⊑-base q) = cong base (⊑⊥-antisym p q)
⊑-antisym (⊑-prod a₁ b₁) (⊑-prod a₂ b₂) = cong2 _,_ (⊑-antisym a₁ a₂) (⊑-antisym b₁ b₂)
⊑-antisym (⊑-fun p) (⊑-fun q) = injective-$ (ext' (⊑-antisym p q))
⊑-antisym (⊑-inl p) (⊑-inl q) = cong inl (⊑-antisym p q)
⊑-antisym (⊑-inr p) (⊑-inr q) = cong inr (⊑-antisym p q)
⊑-antisym ⊑-sum ⊑-sum = refl
mutual
⊥ : {τ : Type} → CPO τ
⊥ {Base _} = base bot
⊥ {_ ⊗ _} = ⊥ , ⊥
⊥ {_ ⇒ _} = fun (λ _ → ⊥) continuous-⊥-fun
⊥ {_ ⊕ _} = bot
⊑-bot : {τ : Type} → Initial (⊥ {τ}) _⊑_
⊑-bot {Base _} {base _} = ⊑-base ⊑⊥-bot
⊑-bot {_ ⊗ _} {_ , _} = ⊑-prod ⊑-bot ⊑-bot
⊑-bot {σ ⇒ τ} {fun f cf} = ⊑-fun {σ} {τ} {(λ _ → ⊥)} {f} ⊑-bot
⊑-bot {_ ⊕ _} { _ } = ⊑-sum
abstract
monotonic-⊥-fun : {σ τ : Type} → Monotonic {σ} {τ} (λ _ → ⊥)
monotonic-⊥-fun _ = ⊑-refl
continuous-⊥-fun : {σ τ : Type} → Continuous {σ} {τ} (λ _ → ⊥)
continuous-⊥-fun {σ} {τ} = monotonic-⊥-fun , (λ _ _ _ _ → ⊑-bot)
emptyChain : {τ : Type} → Chain τ
emptyChain = (λ _ → False) , ⊥
splitChain : {σ τ : Type} → Chain (σ ⊗ τ) → Chain σ × Chain τ
splitChain {σ} {τ} (P , ⨆X , ⨆Y) = ((λ x → Σ[ y ∶ CPO τ ] P (x , y)) , ⨆X) ,
((λ y → Σ[ x ∶ CPO σ ] P (x , y)) , ⨆Y)
fstChain : {σ τ : Type} → Chain (σ ⊗ τ) → Chain σ
fstChain = fst ∘ splitChain
sndChain : {σ τ : Type} → Chain (σ ⊗ τ) → Chain τ
sndChain = snd ∘ splitChain
uncurry-prop : {σ τ : Type} → {P : CPO (σ ⊗ τ) → Set} → ((x : CPO σ) → (y : CPO τ) → P (x , y)) → (xy : CPO (σ ⊗ τ)) → P xy
uncurry-prop f (x , y) = f x y
firstChain : {σ τ : Type} → CPO σ → Chain τ → Chain (σ ⊗ τ)
firstChain x (P , ⨆Y) = uncurry-prop (λ x' y → x ≡ x' × P y) , (x , ⨆Y)
secondChain : {σ τ : Type} → CPO τ → Chain σ → Chain (σ ⊗ τ)
secondChain y (P , ⨆X) = uncurry-prop (λ x y' → y ≡ y' × P x) , (⨆X , y)
singletonChain : {τ : Type} → CPO τ → Chain τ
singletonChain x = (λ x' → x' ≡ x) , x
_≣_ : {τ : Type} → Chain τ → Chain τ → Set
(P , ⨆X) ≣ (Q , ⨆Y) = SubSetEq P Q × (⨆X ≡ ⨆Y)
ChainComplete : {τ : Type} → (CPO τ → Set) → Set
ChainComplete {τ} P = (X : Chain τ) → IsNonEmptyChain X → ((x : CPO τ) → x ∈ X → P x) → P (⨆ X)
Strict : {σ τ : Type} → (g : CPO (σ ⇒ τ)) → Set
Strict g = g $ ⊥ ≡ ⊥
FixedPoint : {τ : Type} → (f : CPO (τ ⇒ τ)) → CPO τ → Set
FixedPoint f x = f $ x ≡ x
Functor : Set
Functor = Type → Type