{-# OPTIONS --type-in-type #-}
open import NeilPrelude hiding (result)
open import Logic
open import Extensionality
open import EquationalEq
open import CPO
open import CPOLemmas
open import CPOFunctions
import Fold
module WWFoldDerived
(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)
(A : Type)
(B : Type)
(f : CPO (F A ⇒ A))
(g : CPO (F B ⇒ B))
(rep : CPO (A ⇒ B))
(abs : CPO (B ⇒ A))
where
import ContinuityProps
open ContinuityProps ext fix
import WWFoldCommon
open WWFoldCommon ext fix Computation Induction fix-⊗ FixpointInduction F fmap' fmap-id fmap-comp μ inn out innSur outInj lemma-fold-inn A B f g rep abs
f' : CPO ((μ F ⇒ A) ⇒ (μ F ⇒ A))
f' = fold-fun f
g' : CPO ((μ F ⇒ B) ⇒ (μ F ⇒ B))
g' = fold-fun g
abs' : CPO ((μ F ⇒ B) ⇒ (μ F ⇒ A))
abs' = result abs
rep' : CPO ((μ F ⇒ A) ⇒ (μ F ⇒ B))
rep' = result rep
import WWFix
open WWFix ext fix Computation Induction fix-⊗ FixpointInduction (μ F ⇒ A) (μ F ⇒ B) f' g' rep' abs' renaming (AssA to AssA-fix ; AssB to AssB-fix ; AssC to AssC-fix ; Cond1α to Cond1α-fix ; Cond1β to Cond1β-fix ; Cond2α to Cond2α-fix ; Cond2β to Cond2β-fix ; Cond3α to Cond3α-fix ; WWFactorisation to WWFactorisation-fix ; WWFusion to WWFusion-fix)
AssA⇒AssA-fix : AssA → AssA-fix
AssA⇒AssA-fix A = cpo-ext (λ h → abs ∙ rep ∙ h
⟨ ∙-assocRL abs rep h ⟩
(abs ∙ rep) ∙ h
⟨ ∙-congR h A ⟩
identity ∙ h
⟨ ∙-idL h ⟩
h
QED)
AssB⇒AssB-fix : AssB → AssB-fix
AssB⇒AssB-fix B = cpo-ext (λ h → abs ∙ rep ∙ f ∙ fmap h ∙ out
⟨ ∙-assocRRLR abs rep f (fmap h ∙ out) ⟩
(abs ∙ rep ∙ f) ∙ fmap h ∙ out
⟨ ∙-congR (fmap h ∙ out) B ⟩
f ∙ fmap h ∙ out
QED )
AssC⇔AssC-fix : AssC ↔ AssC-fix
AssC⇔AssC-fix = ↔-≡ (cong fix (cpo-ext (λ h → (abs ∙ rep ∙ f) ∙ fmap h ∙ out
⟨ ∙-assocLRRR abs rep f (fmap h ∙ out) ⟩
abs ∙ rep ∙ f ∙ fmap h ∙ out
QED)))
refl
AssC⇒AssC-fix : AssC → AssC-fix
AssC⇒AssC-fix = fst AssC⇔AssC-fix
cond1aux : (h : CPO (μ F ⇒ B)) → (rep ∙ f ∙ fmap abs) ∙ fmap h ∙ out ≡ rep ∙ f ∙ fmap (abs ∙ h) ∙ out
cond1aux h =
(rep ∙ f ∙ fmap abs) ∙ fmap h ∙ out
⟨ ∙-assocLR rep (f ∙ fmap abs) (fmap h ∙ out) ⟩
rep ∙ (f ∙ fmap abs) ∙ fmap h ∙ out
⟨ ∙-congL rep (
(f ∙ fmap abs) ∙ fmap h ∙ out
⟨ ∙-assocEC f (fmap abs) (fmap h) out ⟩
f ∙ (fmap abs ∙ fmap h) ∙ out
⟨ ∙-congL f (∙-congR out (sym (fmap-comp abs h))) ⟩
f ∙ fmap (abs ∙ h) ∙ out
QED )
⟩
rep ∙ f ∙ fmap (abs ∙ h) ∙ out
QED
Cond1α⇒Cond1α-fix : Cond1α → Cond1α-fix
Cond1α⇒Cond1α-fix 1α = cpo-ext (λ h → g ∙ fmap h ∙ out
⟨ ∙-congR (fmap h ∙ out) 1α ⟩
(rep ∙ f ∙ fmap abs) ∙ fmap h ∙ out
⟨ cond1aux h ⟩
rep ∙ f ∙ fmap (abs ∙ h) ∙ out
QED)
Cond1β⇔Cond1β-fix : Cond1β ↔ Cond1β-fix
Cond1β⇔Cond1β-fix = ↔-≡ refl (cong fix (cpo-ext cond1aux))
Cond1β⇒Cond1β-fix : Cond1β → Cond1β-fix
Cond1β⇒Cond1β-fix = fst Cond1β⇔Cond1β-fix
Cond2α⇒Cond2α-fix : Cond2α → Cond2α-fix
Cond2α⇒Cond2α-fix = 2αAuxEq ∥ fst (PointFreeStrictness rep)
where
2αAuxEq : rep ∙ f ≡ g ∙ fmap rep → rep' ∙ f' ≡ g' ∙ rep'
2αAuxEq 2α = cpo-ext (λ h →
rep ∙ f ∙ fmap h ∙ out
⟨ ∙-assocRL rep f (fmap h ∙ out) ⟩
(rep ∙ f) ∙ fmap h ∙ out
⟨ ∙-congR (fmap h ∙ out) 2α ⟩
(g ∙ fmap rep) ∙ fmap h ∙ out
⟨ ∙-assocEC g (fmap rep) (fmap h) out ⟩
g ∙ (fmap rep ∙ fmap h) ∙ out
⟨ ∙-congL g (∙-congR out (sym (fmap-comp rep h))) ⟩
g ∙ fmap (rep ∙ h) ∙ out
QED)
Cond2β⇒Cond2β-fix : Cond2β → Cond2β-fix
Cond2β⇒Cond2β-fix 2β = 2β
Cond3α⇒Cond3α-fix : Cond3α → Cond3α-fix
Cond3α⇒Cond3α-fix 3α = cpo-ext (λ h →
abs ∙ g ∙ fmap h ∙ out
⟨ ∙-assocRL abs g (fmap h ∙ out) ⟩
(abs ∙ g) ∙ fmap h ∙ out
⟨ ∙-congR (fmap h ∙ out) 3α ⟩
(f ∙ fmap abs) ∙ fmap h ∙ out
⟨ ∙-assocEC f (fmap abs) (fmap h) out ⟩
f ∙ (fmap abs ∙ fmap h) ∙ out
⟨ ∙-congL f (∙-congR out (sym (fmap-comp abs h))) ⟩
f ∙ fmap (abs ∙ h) ∙ out
QED)
WWFac-Fix⇒WWFac : WWFactorisation-fix → WWFactorisation
WWFac-Fix⇒WWFac fac = fac
WWFusion-Fix⇒WWFusion : WWFusion-fix → WWFusion
WWFusion-Fix⇒WWFusion fus = fus
WW-Fold-Fac : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) ⊎ Cond3α → WWFactorisation
WW-Fold-Fac C cond = WW-Fix-Fac (AssC⇒AssC-fix C) (map-⊎ (map-⊎ Cond1α⇒Cond1α-fix Cond1β⇒Cond1β-fix)
(map-⊎ (map-⊎ Cond2α⇒Cond2α-fix Cond2β⇒Cond2β-fix)
Cond3α⇒Cond3α-fix)
cond)
WW-Fold-Fusion : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) → WWFusion
WW-Fold-Fusion C cond = WW-Fix-Fusion (AssC⇒AssC-fix C) (map-⊎ (map-⊎ Cond1α⇒Cond1α-fix Cond1β⇒Cond1β-fix)
(map-⊎ Cond2α⇒Cond2α-fix Cond2β⇒Cond2β-fix)
cond)