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

module MuNu where

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

-- 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
 : ∞ (Z O) → Z O
 :    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^ω = ↓ ( (♯  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
 : ∞ O′ → O′
 :   O′ → O′

mutual

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

ZO→O′ : Z O → O′
ZO→O′ ( z) =  (♯ ZO→O′ (♭ z))
ZO→O′ ( o) =  (O→O′ o)

mutual

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

O′→ZO : O′ → Z O
O′→ZO ( o) =  (♯ O′→ZO (♭ o))
O′→ZO ( o) =  (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
⟦  z ⟧Z = 0b ∷ ♯ ⟦ ♭ z ⟧Z
⟦  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
 : ∀ {z} → ∞ (⇑ P (♭ z)) → ⇑ P ( z)
 : ∀ {o} → P o           → ⇑ P ( 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 ( p) (()   , eq₂ , eq₃)
helper ( 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 .( _) ()  eq₂ eq₃ ( p)
hlp .( _) eq₁ eq₂ eq₃ ( 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 ( z) =  (♯ Z-elim P hyp (♭ z))
Z-elim P hyp ( o) =  (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.
```