{-# OPTIONS --type-in-type #-}
open import NeilPrelude
open import Extensionality
open import CPO
open import CPOLemmas
module CPOFunctions where
infixr 80 _∙_
monotonic-id : {τ : Type} → Monotonic {τ} id
monotonic-id = id
preservesLUB-id : {τ : Type} → PreservesLUB {τ} id
preservesLUB-id (P , ⨆X) ((totX , ubX , lubX) , _) x ub = lubX x (λ y p → ub y (y , p , refl))
continuous-id : {τ : Type} → Continuous {τ} id
continuous-id = monotonic-id , preservesLUB-id
identity : {τ : Type} → CPO (τ ⇒ τ)
identity = fun id continuous-id
monotonic-const : {σ τ : Type} → (y : CPO τ) → Monotonic {σ} {τ} (λ _ → y)
monotonic-const y _ = ⊑-refl
preservesLUB-const : {σ τ : Type} → (y : CPO τ) → PreservesLUB {σ} (λ _ → y)
preservesLUB-const y (P , ⨆X) (_ , x , Px) y' q = q y (x , Px , refl)
continuous-const : {σ τ : Type} → (x : CPO τ) → Continuous {σ} {τ} (λ _ → x)
continuous-const {σ} {τ} y = monotonic-const y , preservesLUB-const y
constant : {σ τ : Type} → (y : CPO τ) → CPO (σ ⇒ τ)
constant y = fun (const y) (continuous-const y)
abstract
monotonic-fork : {τ : Type} → Monotonic {τ} (λ x → (x , x))
monotonic-fork p = ⊑-prod p p
preservesLUB-fork : {τ : Type} → PreservesLUB {τ} (λ x → (x , x))
preservesLUB-fork {τ} (P , ⨆X) ((_ , ubX , lubX) , ne) (x₁ , x₂) ub = ⊑-prod (lubX x₁ (λ x Px → fst (preservesLUB-fork-aux x Px)))
(lubX x₂ (λ x Px → snd (preservesLUB-fork-aux x Px)))
where
preservesLUB-fork-aux : (x : CPO τ) → P x → (x ⊑ x₁) × (x ⊑ x₂)
preservesLUB-fork-aux x p with ub (x , x) (x , p , refl)
preservesLUB-fork-aux x p | ⊑-prod p₁ p₂ = p₁ , p₂
continuous-fork : {τ : Type} → Continuous {τ} (λ x → (x , x))
continuous-fork = monotonic-fork , preservesLUB-fork
fork-⊗ : {τ : Type} → CPO (τ ⇒ (τ ⊗ τ))
fork-⊗ = fun (λ x → x , x) continuous-fork
abstract
preservesLUB-comp : {σ τ υ : Type} → (f : CPO (σ ⇒ τ)) → (g : CPO (τ ⇒ υ)) → PreservesLUB (_$_ g ∘ _$_ f)
preservesLUB-comp {σ} {τ} {υ} f g (P , ⨆X) p z ubZ = preservesLUB g (chainImage f (P , ⨆X)) (imageIsNonEmptyChain f (P , ⨆X) p) z preservesLUB-comp-aux
where
preservesLUB-comp-aux : (z' : CPO υ) → Σ (CPO τ) (λ y → Σ (CPO σ) (λ x → P x × f $ x ≡ y) × g $ y ≡ z') → z' ⊑ z
preservesLUB-comp-aux ._ (._ , (x , Px , refl) , refl) = ubZ (g $ f $ x) (x , Px , refl)
continuous-comp : {σ τ υ : Type} → (f : CPO (σ ⇒ τ)) → (g : CPO (τ ⇒ υ)) → Continuous (_$_ g ∘ _$_ f)
continuous-comp f g = (monotonic g ∘ monotonic f) , preservesLUB-comp f g
_∙_ : {σ τ υ : Type} → CPO (τ ⇒ υ) → CPO (σ ⇒ τ) → CPO (σ ⇒ υ)
g ∙ f = fun (_$_ g ∘ _$_ f) (continuous-comp f g)
monotonic-& : {σ τ₁ τ₂ : Type} → (f : CPO (σ ⇒ τ₁)) → (g : CPO (σ ⇒ τ₂)) → Monotonic (λ x → (f $ x) , (g $ x))
monotonic-& f g p = ⊑-prod (monotonic f p) (monotonic g p)
preservesLUB-& : {σ τ₁ τ₂ : Type} → (f : CPO (σ ⇒ τ₁)) → (g : CPO (σ ⇒ τ₂)) → PreservesLUB (λ x → (f $ x) , (g $ x))
preservesLUB-& {σ} {τ₁} {τ₂} f g (P , ⨆X) p (y₁ , y₂) ubY with preservesLUB f (P , ⨆X) p
| preservesLUB g (P , ⨆X) p
... | lubY₁ | lubY₂ = ⊑-prod (lubY₁ y₁ aux₁) (lubY₂ y₂ aux₂)
where
ubY' : (y₁' : CPO τ₁) → (y₂' : CPO τ₂) → Σ (CPO σ) (λ s → P s × f $ s ≡ y₁' × g $ s ≡ y₂') → y₁' ⊑ y₁ × y₂' ⊑ y₂
ubY' y₁' y₂' (s , Ps , eq₁ , eq₂) with ubY (y₁' , y₂') (s , (Ps , cong2 _,_ eq₁ eq₂))
... | ⊑-prod lt₁ lt₂ = lt₁ , lt₂
aux₁ : (t₁ : CPO τ₁) → Σ (CPO σ) (λ s → P s × (f $ s ≡ t₁)) → t₁ ⊑ y₁
aux₁ ._ (s , Ps , refl) = fst (ubY' (f $ s) (g $ s) (s , Ps , refl , refl))
aux₂ : (t₂ : CPO τ₂) → Σ (CPO σ) (λ s → P s × (g $ s ≡ t₂)) → t₂ ⊑ y₂
aux₂ ._ (s , Ps , refl) = snd (ubY' (f $ s) (g $ s) (s , Ps , refl , refl))
continuous-& : {σ τ₁ τ₂ : Type} → (f : CPO (σ ⇒ τ₁)) → (g : CPO (σ ⇒ τ₂)) → Continuous (λ x → (f $ x) , (g $ x))
continuous-& f g = monotonic-& f g , preservesLUB-& f g
_:&:_ : {σ τ₁ τ₂ : Type} → (f : CPO (σ ⇒ τ₁)) → (g : CPO (σ ⇒ τ₂)) → CPO (σ ⇒ (τ₁ ⊗ τ₂))
f :&: g = fun (λ x → (f $ x) , (g $ x)) (continuous-& f g)
_:×':_ : {σ₁ σ₂ τ₁ τ₂ : Type} → (f : CPO (σ₁ ⇒ τ₁)) → (g : CPO (σ₂ ⇒ τ₂)) → (CPO (σ₁ ⊗ σ₂) → CPO (τ₁ ⊗ τ₂))
(f :×': g) (x , y) = (f $ x) , (g $ y)
monotonic-× : {σ₁ σ₂ τ₁ τ₂ : Type} → (f : CPO (σ₁ ⇒ τ₁)) → (g : CPO (σ₂ ⇒ τ₂)) → Monotonic (f :×': g)
monotonic-× f g {x₁ , x₂} {y₁ , y₂} (⊑-prod p q) = ⊑-prod (monotonic f p) (monotonic g q)
preservesLUB-× : {σ₁ σ₂ τ₁ τ₂ : Type} → (f : CPO (σ₁ ⇒ τ₁)) → (g : CPO (σ₂ ⇒ τ₂)) → PreservesLUB (f :×': g)
preservesLUB-× {σ₁} {σ₂} {τ₁} {τ₂} f g (P , ⨆X₁ , ⨆X₂) pXY (y₁ , y₂) ubY
with
preservesLUB f (fstChain (P , ⨆X₁ , ⨆X₂)) (fstIsNonEmptyChain (P , ⨆X₁ , ⨆X₂) pXY)
| preservesLUB g (sndChain (P , ⨆X₁ , ⨆X₂)) (sndIsNonEmptyChain (P , ⨆X₁ , ⨆X₂) pXY)
... | lubY₁ | lubY₂
= ⊑-prod (lubY₁ y₁ aux₁) (lubY₂ y₂ aux₂)
where
ubY' : (y₁' : CPO τ₁) → (y₂' : CPO τ₂) → Σ (CPO σ₁) (λ s₁ → Σ (CPO σ₂) (λ s₂ → P (s₁ , s₂) × f $ s₁ ≡ y₁' × g $ s₂ ≡ y₂')) → y₁' ⊑ y₁ × y₂' ⊑ y₂
ubY' y₁' y₂' (s₁ , s₂ , Ps , eq₁ , eq₂) with ubY (y₁' , y₂') ((s₁ , s₂) , (Ps , cong2 _,_ eq₁ eq₂))
... | ⊑-prod lt₁ lt₂ = lt₁ , lt₂
aux₁ : (t₁ : CPO τ₁) → Σ (CPO σ₁) (λ s₁ → Σ (CPO σ₂) (λ s₂ → P (s₁ , s₂)) × (f $ s₁ ≡ t₁)) → t₁ ⊑ y₁
aux₁ ._ (s₁ , (s₂ , Pss) , refl) = fst (ubY' (f $ s₁) (g $ s₂) (s₁ , s₂ , Pss , refl , refl))
aux₂ : (t₂ : CPO τ₂) → Σ (CPO σ₂) (λ s₂ → Σ (CPO σ₁) (λ s₁ → P (s₁ , s₂)) × (g $ s₂ ≡ t₂)) → t₂ ⊑ y₂
aux₂ ._ (s₂ , (s₁ , Pss) , refl) = snd (ubY' (f $ s₁) (g $ s₂) (s₁ , s₂ , Pss , refl , refl))
continuous-× : {σ₁ σ₂ τ₁ τ₂ : Type} → (f : CPO (σ₁ ⇒ τ₁)) → (g : CPO (σ₂ ⇒ τ₂)) → Continuous (f :×': g)
continuous-× f g = monotonic-× f g , preservesLUB-× f g
_:×:_ : {σ₁ σ₂ τ₁ τ₂ : Type} → (f : CPO (σ₁ ⇒ τ₁)) → (g : CPO (σ₂ ⇒ τ₂)) → CPO ((σ₁ ⊗ σ₂) ⇒ (τ₁ ⊗ τ₂))
f :×: g = fun (f :×': g) (continuous-× f g)
∙-idL : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO (σ ⇒ τ)) → identity ∙ f ≡ f
∙-idL (fun _ _) = injective-$ refl
∙-idR : {{_ : Extensionality}} → {σ τ : Type} → (f : CPO (σ ⇒ τ)) → f ∙ identity ≡ f
∙-idR (fun _ _) = injective-$ refl
∙-assocLR : {{_ : Extensionality}} → {σ τ υ ν : Type} → (f : CPO (υ ⇒ ν)) → (g : CPO (τ ⇒ υ)) → (h : CPO (σ ⇒ τ)) → (f ∙ g) ∙ h ≡ f ∙ (g ∙ h)
∙-assocLR (fun f cf) (fun g cg) (fun h ch) = injective-$ refl
∙-assocRL : {{_ : Extensionality}} → {σ τ υ ν : Type} → (f : CPO (υ ⇒ ν)) → (g : CPO (τ ⇒ υ)) → (h : CPO (σ ⇒ τ)) → f ∙ (g ∙ h) ≡ (f ∙ g) ∙ h
∙-assocRL (fun f cf) (fun g cg) (fun h ch) = injective-$ refl
∙-assocLRE : {{_ : Extensionality}} → {σ τ υ ν ρ : Type} → (f : CPO (ν ⇒ ρ)) → (g : CPO (υ ⇒ ν)) → (h : CPO (τ ⇒ υ)) → (i : CPO (σ ⇒ τ)) → (f ∙ g ∙ h) ∙ i ≡ (f ∙ g) ∙ h ∙ i
∙-assocLRE (fun f cf) (fun g cg) (fun h ch) (fun i ci) = injective-$ refl
∙-assocELR : {{_ : Extensionality}} → {σ τ υ ν ρ : Type} → (f : CPO (ν ⇒ ρ)) → (g : CPO (υ ⇒ ν)) → (h : CPO (τ ⇒ υ)) → (i : CPO (σ ⇒ τ)) → (f ∙ g) ∙ h ∙ i ≡ (f ∙ g ∙ h) ∙ i
∙-assocELR (fun f cf) (fun g cg) (fun h ch) (fun i ci) = injective-$ refl
∙-assocRRLL : {{_ : Extensionality}} → {σ τ υ ν ρ : Type} → (f : CPO (ν ⇒ ρ)) → (g : CPO (υ ⇒ ν)) → (h : CPO (τ ⇒ υ)) → (i : CPO (σ ⇒ τ)) → f ∙ (g ∙ (h ∙ i)) ≡ ((f ∙ g) ∙ h) ∙ i
∙-assocRRLL (fun f cf) (fun g cg) (fun h ch) (fun i ci) = injective-$ refl
∙-assocRRLR : {{_ : Extensionality}} → {σ τ υ ν ρ : Type} → (f : CPO (ν ⇒ ρ)) → (g : CPO (υ ⇒ ν)) → (h : CPO (τ ⇒ υ)) → (i : CPO (σ ⇒ τ)) → f ∙ (g ∙ (h ∙ i)) ≡ (f ∙ (g ∙ h)) ∙ i
∙-assocRRLR (fun f cf) (fun g cg) (fun h ch) (fun i ci) = injective-$ refl
∙-assocLRRR : {{_ : Extensionality}} → {σ τ υ ν ρ : Type} → (f : CPO (ν ⇒ ρ)) → (g : CPO (υ ⇒ ν)) → (h : CPO (τ ⇒ υ)) → (i : CPO (σ ⇒ τ)) → (f ∙ (g ∙ h)) ∙ i ≡ f ∙ (g ∙ (h ∙ i))
∙-assocLRRR (fun f cf) (fun g cg) (fun h ch) (fun i ci) = injective-$ refl
∙-assocEC : {{_ : Extensionality}} → {σ τ υ ν ρ : Type} → (f : CPO (ν ⇒ ρ)) → (g : CPO (υ ⇒ ν)) → (h : CPO (τ ⇒ υ)) → (i : CPO (σ ⇒ τ)) → (f ∙ g) ∙ (h ∙ i) ≡ f ∙ (g ∙ h) ∙ i
∙-assocEC (fun f cf) (fun g cg) (fun h ch) (fun i ci) = injective-$ refl
∙-congR : {σ τ υ : Type} → {f g : CPO (τ ⇒ υ)} → (h : CPO (σ ⇒ τ)) → f ≡ g → f ∙ h ≡ g ∙ h
∙-congR h refl = refl
∙-congL : {σ τ υ : Type} → {g h : CPO (σ ⇒ τ)} → (f : CPO (τ ⇒ υ)) → g ≡ h → f ∙ g ≡ f ∙ h
∙-congL f refl = refl