Tile Sequence by trigott

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 LP
import Data.List.All as All
open All using (All)
import Data.List.Any as Any
open Any using (Any)
open Any.Membership-≡
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
open import Data.Nat

open import Algebra
import Data.Nat.Properties as Nat
private
  module CS = CommutativeSemiring Nat.commutativeSemiring

open import Data.Sum

RW∷ : ∀ {n} → Vec Tile n → Vec Tile (suc (suc n))
RW∷ l = R Vec.∷ W Vec.∷ l

W∷ : ∀ {n} → Vec Tile n → Vec Tile (suc n)
W∷ l = W Vec.∷ l

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

infixr 5 _All++_

_All++_ : {A : Set} {P : A → Set} {xs ys : List A}
        → All P xs
        → All P ys
        → All P (xs List.++ ys)
All.[] All++ r = r
(px All.∷ l) All++ r = px All.∷ (l All++ r)

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) =
  ((R ∷ []) {λ ()}) All.∷
  ((W ∷ []) {λ ()}) All.∷ All.[]
generate-seqs-generate-valid-tile-seq (suc (suc n)) =
  (g (generate-seqs-generate-valid-tile-seq (suc n))) All++
  (f (generate-seqs-generate-valid-tile-seq n))
  where f : ∀ {n} {l : List (Vec Tile n)} → All ValidTileSeq l → All ValidTileSeq (List.map RW∷ l)
        f All.[] = All.[]
        f (px All.∷ p) = ((R ∷ (W ∷ px) {λ ()}) {λ ()}) All.∷ f p
        g : ∀ {n} {l : List (Vec Tile n)} → All ValidTileSeq l → All ValidTileSeq (List.map W∷ l)
        g All.[] = All.[]
        g (px All.∷ p) = ((W ∷ px) {λ ()}) All.∷ g p

++-any-r : ∀ {A : Set} {P : A → Set} {r : List A} (l : List A) → Any P r → Any P (l List.++ r)
++-any-r {r = r} List.[] prf = prf
++-any-r {r = r} (x List.∷ l) prf = Any.there (++-any-r l prf)

++-any-l : ∀ {a p} {A : Set a} {P : A → Set p} {l : List A} (r : List A) → Any P l → Any P (l List.++ r)
++-any-l {l = List.[]} r ()
++-any-l {l = (x List.∷ l)} r (Any.here px) = Any.here {xs = l List.++ r} px
++-any-l {l = (x List.∷ l)} r (Any.there prf) = Any.there (++-any-l r prf)

split-any : {A : Set} {P : A → Set} (l r : List A) → Any P (l List.++ r) → Any P l ⊎ Any P r
split-any List.[] r p = inj₂ p
split-any (x List.∷ l) r (Any.here px) = inj₁ (Any.here px)
split-any (x List.∷ l) r (Any.there p) with split-any l r p
split-any (x List.∷ l) r (Any.there p) | inj₁ prf = inj₁ (Any.there {x = x} prf)
split-any (x List.∷ l) r (Any.there p) | inj₂ prf = inj₂ prf

any-≡-cong : ∀ {a b} {A : Set a} {B : Set b} {l : List A} {x} (f : A → B)
           → Any (_≡_ x) l
           → Any (_≡_ (f x)) (List.map f l)
any-≡-cong f (Any.here refl) = Any.here refl
any-≡-cong f (Any.there p) = Any.there (any-≡-cong f p)

valid-tile-seq-included-generate-seqs : ∀ n seq → ValidTileSeq seq → seq ∈ generate-seqs n
valid-tile-seq-included-generate-seqs .0 Vec.[] p = Any.here refl
valid-tile-seq-included-generate-seqs .1 (Vec._∷_ {zero} W Vec.[]) p = Any.there (Any.here refl)
valid-tile-seq-included-generate-seqs .1 (Vec._∷_ {zero} R Vec.[]) p = Any.here refl
valid-tile-seq-included-generate-seqs .(suc (suc n)) (Vec._∷_ {suc n} W seq) (.W ∷ p) =
  ++-any-l (List.map RW∷ (generate-seqs n))
           (any-≡-cong W∷
                       (valid-tile-seq-included-generate-seqs (suc n) seq p))
valid-tile-seq-included-generate-seqs .(suc (suc n)) (Vec._∷_ {suc n} R (W Vec.∷ seq)) (.R ∷ (.W ∷ p)) =
  ++-any-r (List.map W∷ (generate-seqs (suc n)))
           (any-≡-cong RW∷ (valid-tile-seq-included-generate-seqs n seq p))
valid-tile-seq-included-generate-seqs .(suc (suc n)) (Vec._∷_ {suc n} R (R Vec.∷ seq)) ((.R ∷ p) {q}) with q refl
... | ()

h : ∀ {x y y'} → y ≡ y' → Fib x y → Fib x y'
h refl p = p

length∘generate-seqs-is-FibFunc : FibFunc (List.length ∘ generate-seqs)
length∘generate-seqs-is-FibFunc zero = Fib0
length∘generate-seqs-is-FibFunc (suc zero) = Fib1
length∘generate-seqs-is-FibFunc (suc (suc n))
  -- rewrite (LP.length-++ (List.map W∷ (generate-seqs (suc n)))
  --                       {ys = List.map RW∷ (generate-seqs n)})
  --       | (LP.length-map W∷ (generate-seqs (suc n)))
  --       | (LP.length-map RW∷ (generate-seqs n))
  = h (sym eq) (FibN (length∘generate-seqs-is-FibFunc (suc n))
              (length∘generate-seqs-is-FibFunc n))
  where eq : List.length (List.map W∷ (generate-seqs (suc n)) List.++
                          List.map RW∷ (generate-seqs n)) ≡
             List.length (generate-seqs (suc n)) + List.length (generate-seqs n)
        eq = begin
          List.length (List.map W∷ (generate-seqs (suc n)) List.++
                       List.map RW∷ (generate-seqs n)) ≡⟨ LP.length-++ (List.map W∷ (generate-seqs (suc n)))
                                                                       {ys = List.map RW∷ (generate-seqs n)} ⟩
          List.length (List.map W∷ (generate-seqs (suc n))) +
            List.length (List.map RW∷ (generate-seqs n)) ≡⟨ cong (λ x → x + (List.length (List.map RW∷ (generate-seqs n))))
                                                                 (LP.length-map W∷ (generate-seqs (suc n))) ⟩
          List.length (generate-seqs (suc n)) +
            List.length (List.map RW∷ (generate-seqs n)) ≡⟨ cong (λ x → (List.length (generate-seqs (suc n))) + x)
                                                                 (LP.length-map RW∷ (generate-seqs n)) ⟩
          List.length (generate-seqs (suc n)) + List.length (generate-seqs n)
          ∎