------------------------------------------------------------------------
-- An implementation of the Thue-Morse sequence
------------------------------------------------------------------------
-- This module is a variant of ThueMorse. The difference is that, in
-- this module, the cast operation takes an inequality instead of an
-- equality, and that this module does not contain any correctness
-- proofs.
module ThueMorseLeq where
open import Coinduction
open import Data.Bool using (Bool; not); open Data.Bool.Bool
open import Data.Nat using (ℕ); open Data.Nat.ℕ
open import Data.Stream using (Stream; _≈_); open Data.Stream.Stream
open import Data.Vec using (Vec; _∷ʳ_); open Data.Vec.Vec
------------------------------------------------------------------------
-- Chunks
-- A value of type Chunks describes how a stream is generated. Note
-- that an infinite sequence of empty chunks is not allowed.
data Chunks : Set where
-- Start the next chunk.
next : (m : Chunks) → Chunks
-- Cons an element to the current chunk.
cons : (m : ∞ Chunks) → Chunks
-- Inequality of chunks.
infix 4 _≥C_
data _≥C_ : Chunks → Chunks → Set where
next : ∀ {m m′} (m≥m′ : m ≥C m′ ) → next m ≥C next m′
cons : ∀ {m m′} (m≥m′ : ∞ (♭ m ≥C ♭ m′)) → cons m ≥C cons m′
consˡ : ∀ {m m′} (m≥m′ : ♭ m ≥C m′ ) → cons m ≥C m′
------------------------------------------------------------------------
-- Chunk transformers
tailC : Chunks → Chunks
tailC (next m) = next (tailC m)
tailC (cons m) = ♭ m
mutual
evensC : Chunks → Chunks
evensC (next m) = next (evensC m)
evensC (cons m) = cons (♯ oddsC (♭ m))
oddsC : Chunks → Chunks
oddsC (next m) = next (oddsC m)
oddsC (cons m) = evensC (♭ m)
infixr 5 _⋎C_
-- Note that care is taken to create as few and large chunks as
-- possible (see also _⋎W_).
_⋎C_ : Chunks → Chunks → Chunks
next m ⋎C next m′ = next (m ⋎C m′) -- Two chunks in, one out.
next m ⋎C cons m′ = next (m ⋎C cons m′)
cons m ⋎C m′ = cons (♯ (m′ ⋎C ♭ m))
------------------------------------------------------------------------
-- Stream programs
-- StreamP m A encodes programs which generate streams with chunk
-- sizes given by m.
infixr 5 _∷_ _⋎_
data StreamP : Chunks → Set → Set₁ where
[_] : ∀ {m A} (xs : ∞ (StreamP m A)) → StreamP (next m) A
_∷_ : ∀ {m A} (x : A) (xs : StreamP (♭ m) A) → StreamP (cons m) A
tail : ∀ {m A} (xs : StreamP m A) → StreamP (tailC m) A
evens : ∀ {m A} (xs : StreamP m A) → StreamP (evensC m) A
odds : ∀ {m A} (xs : StreamP m A) → StreamP (oddsC m) A
_⋎_ : ∀ {m m′ A} (xs : StreamP m A) (ys : StreamP m′ A) →
StreamP (m ⋎C m′) A
map : ∀ {m A B} (f : A → B) (xs : StreamP m A) → StreamP m B
cast : ∀ {m m′ A} (ok : m ≥C m′) (xs : StreamP m A) → StreamP m′ A
data StreamW : Chunks → Set → Set₁ where
[_] : ∀ {m A} (xs : StreamP m A) → StreamW (next m) A
_∷_ : ∀ {m A} (x : A) (xs : StreamW (♭ m) A) → StreamW (cons m) A
program : ∀ {m A} → StreamW m A → StreamP m A
program [ xs ] = [ ♯ xs ]
program (x ∷ xs) = x ∷ program xs
tailW : ∀ {m A} → StreamW m A → StreamW (tailC m) A
tailW [ xs ] = [ tail xs ]
tailW (x ∷ xs) = xs
mutual
evensW : ∀ {m A} → StreamW m A → StreamW (evensC m) A
evensW [ xs ] = [ evens xs ]
evensW (x ∷ xs) = x ∷ oddsW xs
oddsW : ∀ {m A} → StreamW m A → StreamW (oddsC m) A
oddsW [ xs ] = [ odds xs ]
oddsW (x ∷ xs) = evensW xs
infixr 5 _⋎W_
-- Note: Uses swapping of arguments.
_⋎W_ : ∀ {m m′ A} → StreamW m A → StreamW m′ A → StreamW (m ⋎C m′) A
[ xs ] ⋎W [ ys ] = [ xs ⋎ ys ]
[ xs ] ⋎W (y ∷ ys) = [ xs ⋎ program (y ∷ ys) ]
(x ∷ xs) ⋎W ys = x ∷ ys ⋎W xs
mapW : ∀ {m A B} → (A → B) → StreamW m A → StreamW m B
mapW f [ xs ] = [ map f xs ]
mapW f (x ∷ xs) = f x ∷ mapW f xs
module Cast where
infixr 6 _+_
infixr 5 _++_
_+_ : ℕ → Chunks → Chunks
zero + m = m
suc n + m = cons (♯ (n + m))
_++_ : ∀ {A n m} → Vec A n → StreamP m A → StreamP (n + m) A
[] ++ ys = ys
(x ∷ xs) ++ ys = x ∷ (xs ++ ys)
+ˡ : ∀ {m m′} n → m ≥C m′ → n + m ≥C m′
+ˡ zero m≥m′ = m≥m′
+ˡ (suc n) m≥m′ = consˡ (+ˡ n m≥m′)
castW : ∀ {n m m′ A} → m ≥C m′ → Vec A n → StreamW m A → StreamW m′ A
castW {n} (next m≥m′) xs [ ys ] = [ cast (+ˡ n m≥m′) (xs ++ ys) ]
castW (cons m≥m′) [] (y ∷ ys) = y ∷ castW (♭ m≥m′) [] ys
castW (cons m≥m′) (x ∷ xs) (y ∷ ys) = x ∷ castW (♭ m≥m′) (xs ∷ʳ y) ys
castW (consˡ m≥m′) xs (y ∷ ys) = castW m≥m′ (xs ∷ʳ y) ys
whnf : ∀ {m A} → StreamP m A → StreamW m A
whnf [ xs ] = [ ♭ xs ]
whnf (x ∷ xs) = x ∷ whnf xs
whnf (tail xs) = tailW (whnf xs)
whnf (evens xs) = evensW (whnf xs)
whnf (odds xs) = oddsW (whnf xs)
whnf (xs ⋎ ys) = whnf xs ⋎W whnf ys
whnf (map f xs) = mapW f (whnf xs)
whnf (cast m≥m′ xs) = Cast.castW m≥m′ [] (whnf xs)
mutual
⟦_⟧W : ∀ {m A} → StreamW m A → Stream A
⟦ [ xs ] ⟧W = ⟦ xs ⟧P
⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧W
⟦_⟧P : ∀ {m A} → StreamP m A → Stream A
⟦ xs ⟧P = ⟦ whnf xs ⟧W
------------------------------------------------------------------------
-- The Thue-Morse sequence
[ccn]ω : Chunks
[ccn]ω = cons (♯ cons (♯ next [ccn]ω))
[cn]²[ccn]ω : Chunks
[cn]²[ccn]ω = cons (♯ next (cons (♯ next [ccn]ω)))
[cn]³[ccn]ω : Chunks
[cn]³[ccn]ω = cons (♯ next [cn]²[ccn]ω)
lemma₁ : oddsC [ccn]ω ⋎C [ccn]ω ≥C [ccn]ω
lemma₁ = cons (♯ cons (♯ next (cons (♯ cons (♯ next lemma₁)))))
lemma : evensC [cn]³[ccn]ω ⋎C tailC [cn]³[ccn]ω ≥C [cn]²[ccn]ω
lemma = cons (♯ next (cons (♯ next (cons (♯ cons (♯ next lemma₁))))))
thueMorse : StreamP [cn]³[ccn]ω Bool
thueMorse =
false ∷ [ ♯ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ]