# Tile Sequence by notogawa

```module Theorem where

open import Definitions
open import Function
import Data.Vec as Vec
open Vec using (Vec)
import Data.List as List
open List using (List; _++_)
import Data.List.Properties as List
import Data.List.All as All
open All using (All)
import Data.List.All.Properties as All
import Data.List.Any as Any
open Any using (Any)
import Data.List.Any.Properties as Any
open import Data.Product
open import Data.Sum
open Any.Membership-≡
open import Data.Nat using (ℕ; zero; suc; _+_)
open import Relation.Binary.PropositionalEquality

generate-seqs : ∀ n → List (Vec Tile n)
generate-seqs zero = Vec.[] List.∷ List.[]
generate-seqs (suc zero) = (W Vec.∷ Vec.[]) List.∷ (R Vec.∷ Vec.[]) List.∷ List.[]
generate-seqs (suc (suc n)) = List.map (Vec._∷_ W) (generate-seqs (suc n)) ++
List.map (Vec._∷_ R) (List.map (Vec._∷_ W) (generate-seqs n))

generate-seqs-generate-valid-tile-seq : ∀ n → All ValidTileSeq (generate-seqs n)
generate-seqs-generate-valid-tile-seq zero = [] All.∷ All.[]
generate-seqs-generate-valid-tile-seq (suc zero) = (W ∷ []) {λ ()} All.∷ (R ∷ []) {λ ()} All.∷ All.[]
generate-seqs-generate-valid-tile-seq (suc (suc n)) with generate-seqs-generate-valid-tile-seq (suc n) | generate-seqs-generate-valid-tile-seq n
... | p₁ | p₂ = to All.++↔ ⟨\$⟩ (wss-is-valid , rss-is-valid) where
W∷valid-seq→valid-seq : ∀ {n} {ts : Vec Tile n}
→ ValidTileSeq ts
→ ValidTileSeq (W Vec.∷ ts)
W∷valid-seq→valid-seq = λ {n} {ts} z → (W ∷ z) {λ ()}

W∷valid-seqs→valid-seqs : ∀ {n} {xs : List (Vec Tile n)}
→ All ValidTileSeq xs
→ All ValidTileSeq (List.map (Vec._∷_ W) xs)
W∷valid-seqs→valid-seqs All.[] = All.[]
W∷valid-seqs→valid-seqs (px All.∷ z) = W∷valid-seq→valid-seq px All.∷ W∷valid-seqs→valid-seqs z

R∷W∷valid-seq→valid-seq : ∀ {n} {ts : Vec Tile n}
→ ValidTileSeq ts
→ ValidTileSeq (R Vec.∷ W Vec.∷ ts)
R∷W∷valid-seq→valid-seq = λ z → (R ∷ ((W ∷ z) {λ ()})) {λ ()}

R∷W∷valid-seqs→valid-seqs : ∀ {n} {xs : List (Vec Tile n)}
→ All ValidTileSeq xs
→ All ValidTileSeq (List.map (Vec._∷_ R) (List.map (Vec._∷_ W) xs))
R∷W∷valid-seqs→valid-seqs All.[] = All.[]
R∷W∷valid-seqs→valid-seqs (px All.∷ z) = R∷W∷valid-seq→valid-seq px All.∷ R∷W∷valid-seqs→valid-seqs z
wss = List.map (Vec._∷_ W) (generate-seqs (suc n))
wss-is-valid : All ValidTileSeq wss
wss-is-valid = W∷valid-seqs→valid-seqs p₁
rss = List.map (Vec._∷_ R) (List.map (Vec._∷_ W) (generate-seqs n))
open import Function.Inverse
open Inverse
open import Function.Equality

x∈ys⊎x∈zs→x∈ys++zs : ∀ {n} (x : Vec Tile n) ys zs → x ∈ ys ⊎ x ∈ zs → x ∈ ys ++ zs
x∈ys⊎x∈zs→x∈ys++zs x ys zs p = to Any.++↔ ⟨\$⟩ p
where
open import Function.Inverse
open Inverse
open import Function.Equality

xs∈xss→x∷xs∈map-x∷-xss : ∀ {n} x (xs : Vec Tile n) xss
→ xs ∈ xss → x Vec.∷ xs ∈ List.map (Vec._∷_ x) xss
xs∈xss→x∷xs∈map-x∷-xss x xs .(xs₁ List.∷ xss₁) (Any.here {xs₁} {xss₁} px)
= Any.here (cong (Vec._∷_ x) px)
xs∈xss→x∷xs∈map-x∷-xss x xs .(xs₁ List.∷ xss₁) (Any.there {xs₁} {xss₁} xs∈xss₁)
= Any.there (xs∈xss→x∷xs∈map-x∷-xss x xs xss₁ xs∈xss₁)

valid-tile-seq-included-generate-seqs : ∀ n seq → ValidTileSeq seq → seq ∈ generate-seqs n
valid-tile-seq-included-generate-seqs .0 .Vec.[] [] = Any.here refl
valid-tile-seq-included-generate-seqs .(suc n) .(t Vec.∷ vs) (_∷_ {n} {vs} t valid) with valid-tile-seq-included-generate-seqs n vs valid
valid-tile-seq-included-generate-seqs .(suc 0) .(W Vec.∷ Vec.[]) (W ∷ []) | p₁ = Any.here refl
valid-tile-seq-included-generate-seqs .(suc 0) .(R Vec.∷ Vec.[]) (R ∷ []) | p₁ = Any.there (Any.here refl)
valid-tile-seq-included-generate-seqs .(suc (suc n)) .(W Vec.∷ t Vec.∷ vs) (W ∷ _∷_ {n} {vs} t valid) | p₁ with valid-tile-seq-included-generate-seqs n vs valid
... | p₂ = x∈ys⊎x∈zs→x∈ys++zs (W Vec.∷ t Vec.∷ vs)
(List.map (Vec._∷_ W) (generate-seqs (suc n)))
(List.map (Vec._∷_ R) (List.map (Vec._∷_ W) (generate-seqs n)))
(inj₁
(xs∈xss→x∷xs∈map-x∷-xss W (t Vec.∷ vs) (generate-seqs (suc n)) p₁))
valid-tile-seq-included-generate-seqs .(suc (suc n)) .(R Vec.∷ W Vec.∷ vs) (R ∷ _∷_ {n} {vs} W valid) | p₁ with valid-tile-seq-included-generate-seqs n vs valid
... | p₂ = x∈ys⊎x∈zs→x∈ys++zs (R Vec.∷ W Vec.∷ vs)
(List.map (Vec._∷_ W) (generate-seqs (suc n)))
(List.map (Vec._∷_ R) (List.map (Vec._∷_ W) (generate-seqs n)))
(inj₂
(xs∈xss→x∷xs∈map-x∷-xss R (W Vec.∷ vs)
(List.map (Vec._∷_ W) (generate-seqs n))
(xs∈xss→x∷xs∈map-x∷-xss W vs (generate-seqs n) p₂)))
valid-tile-seq-included-generate-seqs .(suc (suc n)) .(R Vec.∷ R Vec.∷ vs) ((R ∷ _∷_ {n} {vs} R valid) {≢rr}) | p₁ with ≢rr refl
valid-tile-seq-included-generate-seqs .(suc (suc n)) .(R Vec.∷ R Vec.∷ vs) (R ∷ _∷_ {n} {vs} R valid) | p₁ | ()

length∘generate-seqs-is-FibFunc : FibFunc (List.length ∘ generate-seqs)
length∘generate-seqs-is-FibFunc = proj₁ ∘ lemma where
lemma : ∀ n → Fib n ((List.length ∘ generate-seqs) n) × Fib (suc n) ((List.length ∘ generate-seqs) (suc n))
lemma zero = Fib0 , Fib1
lemma (suc n) with lemma n
... | p₁ , p₂
rewrite List.length-++ (List.map (Vec._∷_ W) (generate-seqs (suc n)))
{List.map (Vec._∷_ R) (List.map (Vec._∷_ W) (generate-seqs n))}
| List.length-map (Vec._∷_ W) (generate-seqs (suc n))
| List.length-map (Vec._∷_ R) (List.map (Vec._∷_ W) (generate-seqs n))
| List.length-map (Vec._∷_ W) (generate-seqs n)
= p₂ , FibN p₂ p₁
```