{-# OPTIONS --type-in-type #-}

open import NeilPrelude
open import Extensionality
open import Logic
open import EquationalEq
open import CPO
open import CPOLemmas
open import CPOFunctions

module FixTheorems

  (fix : {τ : Type}  CPO (τ  τ)  CPO τ)

  (Computation : {τ : Type}  (f : CPO (τ  τ))  fix f  f $ (fix f))
  (Induction : {τ : Type}  {x : CPO τ}   (f : CPO (τ  τ))  f $ x  x  fix f  x)

  (fix-⊗ : {σ τ : Type}  {f : CPO (σ  σ)}  {g : CPO (τ  τ)}  fix (f :×: g)  (fix f , fix g))

  (FixpointInduction : {τ : Type}  (P : CPO τ  Set)  (f : CPO (τ  τ))  ChainComplete P  P   ((x : CPO τ)  P x  P (f $ x))  P (fix f))

where

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

fixIsFixedPoint : {τ : Type}  (f : CPO (τ  τ))  FixedPoint f (fix f)
fixIsFixedPoint f = sym (Computation f)

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

FixpointInduction-⊗ : {σ τ : Type}  (P : CPO (σ  τ)  Set)  (f : CPO (σ  σ))  (g : CPO (τ  τ))  ChainComplete P  P ( , )  ((x : CPO σ)  (y : CPO τ)  P (x , y)  P (f $ x , g $ y))  P (fix f , fix g)
FixpointInduction-⊗ {σ} {τ} P f g ccP P⊥ =

   P (fix f , fix g)
                                                               ←⟨ ≡→↔ (cong P fix-⊗) ⟩↔
   P (fix (f :×: g))
                                                               ←⟨ FixpointInduction P (f :×: g) ccP P⊥ 
   ((xy : CPO (σ  τ))  (Pxy : P xy)  P ((f :×: g) $ xy))
                                                               ←⟨ lem-products ⟩↔
   ((x : CPO σ)  (y : CPO τ)  P (x , y)  P (f $ x , g $ y))
                                                               Qed

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

⊥-LeftZero : {{_ : Extensionality}}  {σ τ υ : Type}  (f : CPO (σ  τ))    f   {σ  υ}
⊥-LeftZero (fun _ _) = injective-$ refl

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

PointFreeStrictness : {{_ : Extensionality}}  {σ τ υ : Type}  (f : CPO (τ  υ))  Strict f  (f     {σ  υ})
PointFreeStrictness f =   sf  cpo-ext' sf) ,  eq  cpo-func' eq {})

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

StrictComposition : {σ τ υ : Type}  (f : CPO (σ  τ))  (g : CPO (τ  υ))  Strict f  Strict g  Strict (g  f)
StrictComposition f g sf =

   Strict (g  f)
                   ←⟨ ↔-refl ⟩↔
   g $ f $   
                   ←⟨ ↔-≡ (cong (_$_ g) (sym sf)) refl ⟩↔
   g $   
                   ←⟨ ↔-refl ⟩↔
   Strict g
                   Qed

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

StrictCancellation : {{_ : Extensionality}}  {σ τ υ : Type}  (f : CPO (σ  τ))  (g : CPO (τ  υ))  Strict (g  f)  Strict g
StrictCancellation f g sgf = ⊑-⊥-eq

   ( g $ 
                   ⊑⟨ monotonic g ⊑-bot 
     (g  f) $ 
                   ⊑⟨ ≡→⊑ sgf 
     
                   ⊑-QED
   )

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

DownwardClosed : {{_ : Extensionality}}  {σ τ : Type}  {f g : CPO (σ  τ)}  Strict f  g  f  Strict g
DownwardClosed {_} {_} {fun f _} {fun g _} sf (⊑-fun lt) = ⊑-⊥-eq

   ( g 
            ⊑⟨ lt 
     f 
            ⊑⟨ ≡→⊑ sf 
     
            ⊑-QED
   )

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

RollingRule : {{_ : Extensionality}}  {σ τ : Type}  (f : CPO (τ  σ))  (g : CPO (σ  τ))  fix (f  g)  f $ fix (g  f)
RollingRule f g = ⊑-antisym RollingRuleL RollingRuleR
  where
    RollingRuleAux : {υ ρ : Type}  (h : CPO (ρ  υ))  (i : CPO (υ  ρ))  fix (h  i)  (h $ fix (i  h))
    RollingRuleAux h i = Induction (h  i) (≡→⊑ (
                                                  ((h  i  h) $ fix (i  h))
                                                                               cong (_$_ h) (sym (Computation (i  h))) 
                                                  (h $ fix (i  h))
                                                                              QED
                                                ))

    RollingRuleL : fix (f  g)  (f $ fix (g  f))
    RollingRuleL = RollingRuleAux f g

    RollingRuleR : (f $ fix (g  f))  fix (f  g)
    RollingRuleR = ProveTruth (
                                (f $ fix (g  f))  fix (f  g)
                                                                             ←⟨ ↔-⊑L (sym (Computation (f  g))) ⟩↔
                                (f $ fix (g  f))  ((f  g) $ fix (f  g))
                                                                             ←⟨ monotonic f 
                                fix (g  f)  ( g $ fix (f  g))
                                                                             ←⟨ RollingRuleAux g f ⟩TRUE
                              )

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

NonStrictFixFusion : {{_ : Extensionality}}  {σ τ : Type}  (f : CPO (τ  σ))  (g : CPO (τ  τ))  (h : CPO (σ  σ))  f  g  h  f  FixedPoint h (f $ fix g)
NonStrictFixFusion f g h eq =
   (h  f) $ fix g
                    cong2R _$_ (sym eq) 
   (f  g) $ fix g
                    refl 
   f $ g $ fix g
                    cong (_$_ f) (sym (Computation g)) 
   f $ fix g
                   QED

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

FixFusion : {{_ : Extensionality}}  {σ τ : Type}  (f : CPO (τ  σ))  (g : CPO (τ  τ))  (h : CPO (σ  σ))  Strict f  f  g  h  f  f $ fix g  fix h
FixFusion {σ} {τ} f g h sf eq = FixpointInduction-⊗ P g h ChainCompleteP sf

    a b eqhb  (f  g) $ a
                                 function (cong _$_ eq) 
                 (h  f) $ a
                                cong (_$_ h) eqhb 
                 h $ b
                               QED
   )

  where

    P : CPO (τ  σ)  Set
    P (y , x) = f $ y  x

    ChainCompleteP : ChainComplete P
    ChainCompleteP (Q , ⨆Y , ⨆X) (p , ne) =

        P ( YX)
                                                               ←⟨ ↔-refl ⟩↔
        f $ ⨆Y  ⨆X
                                                               ←⟨ ↔-refl ⟩↔
         (chainImage f Y)   X
                                                               ←⟨ cong-≣-⨆ (chainImage f Y) X 
        chainImage f Y  X
                                                               ←⟨ chain-ext (chainImage f Y) X ImgYisChain XisChain ⟩↔
        ((x : CPO σ)  x  chainImage f Y  x  X)
                                                               ←⟨ lem-image-eq (_$_ f) YX p 
        ((y : CPO τ)  (x : CPO σ)  (y , x)  YX  f $ y  x)
                                                               ←⟨ ↔-refl ⟩↔
        ((y : CPO τ)  (x : CPO σ)  (y , x)  YX  P (y , x))
                                                               ←⟨ ↔-sym lem-products ⟩↔
        ((yx : CPO (τ  σ))  yx  YX  P yx)
                                                               Qed
       where
             YX = (Q , ⨆Y , ⨆X )
             Y  = fstChain YX
             X  = sndChain YX

             XisChain : IsChain X
             XisChain = sndIsChain YX p

             ImgYisChain : IsChain (chainImage f Y)
             ImgYisChain = fst (imageIsNonEmptyChain f Y (fstIsNonEmptyChain YX (p , ne)))

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

FixDouble : {{_ : Extensionality}}  {τ : Type}  (f : CPO (τ  τ))  fix (f  f)  fix f
FixDouble f = ⊑-antisym (ProveTruth (
                                      fix (f  f)  fix f
                                                               ←⟨ Induction (f  f) 
                                      ((f  f) $ fix f)  fix f
                                                               ←⟨ ≡→⊑ 
                                      ((f  f) $ fix f)  fix f
                                                               ←⟨
                                                                  ((f  f) $ fix f)
                                                                                     cong (_$_ f) (sym (Computation f)) 
                                                                  (f $ fix f)
                                                                                     sym (Computation f) 
                                                                  fix f
                                                                                    QED
                                                               ⟩TRUE
                        ))
                        (ProveTruth (
                                      fix f  fix (f  f)
                                                                      ←⟨ Induction f 
                                      (f $ fix (f  f))  fix (f  f)
                                                                      ←⟨ ≡→⊑ 
                                      (f $ fix (f  f))  fix (f  f)
                                                                      ←⟨ sym (RollingRule f f) ⟩TRUE
                        ))

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