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