{-# 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αC⇒Fac C 
WW-Fix-Fac C (inl (inr ))       = 1βC⇒Fac C 
WW-Fix-Fac C (inr (inl (inl ))) = 2αC⇒Fac C 
WW-Fix-Fac C (inr (inl (inr ))) = 2βC⇒Fac C 
WW-Fix-Fac C (inr (inr ))       = 3αC⇒Fac C 

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

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