```------------------------------------------------------------------------
-- 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
[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.
```