# Tile Sequence

## Description

There are red(R) tiles and white(W) tiles. Generate all size n "valid" tile sequences. "valid" tile sequence have no adjacent red tiles.

example)
[] is valid size 0 tile sequence
[W] is valid size 1 tile sequence
[R] is valid size 1 tile sequence
[RWWW] is valid size 4 tile sequence
[WRWRWR] is valid size 6 tile sequence
[WRRW] is invalid size 4 tile sequence

And, show that the numerical sequence of the number of all size n "valid" tile sequences is Fibonacci number.

```module Definitions where

open import Data.Nat using (ℕ; suc; _+_)
import Data.List as List
open List using (List)
import Data.Vec as Vec
open Vec using (Vec)
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.PropositionalEquality

data Tile : Set where
W : Tile -- White Tile
R : Tile -- Red Tile

infix 4 _≟_

_≟_ : Decidable {A = Tile} _≡_
W ≟ W = yes refl
R ≟ R = yes refl
W ≟ R = no λ ()
R ≟ W = no λ ()

data ValidTileSeq : {n : ℕ} → Vec Tile n → Set where
[] : ValidTileSeq Vec.[]
_∷_ : ∀ {n} {vs : Vec Tile n}
→ (t : Tile)
→ ValidTileSeq vs
→ {≢rr : t List.∷ List.take 1 (Vec.toList vs) ≢ R List.∷ R List.∷ List.[]}
→ ValidTileSeq (t Vec.∷ vs)

data Fib : ℕ → ℕ → Set where
Fib0 : Fib 0 1
Fib1 : Fib 1 2
FibN : ∀ {n x y} → Fib (suc n) x → Fib n y → Fib (suc (suc n)) (x + y)

FibFunc : (ℕ → ℕ) → Set
FibFunc f = ∀ n → Fib n (f n)
```

```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.All as All
open All using (All)
import Data.List.Any as Any
open Any using (Any)
open Any.Membership-≡

postulate
generate-seqs : ∀ n → List (Vec Tile n)

generate-seqs-generate-valid-tile-seq : ∀ n → All ValidTileSeq (generate-seqs n)

valid-tile-seq-included-generate-seqs : ∀ n seq → ValidTileSeq seq → seq ∈ generate-seqs n

length∘generate-seqs-is-FibFunc : FibFunc (List.length ∘ generate-seqs)
```

## Verifier

```module Verifier where

open import Definitions
open import Theorem
open import Function
import Data.Vec as Vec
open Vec using (Vec)
import Data.List as List
open List using (List)
import Data.List.All as All
open All using (All)
import Data.List.Any as Any
open Any using (Any)
open Any.Membership-≡

verify₁ : ∀ n → All ValidTileSeq (generate-seqs n)
verify₁ = generate-seqs-generate-valid-tile-seq

verify₂ : ∀ n seq → ValidTileSeq seq → seq ∈ generate-seqs n
verify₂ = valid-tile-seq-included-generate-seqs

verify₃ : FibFunc (List.length ∘ generate-seqs)
verify₃ = length∘generate-seqs-is-FibFunc
```

## Proofs

Rank Prover Size Date
1 trigott 4310 2014-11-20 01:46:09 JST
2 notogawa 4522 2013-09-29 22:57:26 JST