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
data Z (O : Set) : Set where
[0] : ∞ (Z O) → Z O
[1] : O → Z O
data O : Set where
↓ : Z O → O
01^ω : O
01^ω = ↓ ([0] (♯ [1] 01^ω))
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)
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)
inconsistency : Theorem → ⊥
inconsistency theorem = theorem 01^ω (refl , refl , proof)
where
proof : tail (tail ⟦ 01^ω ⟧O) ≈ ⟦ 01^ω ⟧O
proof = 0b ∷ ♯ (1b ∷ ♯ proof)
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)
head-cong : ∀ {A} {xs ys : Stream A} → xs ≈ ys → head xs ≡ head ys
head-cong (x ∷ xs≈) = refl
tail-cong : ∀ {A} {xs ys : Stream A} → xs ≈ ys → tail xs ≈ tail ys
tail-cong (x ∷ xs≈) = ♭ xs≈
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₃)