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

module WWFix

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

  (A : Type)
  (B : Type)

  (f : CPO (A ⇒ A))
  (g : CPO (B ⇒ B))
  (rep : CPO (A ⇒ B))
  (abs : CPO (B ⇒ A))

where

import FixTheorems
open FixTheorems fix Computation Induction fix-⊗ FixpointInduction

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

AssA : Set
AssA = abs ∙ rep ≡ identity

AssB : Set
AssB = abs ∙ rep ∙ f ≡ f

AssC : Set
AssC = fix (abs ∙ rep ∙ f) ≡ fix f


Cond1α : Set
Cond1α = g ≡ rep ∙ f ∙ abs

Cond1β : Set
Cond1β = fix g ≡ fix (rep ∙ f ∙ abs)

Cond2α : Set
Cond2α = (rep ∙ f ≡ g ∙ rep) × Strict rep

Cond2β : Set
Cond2β = fix g ≡ rep $ fix f

Cond3α : Set
Cond3α = abs ∙ g ≡ f ∙ abs


WWFactorisation : Set
WWFactorisation = fix f ≡ abs $ fix g

WWFusion : Set
WWFusion = rep $ abs $ fix g ≡ fix g

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

A⇒strictabs : AssA → Strict abs
A⇒strictabs A = ⊑-⊥-eq (ProveTruth (

    abs $ ⊥ ⊑ ⊥
                             ←⟨ ↔-⊑L (
                                       (abs ∙ rep) $ ⊥
                                                        ⟨ cong2R _$_ A ⟩
                                       identity $ ⊥
                                                        ⟨ refl ⟩
                                       ⊥
                                                        QED
                                     )
                              ⟩↔
    abs $ ⊥ ⊑ abs $ rep $ ⊥
                             ←⟨ monotonic abs ⟩
    ⊥ ⊑ rep $ ⊥
                             ←⟨ ⊑-bot ⟩TRUE
  ))

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

A⇒B : AssA → AssB
A⇒B A =  abs ∙ rep ∙ f
                          ⟨ ∙-assocRL abs rep f ⟩
         (abs ∙ rep) ∙ f
                          ⟨ ∙-congR f A ⟩
         identity ∙ f
                          ⟨ ∙-idL f ⟩
         f
                          QED

B⇒C : AssB → AssC
B⇒C = cong fix

A⇒C : AssA → AssC
A⇒C = B⇒C ∘ A⇒B

1α⇒1β : Cond1α → Cond1β
1α⇒1β α = cong fix α

2α⇒2β : Cond2α → Cond2β
2α⇒2β (β , strictrep) = sym (FixFusion rep f g strictrep β)

1β⇔2β : AssC → Cond1β ↔ Cond2β
1β⇔2β C = ↔-≡ refl (

   fix (rep ∙ f ∙ abs)
                                    ⟨ cong fix (∙-assocRL rep f abs) ⟩
   fix ((rep ∙ f) ∙ abs)
                                    ⟨ RollingRule (rep ∙ f) abs ⟩
   (rep ∙ f) $ fix (abs ∙ rep ∙ f)
                                    ⟨ cong (_$_ (rep ∙ f)) C ⟩
   (rep ∙ f) $ fix f
                                    ⟨ cong (_$_ rep) (sym (Computation f)) ⟩
   rep $ fix f
                                    QED)

1αB⇒3α : AssB → Cond1α → Cond3α
1αB⇒3α B =

   g ≡ rep ∙ f ∙ abs
                                  →⟨ ∙-congL abs ⟩
   abs ∙ g ≡ abs ∙ rep ∙ f ∙ abs
                                  →⟨ ↔-≡ refl ( abs ∙ rep ∙ f ∙ abs
                                                                      ⟨ ∙-assocRRLR abs rep f abs ⟩
                                                (abs ∙ rep ∙ f) ∙ abs
                                                                      ⟨ ∙-congR abs B ⟩
                                                f ∙ abs
                                                                      QED
                                              )
                                   ⟩↔
   abs ∙ g ≡ f ∙ abs
                                   Qed

1αA⇒2α : AssA → Strict rep → Cond1α → Cond2α
1αA⇒2α A sr =

   g ≡ rep ∙ f ∙ abs
                                     →⟨ ∙-congR rep ⟩
   g ∙ rep ≡ (rep ∙ f ∙ abs) ∙ rep
                                     →⟨ ↔-≡ refl ( (rep ∙ f ∙ abs) ∙ rep
                                                                          ⟨ ∙-assocLRE rep f abs rep ⟩
                                                   (rep ∙ f) ∙ abs ∙ rep
                                                                          ⟨ ∙-congL (rep ∙ f) A ⟩
                                                   (rep ∙ f) ∙ identity
                                                                          ⟨ ∙-idR (rep ∙ f) ⟩
                                                   rep ∙ f
                                                                          QED)
                                     ⟩↔
   g ∙ rep ≡ rep ∙ f
                                     →⟨ (λ eq → sym eq , sr) ⟩
   Cond2α
                                             Qed

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

1βC⇒Fac : AssC → Cond1β → WWFactorisation
1βC⇒Fac C β =

   fix f
                                ⟨ sym C ⟩
   fix (abs ∙ rep ∙ f)
                                ⟨ RollingRule abs (rep ∙ f) ⟩
   abs $ fix ((rep ∙ f) ∙ abs)
                                ⟨ cong (_$_ abs ∘ fix) (∙-assocLR rep f abs) ⟩
   abs $ fix (rep ∙ f ∙ abs)
                                ⟨ cong (_$_ abs) (sym β) ⟩
   abs $ fix g
                                QED

2βC⇒Fac : AssC → Cond2β → WWFactorisation
2βC⇒Fac C β = 1βC⇒Fac C (snd (1β⇔2β C) β)

1αC⇒Fac : AssC → Cond1α → WWFactorisation
1αC⇒Fac C = 1βC⇒Fac C ∘ 1α⇒1β

2αC⇒Fac : AssC → Cond2α → WWFactorisation
2αC⇒Fac C = 2βC⇒Fac C ∘ 2α⇒2β

2βC⇒Fusion : AssC → Cond2β → WWFusion
2βC⇒Fusion C β =

   rep $ abs $ fix g
                      ⟨ cong (_$_ rep) (sym (2βC⇒Fac C β)) ⟩
   rep $ fix f
                      ⟨ sym β ⟩
   fix g
                      QED

1βC⇒Fusion : AssC → Cond1β → WWFusion
1βC⇒Fusion C β = 2βC⇒Fusion C (fst (1β⇔2β C) β)

1αC⇒Fusion : AssC → Cond1α → WWFusion
1αC⇒Fusion C = 1βC⇒Fusion C ∘ 1α⇒1β

2αC⇒Fusion : AssC → Cond2α → WWFusion
2αC⇒Fusion C = 2βC⇒Fusion C ∘ 2α⇒2β

FactFusionC⇒2β : AssC → WWFactorisation → WWFusion → Cond2β
FactFusionC⇒2β C fact fus =

   fix g
                      ⟨ sym fus ⟩
   rep $ abs $ fix g
                      ⟨ cong (_$_ rep) (sym fact) ⟩
   rep $ fix f
                      QED

FactFusion⇔2β : AssC → Cond2β ↔ (WWFactorisation × WWFusion)
FactFusion⇔2β C = (λ β → 2βC⇒Fac C β , 2βC⇒Fusion C β) , uncurry (FactFusionC⇒2β C)

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

3αC⇒Fac : AssC → Cond3α → WWFactorisation
3αC⇒Fac C α = ⊑-antisym leqL leqR
  where
    leqL : fix f ⊑ abs $ fix g
    leqL = ProveTruth (
              fix f ⊑ abs $ fix g
                                               ←⟨ Induction f ⟩
              (f ∙ abs) $ fix g ⊑ abs $ fix g
                                               ←⟨ ↔-⊑R (cong2R _$_ α) ⟩↔
              (abs ∙ g) $ fix g ⊑ abs $ fix g
                                               ←⟨ ↔-⊑R (cong (_$_ abs) (Computation g)) ⟩↔
              abs $ fix g  ⊑ abs $ fix g
                                               ←⟨ ⊑-refl ⟩TRUE
              )

    P : CPO B → Set
    P b = abs $ b ⊑ fix f

    ChainCompleteP : ChainComplete P
    ChainCompleteP X p =

        P (⨆ X)
                                                 ←⟨ ↔-refl ⟩↔
        abs $ ⨆ X ⊑ fix f
                                                 ←⟨ ↔-refl ⟩↔
        ⨆ (chainImage abs X) ⊑ fix f
                                                 ←⟨ continuity abs X p (fix f) ⟩↔
        ((b : CPO B) → b ∈ X → abs $ b ⊑ fix f)
                                                 ←⟨ ↔-refl ⟩↔
        ((b : CPO B) → b ∈ X → P b)
                                                 Qed

    leqR : abs $ fix g ⊑ fix f
    leqR = FixpointInduction P g ChainCompleteP
             (ProveTruth (
                 P ⊥
                                                       ←⟨ ↔-refl ⟩↔
                 abs $ ⊥ ⊑ fix f
                                                       ←⟨ ↔-⊑L C ⟩↔
                 abs $ ⊥ ⊑ fix (abs ∙ rep ∙ f)
                                                       ←⟨ ↔-⊑L (sym (RollingRule abs (rep ∙ f))) ⟩↔
                 abs $ ⊥ ⊑ abs $ fix ((rep ∙ f) ∙ abs)
                                                       ←⟨ monotonic abs ⟩
                 ⊥ ⊑ fix ((rep ∙ f) ∙ abs)
                                                       ←⟨ ⊑-bot ⟩TRUE
                 )
             )
             (λ b →
                    P (g $ b)
                                           ←⟨ ↔-refl ⟩↔
                    (abs ∙ g) $ b ⊑ fix f
                                           ←⟨ ↔-⊑R (sym (cong2R _$_ α)) ⟩↔
                    (f ∙ abs) $ b ⊑ fix f
                                           ←⟨ ↔-⊑L (sym (Computation f)) ⟩↔
                    f $ abs $ b ⊑ f $ fix f
                                           ←⟨ monotonic f ⟩
                    abs $ b ⊑ fix f
                                           ←⟨ ↔-refl ⟩↔
                    P b
                                           Qed
             )

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

WW-Fix-Fac : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) ⊎ Cond3α → WWFactorisation
WW-Fix-Fac C (inl (inl 1α))       = 1αC⇒Fac C 1α
WW-Fix-Fac C (inl (inr 1β))       = 1βC⇒Fac C 1β
WW-Fix-Fac C (inr (inl (inl 2α))) = 2αC⇒Fac C 2α
WW-Fix-Fac C (inr (inl (inr 2β))) = 2βC⇒Fac C 2β
WW-Fix-Fac C (inr (inr 3α))       = 3αC⇒Fac C 3α

WW-Fix-Fusion : AssC → (Cond1α ⊎ Cond1β) ⊎ (Cond2α ⊎ Cond2β) → WWFusion
WW-Fix-Fusion C (inl (inl 1α)) = 1αC⇒Fusion C 1α
WW-Fix-Fusion C (inl (inr 1β)) = 1βC⇒Fusion C 1β
WW-Fix-Fusion C (inr (inl 2α)) = 2αC⇒Fusion C 2α
WW-Fix-Fusion C (inr (inr 2β)) = 2βC⇒Fusion C 2β

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