{-# OPTIONS --type-in-type #-}
open import NeilPrelude
open import Extensionality
open import CPO
module CPOLemmas where
cpo-ext : {{_ : Extensionality}} → {σ τ : Type} → {f g : CPO (σ ⇒ τ)} → ((x : CPO σ) → (f $ x) ≡ (g $ x)) → f ≡ g
cpo-ext eq = injective-$ (ext eq)
cpo-ext' : {{_ : Extensionality}} → {σ τ : Type} → {f g : CPO (σ ⇒ τ)} → ({x : CPO σ} → (f $ x) ≡ (g $ x)) → f ≡ g
cpo-ext' eq = injective-$ (ext' eq)
cpo-func' : {σ τ : Type} → {f g : CPO (σ ⇒ τ)} → f ≡ g → ({x : CPO σ} → (f $ x) ≡ (g $ x))
cpo-func' refl = refl
cpo-func : {σ τ : Type} → {f g : CPO (σ ⇒ τ)} → f ≡ g → ((x : CPO σ) → (f $ x) ≡ (g $ x))
cpo-func refl _ = refl
infixr 1 _⊑⟨_⟩_
infix 2 _⊑-QED
_⊑⟨_⟩_ : {τ : Type} → {y z : CPO τ} → (x : CPO τ) → x ⊑ y → y ⊑ z → x ⊑ z
_⊑⟨_⟩_ _ = ⊑-trans
_⊑-QED : {τ : Type} → (x : CPO τ) → x ⊑ x
_⊑-QED _ = ⊑-refl
≡→⊑ : {τ : Type} → {x y : CPO τ} → x ≡ y → x ⊑ y
≡→⊑ refl = ⊑-refl
⊑-, : {σ τ : Type} → {x₁ x₂ : CPO σ} → {y₁ y₂ : CPO τ} → (x₁ , y₁) ⊑ (x₂ , y₂) → x₁ ⊑ x₂ × y₁ ⊑ y₂
⊑-, (⊑-prod p q) = p , q
⊑-cong : {σ τ : Type} → (f : CPO σ → CPO τ) → {x y : CPO σ} → x ≡ y → f x ⊑ f y
⊑-cong f refl = ⊑-refl
⊑-$ : {σ τ : Type} → {f g : CPO (σ ⇒ τ)} → {x : CPO σ} → f ⊑ g → (f $ x) ⊑ (g $ x)
⊑-$ (⊑-fun p) = p
⊑-app : {σ τ : Type} → {f g : CPO (σ ⇒ τ)} → {x y : CPO σ} → f ⊑ g → x ⊑ y → (f $ x) ⊑ (g $ y)
⊑-app {_} {_} {f} {g} {x} {y} p q =
f $ x
⊑⟨ monotonic f q ⟩
f $ y
⊑⟨ ⊑-$ p ⟩
g $ y
⊑-QED
↔-⊑ : {τ : Type} → {a b c d : CPO τ} → (a ≡ c) → (b ≡ d) → (a ⊑ b) ↔ (c ⊑ d)
↔-⊑ refl refl = id , id
↔-⊑L : {τ : Type} → {a b d : CPO τ} → (b ≡ d) → (a ⊑ b) ↔ (a ⊑ d)
↔-⊑L refl = id , id
↔-⊑R : {τ : Type} → {a b c : CPO τ} → (a ≡ c) → (a ⊑ b) ↔ (c ⊑ b)
↔-⊑R refl = id , id
⊑-⊥-eq : {{_ : Extensionality}} → {τ : Type} → {a : CPO τ} → a ⊑ ⊥ → a ≡ ⊥
⊑-⊥-eq lt = ⊑-antisym lt ⊑-bot
emptyIsChain : {τ : Type} → IsChain {τ} emptyChain
emptyIsChain = (λ _ _ ()) , (λ _ ()) , (λ _ _ → ⊑-bot)
fstIsTotalOrder : {σ τ : Type} → (XY : Chain (σ ⊗ τ)) → IsTotalOrder XY → IsTotalOrder (fstChain XY)
fstIsTotalOrder (P , ⨆X , ⨆Y) totXY x₁ x₂ (y₁ , Pxy₁) (y₂ , Pxy₂) with totXY (x₁ , y₁) (x₂ , y₂) Pxy₁ Pxy₂
... | inl (⊑-prod lt₁ lt₂) = inl lt₁
... | inr (⊑-prod lt₁ lt₂) = inr lt₁
sndIsTotalOrder : {σ τ : Type} → (XY : Chain (σ ⊗ τ)) → IsTotalOrder XY → IsTotalOrder (sndChain XY)
sndIsTotalOrder (P , ⨆X , ⨆Y) totXY y₁ y₂ (x₁ , Pxy₁) (x₂ , Pxy₂) with totXY (x₁ , y₁) (x₂ , y₂) Pxy₁ Pxy₂
... | inl (⊑-prod lt₁ lt₂) = inl lt₂
... | inr (⊑-prod lt₁ lt₂) = inr lt₂
fstIsUB : {σ τ : Type} → (XY : Chain (σ ⊗ τ)) → IsUB XY → IsUB (fstChain XY)
fstIsUB (P , ⨆X , ⨆Y) ubXY x (y , Pxy) with ubXY (x , y) Pxy
... | ⊑-prod lt₁ lt₂ = lt₁
sndIsUB : {σ τ : Type} → (XY : Chain (σ ⊗ τ)) → IsUB XY → IsUB (sndChain XY)
sndIsUB (P , ⨆X , ⨆Y) ubXY y (x , Pxy) with ubXY (x , y) Pxy
... | ⊑-prod lt₁ lt₂ = lt₂
fstIsLUB : {σ τ : Type} → (XY : Chain (σ ⊗ τ)) → IsChain XY → IsLUB (fstChain XY)
fstIsLUB {σ} {τ} (P , ⨆X , ⨆Y) (totXY , ubXY , lubXY) x₁ least = fst (⊑-split (lubXY (x₁ , ⨆Y) fstLUBaux))
where
fstLUBaux : (xy : CPO (σ ⊗ τ)) → P xy → xy ⊑ (x₁ , ⨆Y)
fstLUBaux (x , y) Pxy = ⊑-prod (least x (y , Pxy)) (sndIsUB (P , ⨆X , ⨆Y) ubXY y (x , Pxy))
sndIsLUB : {σ τ : Type} → (XY : Chain (σ ⊗ τ)) → IsChain XY → IsLUB (sndChain XY)
sndIsLUB {σ} {τ} (P , ⨆X , ⨆Y) (totXY , ubXY , lubXY) y₁ least = snd (⊑-split (lubXY (⨆X , y₁) sndLUBaux))
where
sndLUBaux : (xy : CPO (σ ⊗ τ)) → P xy → xy ⊑ (⨆X , y₁)
sndLUBaux (x , y) Pxy = ⊑-prod (fstIsUB (P , ⨆X , ⨆Y) ubXY x (y , Pxy)) (least y (x , Pxy))
fstIsChain : {σ τ : Type} → (X : Chain (σ ⊗ τ)) → IsChain X → IsChain (fstChain X)
fstIsChain X (totX , ubX , lubX) = fstIsTotalOrder X totX , fstIsUB X ubX , fstIsLUB X (totX , ubX , lubX)
sndIsChain : {σ τ : Type} → (X : Chain (σ ⊗ τ)) → IsChain X → IsChain (sndChain X)
sndIsChain X (totX , ubX , lubX) = sndIsTotalOrder X totX , sndIsUB X ubX , sndIsLUB X (totX , ubX , lubX)
fstIsNonEmptyChain : {σ τ : Type} → (X : Chain (σ ⊗ τ)) → IsNonEmptyChain X → IsNonEmptyChain (fstChain X)
fstIsNonEmptyChain (P , ⨆X , ⨆Y) (pXY , (x , y) , Pxy) = fstIsChain (P , ⨆X , ⨆Y) pXY , x , y , Pxy
sndIsNonEmptyChain : {σ τ : Type} → (X : Chain (σ ⊗ τ)) → IsNonEmptyChain X → IsNonEmptyChain (sndChain X)
sndIsNonEmptyChain (P , ⨆X , ⨆Y) (pXY , (x , y) , Pxy) = sndIsChain (P , ⨆X , ⨆Y) pXY , y , x , Pxy
firstIsTotalOrder : {σ τ : Type} → (x : CPO σ) → (Y : Chain τ) → IsTotalOrder Y → IsTotalOrder (firstChain x Y)
firstIsTotalOrder x Y totY (.x , y₁) (.x , y₂) (refl , Py₁) (refl , Py₂) with totY y₁ y₂ Py₁ Py₂
... | inl lt = inl (⊑-prod ⊑-refl lt)
... | inr lt = inr (⊑-prod ⊑-refl lt)
secondIsTotalOrder : {σ τ : Type} → (y : CPO τ) → (X : Chain σ) → IsTotalOrder X → IsTotalOrder (secondChain y X)
secondIsTotalOrder y X totX (x₁ , .y) (x₂ , .y) (refl , Px₁) (refl , Px₂) with totX x₁ x₂ Px₁ Px₂
... | inl lt = inl (⊑-prod lt ⊑-refl)
... | inr lt = inr (⊑-prod lt ⊑-refl)
firstIsUB : {σ τ : Type} → (x : CPO σ) → (Y : Chain τ) → IsUB Y → IsUB (firstChain x Y)
firstIsUB x Y ubY (.x , y) (refl , Py) = ⊑-prod ⊑-refl (ubY y Py)
secondIsUB : {σ τ : Type} → (y : CPO τ) → (X : Chain σ) → IsUB X → IsUB (secondChain y X)
secondIsUB y X ubX (x , .y) (refl , Px) = ⊑-prod (ubX x Px) ⊑-refl
firstIsLUB : {σ τ : Type} → (x : CPO σ) → (Y : Chain τ) → IsNonEmptyChain Y → IsLUB (firstChain x Y)
firstIsLUB x Y ((_ , ubY , lubY) , y₀ , Py₀) (x' , y) ub = ⊑-prod (fst (⊑-split (ub (x , y₀) (refl , Py₀)))) (lubY y (λ y' Py' → snd (⊑-split (ub (x , y') (refl , Py')))))
secondIsLUB : {σ τ : Type} → (y : CPO τ) → (X : Chain σ) → IsNonEmptyChain X → IsLUB (secondChain y X)
secondIsLUB y X ((_ , ubX , lubX) , x₀ , Px₀) (x , y') ub = ⊑-prod (lubX x (λ x' Px' → fst (⊑-split (ub (x' , y) (refl , Px'))))) (snd (⊑-split (ub (x₀ , y) (refl , Px₀))))
firstIsNonEmptyChain : {σ τ : Type} → (x : CPO σ) → (Y : Chain τ) → IsNonEmptyChain Y → IsNonEmptyChain (firstChain x Y)
firstIsNonEmptyChain x Y ((totY , ubY , lubY) , y , Py) = (firstIsTotalOrder x Y totY , firstIsUB x Y ubY , firstIsLUB x Y ((totY , ubY , lubY) , y , Py)) , (x , y) , refl , Py
secondIsNonEmptyChain : {σ τ : Type} → (y : CPO τ) → (X : Chain σ) → IsNonEmptyChain X → IsNonEmptyChain (secondChain y X)
secondIsNonEmptyChain y X ((totX , ubX , lubX) , x , Px) = (secondIsTotalOrder y X totX , secondIsUB y X ubX , secondIsLUB y X ((totX , ubX , lubX) , x , Px)) , (x , y) , refl , Px
singletonIsNonEmptyChain : {τ : Type} → (x : CPO τ) → IsNonEmptyChain (singletonChain x)
singletonIsNonEmptyChain x = ((λ x₁ x₂ eq₁ eq₂ → inl (⊑-eq (trans eq₁ (sym eq₂)))) , (λ x' → ⊑-eq) , (λ x' p → p x refl)) , (x , refl)
unpair : {σ τ : Type} → CPO (σ ⊗ τ) → CPO σ × CPO τ
unpair (x , y) = (x , y)
lem-products : {σ τ : Type} → {Q : CPO (σ ⊗ τ) → Set} → ((x : CPO σ) → (y : CPO τ) → Q (x , y)) ↔ ((xy : CPO (σ ⊗ τ)) → Q xy)
lem-products {σ} {τ} {Q} = uncurry-prop , (λ Q x y → Q (x , y))
continuity : {σ τ : Type} → (f : CPO (σ ⇒ τ)) → (X : Chain σ) → (p : IsNonEmptyChain X) → (y : CPO τ) → ((x : CPO σ) → x ∈ X → (f $ x) ⊑ y) ↔ ⨆ (chainImage f X) ⊑ y
continuity f X ((totX , ubX , lubX) , neX) y =
(λ leq → preservesLUB f X ((totX , ubX , lubX) , neX) y (λ y' → uncurry (λ x Px →
y'
⊑⟨ ≡→⊑ (sym (snd Px)) ⟩
f $ x
⊑⟨ leq x (fst Px) ⟩
y
⊑-QED)))
, (λ leq x Ps →
f $ x
⊑⟨ monotonic f (ubX x Ps) ⟩
f $ (⨆ X)
⊑⟨ leq ⟩
y
⊑-QED)
cong-≣-⨆ : {τ : Type} → (X Y : Chain τ) → X ≣ Y → ⨆ X ≡ ⨆ Y
cong-≣-⨆ (P , ⨆X) (Q , ⨆Y) = snd
⨆-unique : {{_ : Extensionality}} → {τ : Type} → (X Y : Chain τ) → IsChain X → IsChain Y → ((a : CPO τ) → a ∈ X ↔ a ∈ Y) → ⨆ X ≡ ⨆ Y
⨆-unique (P , ⨆X) (Q , ⨆Y) (totX , ubX , lubX) (totY , ubY , lubY) eq = ⊑-antisym (lubX ⨆Y (λ x Px → ubY x ( fst (eq x) Px)))
(lubY ⨆X (λ y Py → ubX y ( snd (eq y) Py)))
chain-ext : {{_ : Extensionality}} → {τ : Type} → (X Y : Chain τ) → IsChain X → IsChain Y → ((a : CPO τ) → a ∈ X ↔ a ∈ Y) ↔ (X ≣ Y)
chain-ext X Y pX pY = (λ eq → eq , ⨆-unique X Y pX pY eq) , fst
lem-image-eq : {σ τ : Type} → (f : CPO σ → CPO τ) → (XY : Chain (σ ⊗ τ)) → IsChain XY → ((x : CPO σ) → (y : CPO τ) → (x , y) ∈ XY → f x ≡ y) → (y : CPO τ) → y ∈ chainImage' f (fstChain XY) ↔ y ∈ (sndChain XY)
lem-image-eq {σ} {τ} f (P , ⨆X , ⨆Y) (totXY , ubXY , lubXY) feq y = second' (lem-image-eq-aux y) , second' (λ {x} Pxy → (y , Pxy) , feq x y Pxy)
where
lem-image-eq-aux : {x : CPO σ} → (y : CPO τ) → Σ (CPO τ) (λ y' → P (x , y')) × f x ≡ y → P (x , y)
lem-image-eq-aux {x} ._ ((y' , Pxy') , refl) with feq x y' Pxy'
lem-image-eq-aux {x} ._ ((._ , Pxy') , refl) | refl = Pxy'