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))
  rss-is-valid : All ValidTileSeq rss
  rss-is-valid = R∷W∷valid-seqs→valid-seqs p₂
  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₁