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

------------------------------------------------------------------------

-- Some utilities for writing proofs

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'

-----------------------------------------------------------------------