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

open import NeilPrelude hiding (result)
open import Logic
open import Extensionality
open import CPO
open import EquationalEq
open import CPOLemmas
open import CPOFunctions
import Fold

module FoldTheorems

  (ext : Extensionality)

  (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))

  (F : Functor)
  (fmap' : {σ τ : Type}  CPO ((σ  τ)  (F σ  F τ)))
  (fmap-id   : {τ : Type}  fmap' $ identity {τ}  identity)
  (fmap-comp : {σ τ υ : Type}  (f : CPO (τ  υ))  (g : CPO (σ  τ))  fmap' $ (f  g)  (fmap' $ f)  (fmap' $ g))

  (μ : Functor  Type)
  (inn    : CPO (F (μ F)  μ F))
  (out    : CPO (μ F  F (μ F)))
  (innSur : inn  out  identity)
  (outInj : out  inn  identity)
  (lemma-fold-inn : (Fold.fold ext fix F fmap' μ out) inn  identity)

where

import FixTheorems
open FixTheorems fix Computation Induction fix-⊗ FixpointInduction public

import ContinuityProps
open ContinuityProps ext fix

open Fold ext fix F fmap' μ out public

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

fmap : {σ τ : Type}  CPO (σ  τ)  CPO (F σ  F τ)
fmap = _$_ fmap'

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

lemma-fold-in : fold inn  identity
lemma-fold-in = lemma-fold-inn

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

strict-in : Strict inn
strict-in = StrictCancellation out inn (cpo-func' innSur)

strict-out : Strict out
strict-out = StrictCancellation inn out (cpo-func' outInj)

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

FoldDef : {τ : Type}  (f : CPO (F τ  τ))  fold f  f  fmap (fold f)  out
FoldDef f =

   fold f
                                                refl 
   fix (fold-fun f)
                                                Computation (fold-fun f) 
    h  f  fmap h  out) (fix (fold-fun f))
                                                refl 
    h  f  fmap h  out) (fold f)
                                                refl 
   f  fmap (fold f)  out
                                               QED

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

UniPropFoldL : {τ : Type}  (f : CPO (F τ  τ))  (h : CPO (μ F  τ))  h  fold f  h  inn  f  fmap h
UniPropFoldL f ._ refl = ProveTruth (

   fold f  inn  f  fmap (fold f)
                                               ←⟨ ↔-≡ refl (
                                                     (f  fmap (fold f)  out)  inn
                                                                                       ∙-assocLRE f (fmap (fold f)) out inn 
                                                     (f  fmap (fold f))  out  inn
                                                                                       ∙-congL (f  fmap (fold f)) outInj 
                                                     (f  fmap (fold f))  identity
                                                                                       ∙-idR (f  fmap (fold f)) 
                                                     f  fmap (fold f)
                                                                                      QED
                                                     )
                                                ⟩↔
   fold f  inn  (f  fmap (fold f)  out)  inn
                                               ←⟨ ∙-congR inn 
   fold f  f  fmap (fold f)  out
                                               ←⟨ FoldDef f ⟩TRUE
   )


UniPropFoldR : {τ : Type}  (f : CPO (F τ  τ))  (h : CPO (μ F  τ))  Strict h  h  inn  f  fmap h  h  fold f
UniPropFoldR {τ} f (fun h' ch) sh eq = ProveTruth (

   h  fold f
                                            ←⟨ ↔-≡ (∙-idR h) refl ⟩↔
   h  identity  fold f
                                            ←⟨ ↔-≡ (∙-congL h lemma-fold-in) refl ⟩↔
   h  fold inn  fold f
                                            ←⟨ ↔-refl ⟩↔
   P (fold inn , fold f)
                                            ←⟨ ↔-refl ⟩↔
   P (fix (fold-fun inn) , fix (fold-fun f))
                                            ←⟨ FixpointInduction-⊗ P (fold-fun inn) (fold-fun f) ChainCompleteP base-case inductive-case ⟩TRUE )

   where
     h = fun h' ch

     P : CPO ((μ F  μ F)  (μ F  τ))  Set
     P (i , j) = h  i  j

     base-case : P ( , )
     base-case = ProveTruth (
                    P ( , )
                                           ←⟨ ↔-refl ⟩↔
                    h     { μ F  τ }
                                           ←⟨ PointFreeStrictness h ⟩↔
                    Strict h
                                           ←⟨ sh ⟩TRUE
                    )

     inductive-case : (i : CPO (μ F  μ F))  (j : CPO (μ F  τ))  h  i  j  h  inn  fmap i  out  f  fmap j  out
     inductive-case i ._ refl =

       h  inn  fmap i  out
                                     ∙-assocRL h inn (fmap i  out) 
       (h  inn)  fmap i  out
                                     ∙-congR (fmap i  out) eq 
       (f  fmap h)  fmap i  out
                                     ∙-assocEC f (fmap h) (fmap i) out 
       f  (fmap h  fmap i)  out
                                     ∙-congL f (∙-congR out (sym (fmap-comp h i))) 
       f  fmap (h  i)  out
                                     QED

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

       P ( XY)
                                                                                ←⟨ ↔-refl ⟩↔
       P ( X ,  Y)
                                                                                ←⟨ ↔-refl ⟩↔
       h   X   Y
                                                                                ←⟨ ↔-refl ⟩↔
        (chainImage' (_∙_ h) X)   Y
                                                                                ←⟨ cong-≣-⨆ (chainImage' (_∙_ h) X) Y 
       chainImage' (_∙_ h) X  Y
                                                                                ←⟨ chain-ext (chainImage' (_∙_ h) X) Y imgXisChain YisChain ⟩↔
       ((y : CPO (μ F  τ))  y  chainImage' (_∙_ h) X  y  Y)
                                                                                ←⟨ lem-image-eq (_∙_ h) XY p 
       ((x : CPO (μ F  μ F))  (y : CPO (μ F  τ))  (x , y)  XY  h  x  y)
                                                                                ←⟨ ↔-refl ⟩↔
       ((x : CPO (μ F  μ F))  (y : CPO (μ F  τ))  (x , y)  XY  P (x , y))
                                                                                ←⟨ ↔-sym lem-products ⟩↔
       ((xy : CPO ((μ F  μ F)  (μ F  τ)))  xy  XY  P xy)
                                                                                Qed
       where
          XY = (Q , ⨆X , ⨆Y)
          X  = fstChain XY
          Y  = sndChain XY

          XisChain : IsChain X
          XisChain = fstIsChain XY p

          YisChain : IsChain Y
          YisChain = sndIsChain XY p

          imgXisChain : IsChain (chainImage' (_∙_ h) X)
          imgXisChain = fst (imageIsNonEmptyChain (result h) X (fstIsNonEmptyChain XY (p , ne)))

UniversalPropFold : {τ : Type}  (f : CPO (F τ  τ))  (h : CPO (μ F  τ))  Strict h  h  fold f  h  inn  f  fmap h
UniversalPropFold f h sh = UniPropFoldL f h , UniPropFoldR f h sh

FoldHomo : {τ : Type}  (f : CPO (F τ  τ))  fold f  inn  f  fmap (fold f)
FoldHomo f = UniPropFoldL f (fold f) refl

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

FmapPreservesStrictness : {σ τ : Type}  (f : CPO (σ  τ))  Strict f  Strict (fmap f)
FmapPreservesStrictness f sf = ProveTruth (

   Strict (fmap f)
                                           ←⟨ StrictCancellation (fmap ) (fmap f) 
   Strict (fmap f  fmap )
                                           ←⟨ ≡→↔ (cong Strict (
                                                      fmap 
                                                                       cong fmap (sym (fst (PointFreeStrictness f) sf)) 
                                                      fmap (f  )
                                                                       fmap-comp f  
                                                      fmap f  fmap 
                                                                      QED
                                                  ))
                                           ⟩↔
   Strict (fmap )
                                           ←⟨  p  DownwardClosed (fst p) (snd p)) 
   (Strict identity × (fmap   identity))
                                           ←⟨  p  refl , p) 
   fmap   identity
                                           ←⟨ ↔-⊑L fmap-id ⟩↔
   fmap   fmap identity
                                           ←⟨ monotonic fmap' 
     identity
                                           ←⟨ ⊑-bot ⟩TRUE
   )

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

chainCompleteStrict : {σ τ : Type}  ChainComplete (Strict {σ} {τ})
chainCompleteStrict {σ} {τ} X p =

    Strict ( X)
                                               ←⟨ ↔-refl ⟩↔
    ( X) $   
                                               ←⟨ flip ⊑-antisym ⊑-bot 
    ( X) $   
                                               ←⟨ ↔-refl ⟩↔
     h  h $ ) ( X)  
                                               ←⟨ ↔-refl ⟩↔
     (chainImage'  h  h $ ) X)  
                                               ←⟨ continuity (appTo ) X p  ⟩↔
    ((h : CPO (σ  τ))  h  X  (h $ )  )
                                               ←⟨ result2' ⊑-eq 
    ((h : CPO (σ  τ))  h  X  (h $ )  )
                                               ←⟨ ↔-refl ⟩↔
    ((h : CPO (σ  τ))  h  X  Strict h)
                                               Qed

FoldPreservesStrictness : {τ : Type}  (f : CPO (F τ  τ))  Strict f  Strict (fold f)
FoldPreservesStrictness {τ} f sf = ProveTruth (

    Strict (fold f)
                               ←⟨ ↔-refl ⟩↔
    Strict (fix (fold-fun f))
                               ←⟨ FixpointInduction Strict (fold-fun f) chainCompleteStrict refl indStep ⟩TRUE)

  where
    indStep : (g : CPO (μ F  τ))  Strict g  (f  fmap g  out) $   
    indStep g sg =
                    f $ fmap g $ out $ 
                                           cong (_$_ f  _$_ (fmap g)) strict-out 
                    f $ fmap g $ 
                                           cong (_$_ f) (FmapPreservesStrictness g sg) 
                    f $ 
                                           sf 
                    
                                          QED

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

RollingRuleFold : {σ τ : Type}  (f : CPO (τ  σ))  (g : CPO (F σ  τ))  fold (f  g)  f  fold (g  fmap f)
RollingRuleFold f g =

    fold (f  g)
                                    refl 
    fix (fold-fun (f  g))
                                    cong fix (cpo-ext  h  (
                                                                (f  g)  fmap h  out
                                                                                        ∙-assocLR f g (fmap h  out) 
                                                                f  g  fmap h  out
                                                                                       QED)))
                                   
    fix (result f  fold-fun g)
                                    RollingRule (result f) (fold-fun g) 
    f  fix (fold-fun g  result f)
                                    cong ((_∙_ f)  fix) (cpo-ext ( λ h  (
                                                                             g  (fmap (f  h)  out)
                                                                                                           ∙-congL g ( fmap (f  h)  out
                                                                                                                                                 ∙-congR out (fmap-comp f h) 
                                                                                                                        (fmap f  fmap h)  out
                                                                                                                                                 ∙-assocLR (fmap f) (fmap h) out 
                                                                                                                        fmap f  (fmap h  out)
                                                                                                                                                QED)
                                                                                                          
                                                                             g  (fmap f  (fmap h  out))
                                                                                                           ∙-assocRL g (fmap f) (fmap h  out) 
                                                                             (g  fmap f)  (fmap h  out)
                                                                                                          QED)))
                                   
    f  fix (fold-fun (g  fmap f))
                                    refl 
    f  fold (g  fmap f)
                                   QED


ComputationFold : {τ : Type}  (f : CPO (F τ  τ))  fold f  f  fold (fmap f)
ComputationFold f =

          fold f
                                         cong fold (sym (∙-idR f)) 
          fold (f  identity)
                                         RollingRuleFold f identity 
          f  fold (identity  fmap f)
                                         cong (_∙_ f  fold) (∙-idL (fmap f)) 
          f  fold (fmap f)
                                        QED

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

FoldReflectsStrictness : {τ : Type}  (f : CPO (F τ  τ))  Strict (fold f)  Strict f
FoldReflectsStrictness f =
                            Strict f
                                                          ←⟨ StrictCancellation (fold (fmap f)) f 
                            Strict (f  fold (fmap f))
                                                          ←⟨ ≡→↔ (cong Strict (ComputationFold f)) ⟩↔
                            Strict (fold f)
                                                          Qed

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

FoldFunctorProp : {τ : Type}  (f g : CPO (F τ  τ))  fold f  fold g   fold (fmap f)  fold (fmap g)
FoldFunctorProp f g eq =

   fold (fmap f)
                         FFPropAux f 
   fmap (fold f)  out
                         ∙-congR out (cong fmap eq) 
   fmap (fold g)  out
                         sym (FFPropAux g) 
   fold (fmap g)
                        QED

  where
    FFPropAux : {σ : Type}  (h : CPO (F σ  σ))  fold (fmap h)  fmap (fold h)  out
    FFPropAux h =

       fold (fmap h)
                                               FoldDef (fmap h) 
       fmap h  fmap (fold (fmap h))  out
                                               ∙-assocRL (fmap h) (fmap (fold (fmap h))) out 
       (fmap h  fmap (fold (fmap h)))  out
                                               ∙-congR out (sym (fmap-comp h (fold (fmap h)))) 
       fmap (h  fold (fmap h))  out
                                               ∙-congR out (cong fmap (sym (ComputationFold h))) 
       fmap (fold h)  out
                                              QED

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

private
  FoldFusionAux : {σ τ : Type}  (f : CPO (F σ  σ))  (g : CPO (F τ  τ))  (h : CPO (σ  τ))  h  f  g  fmap h  result h  fold-fun f  fold-fun g  result h
  FoldFusionAux f g h eq = cpo-ext  e 
                                          h  f  fmap e  out
                                                                     ∙-assocRRLL h f (fmap e) out 
                                          ((h  f)  fmap e)  out
                                                                     ∙-congR out (
                                                                                    (h  f)  fmap e
                                                                                                            ∙-congR (fmap e) eq 
                                                                                    (g  fmap h)  fmap e
                                                                                                            ∙-assocLR g (fmap h) (fmap e) 
                                                                                    g  fmap h  fmap e
                                                                                                            ∙-congL g (sym (fmap-comp h e)) 
                                                                                    g  fmap (h  e)
                                                                                                           QED)
                                                                    
                                          (g  fmap (h  e))  out
                                                                     ∙-assocLR g (fmap (h  e)) out  
                                          g  fmap (h  e)  out
                                                                    QED
                                   )

NonStrictFoldFusion : {σ τ : Type}  (f : CPO (F σ  σ))  (g : CPO (F τ  τ))  (h : CPO (σ  τ))  h  f  g  fmap h  FixedPoint (fold-fun g) (h  fold f)
NonStrictFoldFusion f g h eq = ProveTruth (

   FixedPoint (fold-fun g) (h  fold f)
                                               ←⟨ NonStrictFixFusion (result h) (fold-fun f) (fold-fun g) 
   result h  fold-fun f  fold-fun g  result h
                                               ←⟨ FoldFusionAux f g h eq ⟩TRUE
   )

FoldFusion : {σ τ : Type}  (f : CPO (F σ  σ))  (g : CPO (F τ  τ))  (h : CPO (σ  τ))  Strict h  h  f  g  fmap h  h  fold f  fold g
FoldFusion f g h sh eq = ProveTruth (

   h  fold f  fold g
                                               ←⟨ ↔-refl  ⟩↔
   h  fix (fold-fun f)  fix (fold-fun g)
                                               ←⟨ FixFusion (result h) (fold-fun f) (fold-fun g) (fst (PointFreeStrictness h) sh) 
   result h  fold-fun f  fold-fun g  result h
                                               ←⟨ FoldFusionAux f g h eq ⟩TRUE
   )

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