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