module ThueMorse where
open import Coinduction
open import Data.Bool using (Bool; not); open Data.Bool.Bool
open import Data.Stream as S using (Stream; _≈_)
open S.Stream; open S._≈_
open import Function
open import Relation.Binary
import Relation.Binary.EqReasoning as EqReasoning
private
module SS {A : Set} = Setoid (S.setoid A)
open module EqR {A : Set} = EqReasoning (S.setoid A)
using (begin_; _∎) renaming (_≈⟨_⟩_ to _≈⟨_⟩′_)
data Chunks : Set where
next : (m : Chunks) → Chunks
cons : (m : ∞ Chunks) → 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′
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_
_⋎C_ : Chunks → Chunks → Chunks
next m ⋎C next m′ = next (m ⋎C m′)
next m ⋎C cons m′ = next (m ⋎C cons m′)
cons m ⋎C m′ = cons (♯ (m′ ⋎C ♭ 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_
_⋎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
castW : ∀ {m m′ A} → m ≈C m′ → StreamW m A → StreamW m′ A
castW (next m≈m′) [ xs ] = [ cast m≈m′ xs ]
castW (cons m≈m′) (x ∷ xs) = x ∷ castW (♭ m≈m′) xs
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) = 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
[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) ]
infix 4 _≈[_]P_ _≈[_]W_
infixr 2 _≈⟨_⟩P_ _≈⟨_⟩_
data _≈[_]P_ : {A : Set} → Stream A → Chunks → Stream A → Set₁ where
[_] : ∀ {m A} {xs ys : Stream A}
(xs≈ys : ∞ (xs ≈[ m ]P ys)) → xs ≈[ next m ]P ys
_∷_ : ∀ {m A} (x : A) {xs ys}
(xs≈ys : ♭ xs ≈[ ♭ m ]P ♭ ys) → x ∷ xs ≈[ cons m ]P x ∷ ys
tail : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) →
S.tail xs ≈[ tailC m ]P S.tail ys
evens : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) →
S.evens xs ≈[ evensC m ]P S.evens ys
odds : ∀ {m A} {xs ys : Stream A} (xs≈ys : xs ≈[ m ]P ys) →
S.odds xs ≈[ oddsC m ]P S.odds ys
_⋎_ : ∀ {m m′ A} {xs xs′ ys ys′ : Stream A}
(xs≈ys : xs ≈[ m ]P ys) (xs′≈ys′ : xs′ ≈[ m′ ]P ys′) →
(xs ⟨ S._⋎_ ⟩ xs′) ≈[ m ⋎C m′ ]P (ys ⟨ S._⋎_ ⟩ ys′)
map : ∀ {m A B} (f : A → B) {xs ys : Stream A}
(xs≈ys : xs ≈[ m ]P ys) → S.map f xs ≈[ m ]P S.map f ys
cast : ∀ {m m′ A} (ok : m ≈C m′) {xs ys : Stream A}
(xs≈ys : xs ≈[ m ]P ys) → xs ≈[ m′ ]P ys
_≈⟨_⟩P_ : ∀ {m A} xs {ys zs : Stream A}
(xs≈ys : xs ≈[ m ]P ys) (ys≈zs : ys ≈ zs) → xs ≈[ m ]P zs
_≈⟨_⟩_ : ∀ {m A} xs {ys zs : Stream A}
(xs≈ys : xs ≈ ys) (ys≈zs : ys ≈[ m ]P zs) → xs ≈[ m ]P zs
data _≈[_]W_ : {A : Set} → Stream A → Chunks → Stream A → Set₁ where
[_] : ∀ {m A} {xs ys : Stream A}
(xs≈ys : xs ≈[ m ]P ys) → xs ≈[ next m ]W ys
_∷_ : ∀ {m A} (x : A) {xs ys}
(xs≈ys : ♭ xs ≈[ ♭ m ]W ♭ ys) → x ∷ xs ≈[ cons m ]W x ∷ ys
program≈ : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈[ m ]P ys
program≈ [ xs≈ys ] = [ ♯ xs≈ys ]
program≈ (x ∷ xs≈ys) = x ∷ program≈ xs≈ys
tail-congW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys →
S.tail xs ≈[ tailC m ]W S.tail ys
tail-congW [ xs≈ys ] = [ tail xs≈ys ]
tail-congW (x ∷ xs≈ys) = xs≈ys
mutual
evens-congW : ∀ {m A} {xs ys : Stream A} →
xs ≈[ m ]W ys → S.evens xs ≈[ evensC m ]W S.evens ys
evens-congW [ xs≈ys ] = [ evens xs≈ys ]
evens-congW (x ∷ xs≈ys) = x ∷ odds-congW xs≈ys
odds-congW : ∀ {m A} {xs ys : Stream A} →
xs ≈[ m ]W ys → S.odds xs ≈[ oddsC m ]W S.odds ys
odds-congW [ xs≈ys ] = [ odds xs≈ys ]
odds-congW (x ∷ xs≈ys) = evens-congW xs≈ys
infixr 5 _⋎-congW_
_⋎-congW_ : ∀ {m m′ A} {xs xs′ ys ys′ : Stream A} →
xs ≈[ m ]W ys → xs′ ≈[ m′ ]W ys′ →
(xs ⟨ S._⋎_ ⟩ xs′) ≈[ m ⋎C m′ ]W (ys ⟨ S._⋎_ ⟩ ys′)
[ xs≈ys ] ⋎-congW [ xs′≈ys′ ] = [ xs≈ys ⋎ xs′≈ys′ ]
[ xs≈ys ] ⋎-congW (y ∷ xs′≈ys′) = [ xs≈ys ⋎ program≈ (y ∷ xs′≈ys′) ]
(x ∷ xs≈ys) ⋎-congW xs′≈ys′ = x ∷ xs′≈ys′ ⋎-congW xs≈ys
map-congW : ∀ {m A B} (f : A → B) {xs ys : Stream A} →
xs ≈[ m ]W ys → S.map f xs ≈[ m ]W S.map f ys
map-congW f [ xs≈ys ] = [ map f xs≈ys ]
map-congW f (x ∷ xs≈ys) = f x ∷ map-congW f xs≈ys
cast-congW : ∀ {m m′ A} (ok : m ≈C m′) {xs ys : Stream A} →
xs ≈[ m ]W ys → xs ≈[ m′ ]W ys
cast-congW (next m≈m′) [ xs≈ys ] = [ cast m≈m′ xs≈ys ]
cast-congW (cons m≈m′) (x ∷ xs≈ys) = x ∷ cast-congW (♭ m≈m′) xs≈ys
transPW : ∀ {m A} {xs ys zs : Stream A} →
xs ≈[ m ]W ys → ys ≈ zs → xs ≈[ m ]W zs
transPW [ xs≈ys ] ys≈zs = [ _ ≈⟨ xs≈ys ⟩P ys≈zs ]
transPW (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ transPW xs≈ys (♭ ys≈zs)
transW : ∀ {m A} {xs ys zs : Stream A} →
xs ≈ ys → ys ≈[ m ]W zs → xs ≈[ m ]W zs
transW (x ∷ xs≈ys) [ ys≈zs ] = [ _ ≈⟨ x ∷ xs≈ys ⟩ ys≈zs ]
transW (x ∷ xs≈ys) (.x ∷ ys≈zs) = x ∷ transW (♭ xs≈ys) ys≈zs
whnf≈ : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]P ys → xs ≈[ m ]W ys
whnf≈ [ xs ] = [ ♭ xs ]
whnf≈ (x ∷ xs) = x ∷ whnf≈ xs
whnf≈ (tail xs) = tail-congW (whnf≈ xs)
whnf≈ (evens xs) = evens-congW (whnf≈ xs)
whnf≈ (odds xs) = odds-congW (whnf≈ xs)
whnf≈ (xs ⋎ ys) = whnf≈ xs ⋎-congW whnf≈ ys
whnf≈ (map f xs) = map-congW f (whnf≈ xs)
whnf≈ (cast m≈m′ xs) = cast-congW m≈m′ (whnf≈ xs)
whnf≈ (xs ≈⟨ xs≈ys ⟩P ys≈zs) = transPW (whnf≈ xs≈ys) ys≈zs
whnf≈ (xs ≈⟨ xs≈ys ⟩ ys≈zs) = transW xs≈ys (whnf≈ ys≈zs)
mutual
soundW : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]W ys → xs ≈ ys
soundW [ xs≈ys ] = soundP xs≈ys
soundW (x ∷ xs≈ys) = x ∷ ♯ soundW xs≈ys
soundP : ∀ {m A} {xs ys : Stream A} → xs ≈[ m ]P ys → xs ≈ ys
soundP xs≈ys = soundW (whnf≈ xs≈ys)
program-hom : ∀ {m A} (xs : StreamW m A) → ⟦ program xs ⟧P ≈ ⟦ xs ⟧W
program-hom [ xs ] = SS.refl
program-hom (x ∷ xs) = x ∷ ♯ program-hom xs
mutual
tailW-hom : ∀ {A : Set} {m} (xs : StreamW m A) →
⟦ tailW xs ⟧W ≈ S.tail ⟦ xs ⟧W
tailW-hom [ xs ] = tail-hom xs
tailW-hom (x ∷ xs) = SS.refl
tail-hom : ∀ {A : Set} {m} (xs : StreamP m A) →
⟦ tail xs ⟧P ≈ S.tail ⟦ xs ⟧P
tail-hom xs = tailW-hom (whnf xs)
mutual
infixr 5 _⋎W-hom_ _⋎-hom_
_⋎W-hom_ : ∀ {A : Set} {m m′} (xs : StreamW m A) (ys : StreamW m′ A) →
⟦ xs ⋎W ys ⟧W ≈[ m ⋎C m′ ]P (⟦ xs ⟧W ⟨ S._⋎_ ⟩ ⟦ ys ⟧W)
(x ∷ xs) ⋎W-hom ys = x ∷ ys ⋎W-hom xs
[ xs ] ⋎W-hom [ ys ] = [ ♯ (xs ⋎-hom ys) ]
[ xs ] ⋎W-hom (y ∷ ys′) =
[ ♯ (⟦ xs ⋎ program ys ⟧P ≈⟨ xs ⋎-hom program ys ⟩P (begin
(⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ program ys ⟧P) ≈⟨ SS.refl ⟨ S._⋎-cong_ ⟩ program-hom ys ⟩′
(⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ ys ⟧W) ∎)) ]
where ys = y ∷ ys′
_⋎-hom_ : ∀ {A : Set} {m m′} (xs : StreamP m A) (ys : StreamP m′ A) →
⟦ xs ⋎ ys ⟧P ≈[ m ⋎C m′ ]P (⟦ xs ⟧P ⟨ S._⋎_ ⟩ ⟦ ys ⟧P)
xs ⋎-hom ys = whnf xs ⋎W-hom whnf ys
mutual
evensW-hom : ∀ {A : Set} {m} (xs : StreamW m A) →
⟦ evensW xs ⟧W ≈ S.evens ⟦ xs ⟧W
evensW-hom [ xs ] = evens-hom xs
evensW-hom (x ∷ xs) = x ∷ ♯ oddsW-hom xs
evens-hom : ∀ {A : Set} {m} (xs : StreamP m A) →
⟦ evens xs ⟧P ≈ S.evens ⟦ xs ⟧P
evens-hom xs = evensW-hom (whnf xs)
oddsW-hom : ∀ {A : Set} {m} (xs : StreamW m A) →
⟦ oddsW xs ⟧W ≈ S.odds ⟦ xs ⟧W
oddsW-hom [ xs ] = odds-hom xs
oddsW-hom (x ∷ xs) = evensW-hom xs
odds-hom : ∀ {A : Set} {m} (xs : StreamP m A) →
⟦ odds xs ⟧P ≈ S.odds ⟦ xs ⟧P
odds-hom xs = oddsW-hom (whnf xs)
mutual
mapW-hom : ∀ {A B : Set} {m} (f : A → B) (xs : StreamW m A) →
⟦ mapW f xs ⟧W ≈ S.map f ⟦ xs ⟧W
mapW-hom f [ xs ] = map-hom f xs
mapW-hom f (x ∷ xs) = f x ∷ ♯ mapW-hom f xs
map-hom : ∀ {A B : Set} {m} (f : A → B) (xs : StreamP m A) →
⟦ map f xs ⟧P ≈ S.map f ⟦ xs ⟧P
map-hom f xs = mapW-hom f (whnf xs)
mutual
castW-hom : ∀ {m m′ A} (m≈m′ : m ≈C m′) (xs : StreamW m A) →
⟦ castW m≈m′ xs ⟧W ≈ ⟦ xs ⟧W
castW-hom (next m≈m′) [ xs ] = cast-hom m≈m′ xs
castW-hom (cons m≈m′) (x ∷ xs) = x ∷ ♯ castW-hom (♭ m≈m′) xs
cast-hom : ∀ {m m′ A} (m≈m′ : m ≈C m′) (xs : StreamP m A) →
⟦ cast m≈m′ xs ⟧P ≈ ⟦ xs ⟧P
cast-hom m≈m′ xs = castW-hom m≈m′ (whnf xs)
rhs : Stream Bool → Stream Bool
rhs bs = false ∷ ♯ (S.map not (S.evens bs) ⟨ S._⋎_ ⟩ S.tail bs)
correct : ⟦ thueMorse ⟧P ≈[ [cn]³[ccn]ω ]P rhs ⟦ thueMorse ⟧P
correct = false ∷ [ ♯ cast lemma (
⟦ cast lemma (map not (evens thueMorse) ⋎ tail thueMorse) ⟧P ≈⟨ cast-hom lemma (map not (evens thueMorse) ⋎ tail thueMorse) ⟩
⟦ map not (evens thueMorse) ⋎ tail thueMorse ⟧P ≈⟨ map not (evens thueMorse) ⋎-hom tail thueMorse ⟩P (begin
(⟦ map not (evens thueMorse) ⟧P ⟨ S._⋎_ ⟩ ⟦ tail thueMorse ⟧P) ≈⟨ SS.trans (map-hom not (evens thueMorse))
(S.map-cong not (evens-hom thueMorse))
⟨ S._⋎-cong_ ⟩
tail-hom thueMorse ⟩′
(S.map not (S.evens ⟦ thueMorse ⟧P) ⟨ S._⋎_ ⟩ S.tail ⟦ thueMorse ⟧P) ∎ )) ]
unique : ∀ bs bs′ → bs ≈ rhs bs → bs′ ≈ rhs bs′ → bs ≈[ [cn]³[ccn]ω ]P bs′
unique bs bs′ bs≈ bs′≈ =
bs ≈⟨ bs≈ ⟩
rhs bs ≈⟨ false ∷ [ ♯ cast lemma
(map not (evens (unique bs bs′ bs≈ bs′≈))
⋎
tail (unique bs bs′ bs≈ bs′≈)) ] ⟩P (begin
rhs bs′ ≈⟨ SS.sym bs′≈ ⟩′
bs′ ∎)