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

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

module FoldTheoremsInstantiated

  (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 FoldTheorems
open FoldTheorems ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn
    hiding (RollingRuleFold ; ComputationFold ; FoldFusion ; FoldReflectsStrictness ; FoldFunctorProp)

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

FoldFusionInstantiated : {σ τ : Type} → (f : CPO (F σ ⇒ σ)) → (g : CPO (F τ ⇒ τ)) → (h : CPO (σ ⇒ τ)) → Strict f → Strict h → h ∙ f ≡ g ∙ fmap h → h ∙ fold f ≡ fold g
FoldFusionInstantiated f g h sf sh =

   h ∙ fold f ≡ fold g
                                                          ←⟨ ↔-sym (UniversalPropFold g (h ∙ fold f) (StrictComposition (fold f) h (FoldPreservesStrictness f sf) sh )) ⟩↔
   (h ∙ fold f) ∙ inn ≡ g ∙ fmap (h ∙ fold f)
                                                          ←⟨ ↔-≡ refl (∙-congL g (sym (fmap-comp h (fold f)))) ⟩↔
   (h ∙ fold f) ∙ inn ≡ g ∙ fmap h ∙ fmap (fold f)
                                                          ←⟨ ↔-≡ (∙-assocRL h (fold f) inn) (∙-assocLR g (fmap h) (fmap (fold f))) ⟩↔
   h ∙ (fold f ∙ inn) ≡ (g ∙ fmap h) ∙ fmap (fold f)
                                                          ←⟨ ↔-≡ (∙-congL h (sym (FoldHomo f))) refl ⟩↔
   h ∙ (f ∙ fmap (fold f)) ≡ (g ∙ fmap h) ∙ fmap (fold f)
                                                          ←⟨ ↔-≡ (∙-assocLR h f (fmap (fold f))) refl ⟩↔
   (h ∙ f) ∙ fmap (fold f) ≡ (g ∙ fmap h) ∙ fmap (fold f)
                                                          ←⟨ ∙-congR (fmap (fold f)) ⟩
   h ∙ f ≡ g ∙ fmap h
                                                          Qed

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

RollingRuleFoldInstantiated : {σ τ : Type} → (f : CPO (τ ⇒ σ)) → (g : CPO (F σ ⇒ τ)) → Strict f → Strict g → fold (f ∙ g) ≡ f ∙ fold (g ∙ fmap f)
RollingRuleFoldInstantiated f g sf sg = sym (FoldFusionInstantiated
                                                     (g ∙ fmap f)
                                                     (f ∙ g)
                                                     f
                                                     (StrictComposition (fmap f) g (FmapPreservesStrictness f sf) sg)
                                                     sf
                                                     (∙-assocRL f g (fmap f))
                                            )

ComputationFoldInstantiated : {τ : Type} → (f : CPO (F τ ⇒ τ)) → Strict f → fold f ≡ f ∙ fold (fmap f)
ComputationFoldInstantiated f sf =

   fold f
                                ⟨ cong fold (sym (∙-idR f))  ⟩
   fold (f ∙ identity)
                                ⟨ RollingRuleFoldInstantiated f identity sf refl ⟩
   f ∙ fold (identity ∙ fmap f)
                                ⟨ ∙-congL f (cong fold (∙-idL (fmap f))) ⟩
   f ∙ fold (fmap f)
                                QED

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

FoldFunctorPropInstantiated : {τ : Type} → (f g : CPO (F τ ⇒ τ)) → Strict f → Strict g → fold f ≡ fold g  → fold (fmap f) ≡ fold (fmap g)
FoldFunctorPropInstantiated f g sf sg eq =

   fold (fmap f)
                        ⟨ FFPropAux f sf ⟩
   fmap (fold f) ∙ out
                        ⟨ ∙-congR out (cong fmap eq) ⟩
   fmap (fold g) ∙ out
                        ⟨ sym (FFPropAux g sg) ⟩
   fold (fmap g)
                        QED

  where
    FFPropAux : {σ : Type} → (h : CPO (F σ ⇒ σ)) → Strict h → fold (fmap h) ≡ fmap (fold h) ∙ out
    FFPropAux h sh =

       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 (ComputationFoldInstantiated h sh))) ⟩
       fmap (fold h) ∙ out
                                              QED

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