------------------------------------------------------------------------
-- An investigation of nested fixpoints of the form μX.νY.… in Agda
------------------------------------------------------------------------

module MuNu where

open import Coinduction
import Data.Colist as Colist
open import Data.Digit
open import Data.Empty
open import Data.List using (List; _∷_; [])
open import Data.Product
open import Data.Stream
open import Relation.Binary.PropositionalEquality
open import Relation.Nullary

-- Christophe Raffalli discusses (essentially) the type μO. νZ. Z + O
-- in his thesis. If Z is read as zero and O as one, then this type
-- contains bit sequences of the form (0^⋆1)^⋆0^ω.

-- It is interesting to note that currently it is not possible to
-- encode this type directly in Agda. One might believe that the
-- following definition should work. First we define the inner
-- greatest fixpoint:

data Z (O : Set) : Set where
  [0] :  (Z O)  Z O
  [1] :    O     Z O

-- Then we define the outer least fixpoint:

data O : Set where
   : Z O  O

-- However, it is still possible to define values of the form (01)^ω:

01^ω : O
01^ω =  ([0] ( [1] 01^ω))

-- The reason is the way the termination/productivity checker works:
-- it accepts definitions by guarded corecursion as long as the guard
-- contains at least one occurrence of ♯_, no matter how the types
-- involved are defined. In effect ∞ has global reach. The mistake
-- done above was believing that O is defined to be a least fixpoint.
-- The type O really corresponds to νZ. μO. Z + O, i.e. (1^⋆0)^ω:

data O′ : Set where
  [0] :  O′  O′
  [1] :   O′  O′

mutual

  O→O′ : O  O′
  O→O′ ( z) = ZO→O′ z

  ZO→O′ : Z O  O′
  ZO→O′ ([0] z) = [0] ( ZO→O′ ( z))
  ZO→O′ ([1] o) = [1] (O→O′ o)

mutual

  O′→O : O′  O
  O′→O o =  (O′→ZO o)

  O′→ZO : O′  Z O
  O′→ZO ([0] o) = [0] ( O′→ZO ( o))
  O′→ZO ([1] o) = [1] (O′→O o)

-- If O had actually encoded the type μO. νZ. Z + O, then we could
-- have proved the following theorem:

mutual

  ⟦_⟧O : O  Stream Bit
    z ⟧O =  z ⟧Z

  ⟦_⟧Z : Z O  Stream Bit
   [0] z ⟧Z = 0b     z ⟧Z
   [1] o ⟧Z = 1b      o ⟧O

Theorem : Set
Theorem =  o  ¬ (head  o ⟧O  0b × head (tail  o ⟧O)  1b ×
                                      tail (tail  o ⟧O)   o ⟧O)

-- This would have been unfortunate, though:

inconsistency : Theorem  
inconsistency theorem = theorem 01^ω (refl , refl , proof)
  where
  proof : tail (tail  01^ω ⟧O)   01^ω ⟧O
  proof = refl   (refl   proof)

-- Using the following elimination principle we can prove the theorem:

data  {O} (P : O  Set) : Z O  Set where
  [0] :  {z}   ( P ( z))   P ([0] z)
  [1] :  {o}  P o             P ([1] o)

O-Elim : Set₁
O-Elim = (P : O  Set)  (∀ {z}   P z  P ( z))  (o : O)  P o

theorem : O-Elim  Theorem
theorem O-elim = O-elim P helper
  where
  P : O  Set
  P o = ¬ (head  o ⟧O  0b × head (tail  o ⟧O)  1b ×
                              tail (tail  o ⟧O)   o ⟧O)

  helper :  {z}   P z  P ( z)
  helper ([1] p) (()   , eq₂ , eq₃)
  helper ([0] p) (refl , eq₂ , eq₃) =
    hlp _ eq₂ (head-cong eq₃) (tail-cong eq₃) ( p)
    where
    hlp :  z  head  z ⟧Z  1b 
                head (tail  z ⟧Z)  0b 
                tail (tail  z ⟧Z)   z ⟧Z 
                 P z  
    hlp .([0] _) ()  eq₂ eq₃ ([0] p)
    hlp .([1] _) eq₁ eq₂ eq₃ ([1] p) =
      p (eq₂ , head-cong eq₃ , tail-cong eq₃)

-- Fortunately it appears as if we cannot prove this elimination
-- principle. The following code is not accepted by the termination
-- checker:

{-
mutual

  O-elim : O-Elim
  O-elim P hyp (↓ z) = hyp (Z-elim P hyp z)

  Z-elim : (P : O → Set) →
           (∀ {z} → ⇑ P z → P (↓ z)) →
           (z : Z O) → ⇑ P z
  Z-elim P hyp ([0] z) = [0] (♯ Z-elim P hyp (♭ z))
  Z-elim P hyp ([1] o) = [1] (O-elim P hyp o)
-}

-- If hyp were known to be contractive, then the code above would be
-- correct (if not accepted by the termination checker). This is not
-- the case in theorem above.