Chuangjie Xu, 2013

Module for both finite and infinite sequences of boolean ₂

\begin{code}

module Sequence where

open import MiniLibrary
open import Inequality

\end{code}

Infinite sequences are defined as functions:

\begin{code}

₂ℕ : Set
₂ℕ = ℕ → ₂

0̄ : ₂ℕ
0̄ i = ₀
1̄ : ₂ℕ
1̄ i = ₁

\end{code}

Finite sequences are defined as vectros:

\begin{code}

₂Fin : ℕ → Set
₂Fin = Vec ₂

⟨₀⟩ : ₂Fin 
⟨₀⟩ = ₀ ∷ ⟨⟩
⟨₁⟩ : ₂Fin 
⟨₁⟩ = ₁ ∷ ⟨⟩

take : (m : ℕ) → ₂ℕ → ₂Fin m
take  α = ⟨⟩
take (succ n) α = α  ∷ take n (α ∘ succ)

drop : (m : ℕ) → ₂ℕ → ₂ℕ
drop  α = α
drop (succ m) α = drop m (α ∘ succ)

Lemma[drop+] : ∀(n : ℕ) → ∀(α : ₂ℕ) → ∀(i : ℕ) → drop n α i ≡ α (i + n)
Lemma[drop+]         α i = refl
Lemma[drop+] (succ n) α i = Lemma[drop+] n (α ∘ succ) i

isomorphism-₂Fin : ∀(X : Set) → ∀(n : ℕ) → (f : ₂Fin (succ n) → X) →
                    ∃ \(g : ₂ → ₂Fin n → X) →
                     ∀(s : ₂Fin (succ n)) → f s ≡ g (head s) (tail s)
isomorphism-₂Fin X n f = ∃-intro g prf
 where
  g : ₂ → ₂Fin n → X
  g b s = f (b ∷ s)
  prf : ∀(s : ₂Fin (succ n)) → f s ≡ g (head s) (tail s)
  prf (b ∷ s) = refl

max-fin : {n : ℕ} → (f : ₂Fin n → ℕ) →
           ∃ \(m : ℕ) → ∀(s : ₂Fin n) → f s ≤ m
max-fin {} f = ∃-intro (f ⟨⟩) prf
 where
  prf : ∀(s : ₂Fin ) → f s ≤ f ⟨⟩
  prf ⟨⟩ = Lemma[n≤n] (f ⟨⟩)
max-fin {succ n} f = ∃-intro m prf
 where
  g : ₂ → ₂Fin n → ℕ
  g = ∃-witness (isomorphism-₂Fin ℕ n f)
  m₀ : ℕ
  m₀ = ∃-witness (max-fin (g ₀))
  prf₀ : ∀(s : ₂Fin n) → g ₀ s ≤ m₀
  prf₀ = ∃-elim (max-fin (g ₀))
  m₁ : ℕ
  m₁ = ∃-witness (max-fin (g ₁))
  prf₁ : ∀(s : ₂Fin n) → g ₁ s ≤ m₁
  prf₁ = ∃-elim (max-fin (g ₁))
  m : ℕ
  m = maximum m₀ m₁
  prf : ∀(s : ₂Fin (succ n)) → f s ≤ m
  prf (₀ ∷ s) = Lemma[a≤b≤c→a≤c] (prf₀ s) (∧-elim₀ (Lemma[≤-max] m₀ m₁))
  prf (₁ ∷ s) = Lemma[a≤b≤c→a≤c] (prf₁ s) (∧-elim₁ (Lemma[≤-max] m₀ m₁))

\end{code}

Pointwise equality over infinite sequences:

\begin{code}

infixl  _≣_

_≣_ : ₂ℕ → ₂ℕ → Set
α ≣ β = ∀(i : ℕ) → α i ≡ β i

Lemma[≣-take] : ∀(n : ℕ) → ∀(α β : ₂ℕ) → α ≣ β → take n α ≡ take n β
Lemma[≣-take]         α β e = refl
Lemma[≣-take] (succ n) α β e = Lemma[Vec-≡] (e ) (Lemma[≣-take] n (α ∘ succ) (β ∘ succ) (λ i → e (succ i)))

Lemma[≣-drop] : ∀(n : ℕ) → ∀(α β : ₂ℕ) → α ≣ β → drop n α ≣ drop n β
Lemma[≣-drop]         α β e = e
Lemma[≣-drop] (succ n) α β e = Lemma[≣-drop] n (α ∘ succ) (β ∘ succ) (λ i → e (succ i))

\end{code}

"Agree with" relation over infinite sequences, which is an equivalence
relation and a deciable type:

\begin{code}

infixl  _≣[_]_

data _≣[_]_ : ₂ℕ → ℕ → ₂ℕ → Set where
 ≣[zero] : {α β : ₂ℕ} → α ≣[  ] β
 ≣[succ] : {α β : ₂ℕ}{n : ℕ} → α ≣[ n ] β → α n ≡ β n → α ≣[ succ n ] β

refl-≣[] : {n : ℕ}{α : ₂ℕ} → α ≣[ n ] α
refl-≣[] {}      = ≣[zero]
refl-≣[] {succ n} = ≣[succ] refl-≣[] refl

sym-≣[] : {n : ℕ}{α β : ₂ℕ} → α ≣[ n ] β → β ≣[ n ] α
sym-≣[] {}      ≣[zero]        = ≣[zero]
sym-≣[] {succ n} (≣[succ] en e) = ≣[succ] (sym-≣[] en) (sym e)

trans-≣[] : {n : ℕ}{α₀ α₁ α₂ : ₂ℕ} → α₀ ≣[ n ] α₁ → α₁ ≣[ n ] α₂ → α₀ ≣[ n ] α₂
trans-≣[] {}      ≣[zero]        ≣[zero]          = ≣[zero]
trans-≣[] {succ n} (≣[succ] en e) (≣[succ] en' e') = ≣[succ] (trans-≣[] en en') (trans e e')

Lemma[≣[succ]]₀ : {α β : ₂ℕ}{n : ℕ} → α ≣[ succ n ] β → α ≣[ n ] β
Lemma[≣[succ]]₀ (≣[succ] en _) = en

Lemma[≣[succ]]₁ : {α β : ₂ℕ}{n : ℕ} → α ≣[ succ n ] β → α n ≡ β n
Lemma[≣[succ]]₁ (≣[succ] _ e) = e

Lemma[≣[]-decidable] : {m : ℕ} → ∀(α β : ₂ℕ) → decidable (α ≣[ m ] β)
Lemma[≣[]-decidable] {}      α β = in₀ ≣[zero]
Lemma[≣[]-decidable] {succ m} α β = case claim₀ claim₁ IH
 where
  IH : decidable (α ≣[ m ] β)
  IH = Lemma[≣[]-decidable] {m} α β
  claim₀ : α ≣[ m ] β → decidable (α ≣[ succ m ] β)
  claim₀ em = case c₀ c₁ (₂-discrete (α m) (β m))
   where
    c₀ : α m ≡ β m → decidable (α ≣[ succ m ] β)
    c₀ e = in₀ (≣[succ] em e)
    c₁ : ¬ (α m ≡ β m) → decidable (α ≣[ succ m ] β)
    c₁ f = in₁ (λ e → f (Lemma[≣[succ]]₁ e))
  claim₁ : ¬ (α ≣[ m ] β) → decidable (α ≣[ succ m ] β)
  claim₁ f = in₁ (λ e → f(Lemma[≣[succ]]₀ e))

Lemma[≣[]-zero] : ∀{n : ℕ}{α β : ₂ℕ} → α ≣[ succ n ] β → α  ≡ β 
Lemma[≣[]-zero] {}      (≣[succ] ≣[zero] e) = e
Lemma[≣[]-zero] {succ n} (≣[succ] en e)      = Lemma[≣[]-zero] en

Lemma[≣[]-succ] : ∀{n : ℕ}{α β : ₂ℕ} → α ≣[ succ n ] β → (α ∘ succ) ≣[ n ] (β ∘ succ)
Lemma[≣[]-succ] {}      _              = ≣[zero]
Lemma[≣[]-succ] {succ n} (≣[succ] en e) = ≣[succ] (Lemma[≣[]-succ] en) e

\end{code}

The following lemmas give an equivalent defintion of _≣[_]_:

\begin{code}

Lemma[<-≣[]] : ∀{n : ℕ}{α β : ₂ℕ} → (∀(i : ℕ) → i < n → α i ≡ β i) → α ≣[ n ] β
Lemma[<-≣[]] {}        {α} {β} f = ≣[zero]
Lemma[<-≣[]] {(succ n)} {α} {β} f = ≣[succ] IH claim
 where
  f' : ∀(i : ℕ) → i < n → α i ≡ β i
  f' i r = f i (Lemma[a<b≤c→a<c] r (Lemma[n≤n+1] n))
  IH : α ≣[ n ] β
  IH = Lemma[<-≣[]] {n} {α} {β} f'
  claim : α n ≡ β n
  claim = f n (Lemma[n≤n] (succ n))

Lemma[≣[]-<] : ∀{n : ℕ}{α β : ₂ℕ} → α ≣[ n ] β → ∀(i : ℕ) → i < n → α i ≡ β i
Lemma[≣[]-<] {}      _ i        ()
Lemma[≣[]-<] {succ n} e         r          = Lemma[≣[]-zero] e
Lemma[≣[]-<] {succ n} e (succ i) (≤-succ r) = Lemma[≣[]-<] (Lemma[≣[]-succ] e) i r

\end{code}

Some useful lemmas about _≣[_]_:

\begin{code}

Lemma[≣[]-≤] : ∀{n m : ℕ}{α β : ₂ℕ} → α ≣[ n ] β → m ≤ n → α ≣[ m ] β
Lemma[≣[]-≤] {n} {m} {α} {β} en r = Lemma[<-≣[]] claim₁
 where
  claim₀ : ∀(i : ℕ) → i < n → α i ≡ β i
  claim₀ = Lemma[≣[]-<] en
  claim₁ : ∀(i : ℕ) → i < m → α i ≡ β i
  claim₁ i r' = claim₀ i (Lemma[a<b≤c→a<c] r' r)

Lemma[≣[]-take] : ∀{n : ℕ}{α β : ₂ℕ} → α ≣[ n ] β → take n α ≡ take n β
Lemma[≣[]-take] {}      {α} {β} _  = refl
Lemma[≣[]-take] {succ n} {α} {β} en = Lemma[Vec-≡] base IH
 where
  base : α  ≡ β 
  base = Lemma[≣[]-zero] en
  IH : take n (α ∘ succ) ≡ take n (β ∘ succ)
  IH = Lemma[≣[]-take] (Lemma[≣[]-succ] en)

Lemma[≣[]-drop] : ∀{n m : ℕ}{α β : ₂ℕ} → α ≣[ n + m ] β → drop n α ≣[ m ] drop n β
Lemma[≣[]-drop] {n} {}      {α} {β} _               = ≣[zero]
Lemma[≣[]-drop] {n} {succ m} {α} {β} (≣[succ] enm e) = ≣[succ] IH claim
 where
  IH : drop n α ≣[ m ] drop n β
  IH = Lemma[≣[]-drop] enm
  claim₀ : drop n α m ≡ α (n + m)
  claim₀ = transport {ℕ} {λ k → drop n α m ≡ α k} (Lemma[n+m=m+n] m n) (Lemma[drop+] n α m)
  claim₁ : drop n β m ≡ β (n + m)
  claim₁ = transport {ℕ} {λ k → drop n β m ≡ β k} (Lemma[n+m=m+n] m n) (Lemma[drop+] n β m)
  claim : drop n α m ≡ drop n β m
  claim = trans claim₀ (trans e (sym claim₁))

\end{code}

Concatenation map:

\begin{code}

cons : {m : ℕ} → ₂Fin m → ₂ℕ → ₂ℕ
cons ⟨⟩      α i        = α i
cons (h ∷ _) α         = h
cons (_ ∷ t) α (succ i) = cons t α i

cons₀ : ₂ℕ → ₂ℕ
cons₀ α         = ₀
cons₀ α (succ i) = α i
cons₁ : ₂ℕ → ₂ℕ
cons₁ α         = ₁
cons₁ α (succ i) = α i

Lemma[cons-take-drop] : ∀(n : ℕ) → ∀(α : ₂ℕ) → cons (take n α) (drop n α) ≣ α
Lemma[cons-take-drop]         α i        = refl
Lemma[cons-take-drop] (succ n) α         = refl
Lemma[cons-take-drop] (succ n) α (succ i) = Lemma[cons-take-drop] n (α ∘ succ) i

Lemma[cons-≣] : ∀{m : ℕ} → ∀(s : ₂Fin m) → ∀(α β : ₂ℕ) → α ≣ β → cons s α ≣ cons s β
Lemma[cons-≣] ⟨⟩      α β eq i        = eq i
Lemma[cons-≣] (h ∷ _) α β eq         = refl
Lemma[cons-≣] (_ ∷ t) α β eq (succ i) = Lemma[cons-≣] t α β eq i

Lemma[cons-≣[]] : ∀{n : ℕ} → ∀(s : ₂Fin n) → ∀(α β : ₂ℕ) → cons s α ≣[ n ] cons s β
Lemma[cons-≣[]] s α β = Lemma[<-≣[]] (lemma s α β)
 where
  lemma : {n : ℕ}(s : ₂Fin n)(α β : ₂ℕ)(i : ℕ) → i < n → cons s α i ≡ cons s β i
  lemma ⟨⟩      α β i        ()
  lemma (b ∷ s) α β         r          = refl
  lemma (b ∷ s) α β (succ i) (≤-succ r) = lemma s α β i r

Lemma[cons-take-≣[]] : ∀(n : ℕ) → ∀(α β : ₂ℕ) → α ≣[ n ] cons (take n α) β
Lemma[cons-take-≣[]] n α β = Lemma[<-≣[]] (lemma n α β)
 where
  lemma : ∀(n : ℕ) → ∀(α β : ₂ℕ) → ∀(i : ℕ) → i < n → α i ≡ cons (take n α) β i
  lemma         α β i        ()
  lemma (succ n) α β         r          = refl
  lemma (succ n) α β (succ i) (≤-succ r) = lemma n (α ∘ succ) β i r

Lemma[cons-Vtake-Vdrop] : ∀(n k : ℕ) → ∀(s : ₂Fin (n + k)) → ∀(α : ₂ℕ) →
                          cons (Vtake n k s) (cons (Vdrop n k s) α) ≣ cons s α
Lemma[cons-Vtake-Vdrop] n         s       α i        = refl
Lemma[cons-Vtake-Vdrop] n (succ k) (b ∷ _) α         = refl
Lemma[cons-Vtake-Vdrop] n (succ k) (_ ∷ s) α (succ i) = Lemma[cons-Vtake-Vdrop] n k s α i

Lemma[cons-Vtake-Vdrop]² : ∀(n m l k : ℕ) → (eq : k ≡ m + l) →
                            ∀(s : ₂Fin (k + n)) → ∀(α : ₂ℕ) →
    cons (Vtake k n s)
         (cons (Vtake m l (transport {ℕ} {λ x → ₂Fin x} eq (Vdrop k n s)))
               (cons (Vdrop m l ((transport {ℕ} {λ x → ₂Fin x} eq (Vdrop k n s)))) α))
  ≣ cons s α
Lemma[cons-Vtake-Vdrop]² n m l k eq s α = goal
 where
  ss : ₂Fin k
  ss = Vdrop k n s
  ss' : ₂Fin (m + l)
  ss' = transport {ℕ} {λ x → ₂Fin x} eq ss
  Q : (i : ℕ) → ₂Fin i  → Set
  Q i t = cons (Vtake k n s) (cons t α) ≣ cons s α
  claim₀ : cons (Vtake k n s) (cons ss α) ≣ cons s α
  claim₀ = Lemma[cons-Vtake-Vdrop] k n s α
  claim₁ : cons (Vtake k n s) (cons ss' α) ≣ cons s α
  claim₁ = Lemma[transport] ℕ ₂Fin Q k (m + l) eq ss claim₀
  claim₂ : cons (Vtake m l ss') (cons (Vdrop m l ss') α) ≣ cons ss' α
  claim₂ = Lemma[cons-Vtake-Vdrop] m l ss' α
  claim₃ :  cons (Vtake k n s) (cons (Vtake m l ss') (cons (Vdrop m l ss') α))
          ≣ cons (Vtake k n s) (cons ss' α)
  claim₃ = Lemma[cons-≣] (Vtake k n s)
                             (cons (Vtake m l ss') (cons (Vdrop m l ss') α))
                             (cons ss' α) claim₂
  goal : cons (Vtake k n s) (cons (Vtake m l ss') (cons (Vdrop m l ss') α)) ≣ cons s α
  goal i = trans (claim₃ i) (claim₁ i)

\end{code}

Overwriting map:

\begin{code}

overwrite : ₂ℕ → ℕ → ₂ → ₂ℕ
overwrite α         b         = b
overwrite α         b (succ i) = α (succ i)
overwrite α (succ n) b         = α 
overwrite α (succ n) b (succ i) = overwrite (α ∘ succ) n b i

Lemma[overwrite] : ∀(α : ₂ℕ) → ∀(n : ℕ) → ∀(b : ₂) → overwrite α n b n ≡ b
Lemma[overwrite] α         b = refl
Lemma[overwrite] α (succ n) b = Lemma[overwrite] (α ∘ succ) n b

Lemma[overwrite-≠] : ∀(α : ₂ℕ) → ∀(n : ℕ) → ∀(b : ₂) → ∀(i : ℕ) → i ≠ n → α i ≡ overwrite α n b i
Lemma[overwrite-≠] α         b         r = ∅-elim (r refl)
Lemma[overwrite-≠] α         b (succ i) r = refl
Lemma[overwrite-≠] α (succ n) b         r = refl
Lemma[overwrite-≠] α (succ n) b (succ i) r = Lemma[overwrite-≠] (α ∘ succ) n b i (λ e → r (ap succ e))

Lemma[overwrite-≣[]] : ∀(α : ₂ℕ) → ∀(n : ℕ) → ∀(b : ₂) → α ≣[ n ] overwrite α n b
Lemma[overwrite-≣[]] α n b = Lemma[<-≣[]] claim
 where
  claim : ∀(i : ℕ) → i < n → α i ≡ overwrite α n b i
  claim i r = Lemma[overwrite-≠] α n b i (Lemma[m<n→m≠n] r)

\end{code}

The product of a family of deciable sets, indexed by finite sequences,
is also decidable.

\begin{code}

Lemma[₂Fin-decidability] : (P : (n : ℕ) → ₂Fin n → Set) →
     (∀(n : ℕ) → ∀(s : ₂Fin n) → decidable (P n s)) →
     ∀(n : ℕ) → decidable (∀(s : ₂Fin n) → P n s)
Lemma[₂Fin-decidability] P f  = cases claim₀ claim₁ (f  ⟨⟩)
 where
  claim₀ : P  ⟨⟩ → ∀(s : ₂Fin ) → P  s
  claim₀ p ⟨⟩ = p
  claim₁ : ¬ (P  ⟨⟩) → ¬ (∀(s : ₂Fin ) → P  s)
  claim₁ q g = q (g ⟨⟩)
Lemma[₂Fin-decidability] P f (succ n) = cases claim₀ claim₁ IH
 where
  Q : (m : ℕ) → ₂Fin m → Set
  Q m s = P (succ m) (₀ ∷ s) ∧ P (succ m) (₁ ∷ s)
  claim : ∀(m : ℕ) → ∀(s : ₂Fin m) → decidable (Q m s)
  claim m s = case sclaim₀ sclaim₁ (f (succ m) (₀ ∷ s))
   where
    sclaim₀ : P (succ m) (₀ ∷ s) → decidable (Q m s)
    sclaim₀ p0s = cases ssclaim₀ ssclaim₁ (f (succ m) (₁ ∷ s))
     where
      ssclaim₀ : P (succ m) (₁ ∷ s) → Q m s
      ssclaim₀ p1s = ∧-intro p0s p1s
      ssclaim₁ : ¬ (P (succ m) (₁ ∷ s)) → ¬ (Q m s)
      ssclaim₁ np1s nq = np1s (∧-elim₁ nq)
    sclaim₁ : ¬ (P (succ m) (₀ ∷ s)) → decidable (Q m s)
    sclaim₁ np0s = in₁ (λ nq → np0s (∧-elim₀ nq))
  claim₀ : (∀(s : ₂Fin n) → P (succ n) (₀ ∷ s) ∧ P (succ n) (₁ ∷ s)) →
            ∀(s : ₂Fin (succ n)) → P (succ n) s
  claim₀ g (₀ ∷ s) = ∧-elim₀ (g s)
  claim₀ g (₁ ∷ s) = ∧-elim₁ (g s)
  claim₁ : ¬ (∀(s : ₂Fin n) → P (succ n) (₀ ∷ s) ∧ P (succ n) (₁ ∷ s)) →
            ¬ (∀(s : ₂Fin (succ n)) → P (succ n) s)
  claim₁ h g = h (λ s → g (₀ ∷ s) , g (₁ ∷ s))
  IH : decidable (∀(s : ₂Fin n) → P (succ n) (₀ ∷ s) ∧ P (succ n) (₁ ∷ s))
  IH = Lemma[₂Fin-decidability] Q claim n

\end{code}