------------------------------------------------------------------------
-- Fixpoint combinators
------------------------------------------------------------------------

{-# OPTIONS --without-K #-}

open import Partiality-algebra as PA hiding (id; _∘_)

module Partiality-algebra.Fixpoints where

open import Equality.Propositional
open import Interval using (ext)
open import Logical-equivalence using (_⇔_)
open import Prelude hiding ()

open import Bijection equality-with-J using (_↔_)
import Equivalence equality-with-J as Eq
open import Function-universe equality-with-J hiding (id; _∘_)
open import H-level equality-with-J hiding (Type)
open import H-level.Closure equality-with-J
open import Monad equality-with-J
open import Univalence-axiom equality-with-J

open import Partiality-algebra.Monotone
open import Partiality-algebra.Omega-continuous
import Partiality-algebra.Properties as PAP

open [_⟶_]⊑

-- The development below, up to fix-is-least, is (very similar to)
-- Kleene's fixed-point theorem.

private
 module Fix₀ {a p q} {A : Set a} {P : Partiality-algebra p q A} where

  open Partiality-algebra P
  open PAP P

  -- Repeated composition of a monotone function with itself.

  comp : [ P  P ]⊑    [ P  P ]⊑
  comp f zero    = id⊑
  comp f (suc n) = f ∘⊑ comp f n

  -- Pre-composition with the function is equal to post-composition
  -- with the function.

  pre≡post :  f n  comp f n ∘⊑ f  f ∘⊑ comp f n
  pre≡post f zero    = f  
  pre≡post f (suc n) =
    (f ∘⊑ comp f n) ∘⊑ f  ≡⟨ ∘⊑-assoc f (comp f n) 
    f ∘⊑ (comp f n ∘⊑ f)  ≡⟨ cong (f ∘⊑_) $ pre≡post f n ⟩∎
    f ∘⊑ (f ∘⊑ comp f n)  

  -- Repeated application of a monotone function to never.

  app : [ P  P ]⊑    Type
  app f n = function (comp f n) never

  -- An increasing sequence consisting of repeated applications of the
  -- given monotone function to never.

  fix-sequence : [ P  P ]⊑  Increasing-sequence
  fix-sequence f = app f , fix-sequence-increasing
    where
    abstract
      fix-sequence-increasing :
         n  function (comp f n) never  function (f ∘⊑ comp f n) never
      fix-sequence-increasing n =
        function (comp f n) never               ⊑⟨ monotone (comp f n) (never⊑ (function f never)) 
        function (comp f n) (function f never)  ⊑⟨⟩
        function (comp f n ∘⊑ f) never          ≡⟨ cong  g  function g never) $ pre≡post f n ⟩⊑
        function (f ∘⊑ comp f n) never          

  -- Taking the tail of this sequence amounts to the same thing as
  -- applying the function to each element in the sequence.

  tailˢ-fix-sequence :
    (f : [ P  P ]⊑) 
    tailˢ (fix-sequence f)  [ f $ fix-sequence f ]-inc
  tailˢ-fix-sequence f =
    _↔_.to equality-characterisation-increasing λ _  refl

  -- The sequence has the same least upper bound as the sequence you get
  -- if you apply the function to each element of the sequence.

  ⨆-fix-sequence :
    (f : [ P  P ]⊑) 
     (fix-sequence f)   [ f $ fix-sequence f ]-inc
  ⨆-fix-sequence f =
     (fix-sequence f)            ≡⟨ sym $ ⨆tail≡⨆ _ 
     (tailˢ (fix-sequence f))    ≡⟨ cong  (tailˢ-fix-sequence f) ⟩∎
     [ f $ fix-sequence f ]-inc  

  -- A fixpoint combinator.

  fix : [ P  P ]⊑  Type
  fix f =  (fix-sequence f)

  -- The fixpoint combinator produces fixpoints for ω-continuous
  -- arguments.

  fix-is-fixpoint-combinator :
    ( : [ P  P ]) 
    let f : [ P  P ]⊑
        f = [_⟶_].monotone-function 
    in fix f  function f (fix f)
  fix-is-fixpoint-combinator  =
    fix f                            ≡⟨⟩
     (fix-sequence f)               ≡⟨ ⨆-fix-sequence f 
     [ f $ fix-sequence f ]-inc     ≡⟨ sym $ [_⟶_].ω-continuous  _ 
    function f ( (fix-sequence f))  ≡⟨⟩
    function f (fix f)               
    where
    f : [ P  P ]⊑
    f = [_⟶_].monotone-function 

  -- The result of the fixpoint combinator is smaller than or equal to
  -- every post-fixpoint.

  fix-is-least :
    (f : [ P  P ]⊑) 
     x  function f x  x  fix f  x
  fix-is-least f x fx⊑x = least-upper-bound _ _ lemma
    where
    lemma :  n  function (comp f n) never  x
    lemma zero    = never⊑ x
    lemma (suc n) =
      function (f ∘⊑ comp f n) never          ⊑⟨⟩
      function f (function (comp f n) never)  ⊑⟨ monotone f (lemma n) 
      function f x                            ⊑⟨ fx⊑x ⟩■
      x                                       

  -- A restricted homomorphism property.

  comp-∘ :  f n  comp (f ∘⊑ f) n  comp f n ∘⊑ comp f n
  comp-∘ f zero    = id⊑  
  comp-∘ f (suc n) =
    (f ∘⊑ f) ∘⊑ comp (f ∘⊑ f) n         ≡⟨ cong ((f ∘⊑ f) ∘⊑_) (comp-∘ f n) 
    (f ∘⊑ f) ∘⊑ (comp f n ∘⊑ comp f n)  ≡⟨ lemma f f (comp f n) _ 
    f ∘⊑ ((f ∘⊑ comp f n) ∘⊑ comp f n)  ≡⟨ cong ((_∘⊑ comp f n)  (f ∘⊑_)) $ sym $ pre≡post f n 
    f ∘⊑ ((comp f n ∘⊑ f) ∘⊑ comp f n)  ≡⟨ sym $ lemma f (comp f n) f _ ⟩∎
    (f ∘⊑ comp f n) ∘⊑ (f ∘⊑ comp f n)  
    where
    lemma : (f g h k : [ P  P ]⊑) 
            (f ∘⊑ g) ∘⊑ (h ∘⊑ k)  f ∘⊑ ((g ∘⊑ h) ∘⊑ k)
    lemma f g h k =
      (f ∘⊑ g) ∘⊑ (h ∘⊑ k)  ≡⟨ ∘⊑-assoc f g 
      f ∘⊑ (g ∘⊑ (h ∘⊑ k))  ≡⟨ cong (f ∘⊑_) $ ∘⊑-assoc g h ⟩∎
      f ∘⊑ ((g ∘⊑ h) ∘⊑ k)  

  -- The function comp f is homomorphic with respect to _+_/_∘⊑_.

  comp-+∘ :  f m {n}  comp f (m + n)  comp f m ∘⊑ comp f n
  comp-+∘ f zero    {n} = comp f n  
  comp-+∘ f (suc m) {n} =
    f ∘⊑ comp f (m + n)          ≡⟨ cong (f ∘⊑_) $ comp-+∘ f m 
    f ∘⊑ (comp f m ∘⊑ comp f n)  ≡⟨ ∘⊑-assoc f (comp f m) ⟩∎
    (f ∘⊑ comp f m) ∘⊑ comp f n  

  -- Taking steps that are "twice as large" does not affect the end
  -- result.

  fix-∘ : (f : [ P  P ]⊑)  fix (f ∘⊑ f)  fix f
  fix-∘ f = antisymmetry
    (least-upper-bound _ _ λ n 
       function (comp (f ∘⊑ f) n) never       ≡⟨ cong  f  function f never) $ comp-∘ f n ⟩⊑
       function (comp f n ∘⊑ comp f n) never  ≡⟨ cong  f  function f never) $ sym $ comp-+∘ f n ⟩⊑
       function (comp f (n + n)) never        ⊑⟨ upper-bound (fix-sequence f) (n + n) ⟩■
        (fix-sequence f)                     )
    (⨆-mono λ n 
       function (comp f n) never                        ⊑⟨ monotone (comp f n) (never⊑ _) 
       function (comp f n) (function (comp f n) never)  ⊑⟨⟩
       function (comp f n ∘⊑ comp f n) never            ≡⟨ cong  f  function f never) $ sym $ comp-∘ f n ⟩⊑
       function (comp (f ∘⊑ f) n) never                 )

open Fix₀

-- N-ary Scott induction.

module N-ary
  (open Partiality-algebra)
  {a p q r} n
  (As : Fin n  Set a)
  (Ps :  i  Partiality-algebra p q (As i))
  (P : (∀ i  Type (Ps i))  Set r)
  (P⊥ : P  i  never (Ps i)))
  (P⨆ : (ss :  i  Increasing-sequence (Ps i)) 
        (∀ n  P  i  _[_] (Ps i) (ss i) n)) 
        P  i   (Ps i) (ss i)))
  (fs :  i  [ Ps i  Ps i ]⊑)
  where

  -- Generalised.

  fix-induction′ :
    (∀ n  P  i  app (fs i) n)  P  i  app (fs i) (suc n))) 
    P (fix  fs)
  fix-induction′ step =                       $⟨ lemma 
    (∀ n  P  i  app (fs i) n))            ↝⟨ P⨆ _ 
    P  i   (Ps i) (fix-sequence (fs i)))  ↝⟨ id ⟩□
    P (fix  fs)                              
    where
    lemma :  n  P  i  function (comp (fs i) n) (never (Ps i)))
    lemma zero    = P⊥
    lemma (suc n) =                             $⟨ lemma n 
      P  i  app (fs i) n)                    ↝⟨ step n ⟩□
      P  i  function (fs i) (app (fs i) n))  

  -- Basic.

  fix-induction :
    (∀ xs  P xs  P  i  function (fs i) (xs i))) 
    P (fix  fs)
  fix-induction step =
    fix-induction′  n  step  i  app (fs i) n))

open N-ary public

module Fix {a p q} {A : Set a} {P : Partiality-algebra p q A} where

  open Partiality-algebra P

  -- Unary Scott induction.

  fix-induction₁ :
     {r}
    (Q : Type  Set r) 
    Q never 
    (∀ s  (∀ n  Q (s [ n ]))  Q ( s)) 
    (f : [ P  P ]⊑) 
    (∀ x  Q x  Q (function f x)) 
    Q (fix f)
  fix-induction₁ Q Q⊥ Q⨆ f step =
    fix-induction
      1
      [ const A ,        ⊥-elim    ]
      [ const P ,  i  ⊥-elim i) ]
      (Q  (_$ fzero))
      Q⊥
      (Q⨆  (_$ fzero))
      [ const f ,  x  ⊥-elim x) ]
      (step  (_$ fzero))

  open Fix₀ {P = P} public

open Fix public