Sequence
Chuangjie Xu 2013 (ported to TypeTopology in 2025) Module for both finite and infinite sequences of boolean 𝟚{-# OPTIONS --safe --without-K #-} module C-Spaces.Preliminaries.Sequence where open import MLTT.Spartan hiding (_+_) open import Naturals.Addition open import UF.DiscreteAndSeparated open import C-Spaces.Preliminaries.Naturals.OrderInfinite sequences are defined as functions:₂ℕ : Set ₂ℕ = ℕ → 𝟚 0̄ : ₂ℕ 0̄ i = ₀ 1̄ : ₂ℕ 1̄ i = ₁Finite sequences are defined as vectors:infixr 50 _∷_ data ₂Fin : ℕ → Set where ⟨⟩ : ₂Fin 0 _∷_ : {n : ℕ} → 𝟚 → ₂Fin n → ₂Fin (succ n) head : {n : ℕ} → ₂Fin (succ n) → 𝟚 head (b ∷ _) = b tail : {n : ℕ} → ₂Fin (succ n) → ₂Fin n tail (_ ∷ s) = s ₂Fin-＝ : ∀{n : ℕ} {s s' : ₂Fin (succ n)} → head s ＝ head s' → tail s ＝ tail s' → s ＝ s' ₂Fin-＝ {n} {x ∷ xs} {.x ∷ .xs} refl refl = refl ⟨₀⟩ : ₂Fin 1 ⟨₀⟩ = ₀ ∷ ⟨⟩ ⟨₁⟩ : ₂Fin 1 ⟨₁⟩ = ₁ ∷ ⟨⟩ ftake : (n k : ℕ) → ₂Fin (n + k) → ₂Fin k ftake n 0 v = ⟨⟩ ftake n (succ k) (h ∷ t) = h ∷ ftake n k t fdrop : (n k : ℕ) → ₂Fin (n + k) → ₂Fin n fdrop n 0 v = v fdrop n (succ k) (h ∷ t) = fdrop n k t take : (m : ℕ) → ₂ℕ → ₂Fin m take 0 α = ⟨⟩ take (succ n) α = α 0 ∷ take n (α ∘ succ) drop : ℕ → ₂ℕ → ₂ℕ drop 0 α = α drop (succ m) α = drop m (α ∘ succ) Lemma[drop+] : ∀(n : ℕ) → ∀(α : ₂ℕ) → ∀(i : ℕ) → drop n α i ＝ α (i + n) Lemma[drop+] 0 α 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 = 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 {0} f = (f ⟨⟩) , prf where prf : ∀(s : ₂Fin 0) → f s ≤ f ⟨⟩ prf ⟨⟩ = ≤-refl max-fin {succ n} f = m , prf where g : 𝟚 → ₂Fin n → ℕ g = pr₁ (isomorphism-₂Fin ℕ n f) m₀ : ℕ m₀ = pr₁ (max-fin (g ₀)) prf₀ : ∀(s : ₂Fin n) → g ₀ s ≤ m₀ prf₀ = pr₂ (max-fin (g ₀)) m₁ : ℕ m₁ = pr₁ (max-fin (g ₁)) prf₁ : ∀(s : ₂Fin n) → g ₁ s ≤ m₁ prf₁ = pr₂ (max-fin (g ₁)) m : ℕ m = max m₀ m₁ prf : ∀(s : ₂Fin (succ n)) → f s ≤ m prf (₀ ∷ s) = ≤-trans (prf₀ s) (max-spec₀ m₀ m₁) prf (₁ ∷ s) = ≤-trans (prf₁ s) (max-spec₁ m₀ m₁)Pointwise equality over infinite sequences:Lemma[∼-take] : ∀(n : ℕ) → ∀(α β : ₂ℕ) → α ∼ β → take n α ＝ take n β Lemma[∼-take] 0 α β e = refl Lemma[∼-take] (succ n) α β e = ₂Fin-＝ (e 0) (Lemma[∼-take] n (α ∘ succ) (β ∘ succ) (λ i → e (succ i))) Lemma[∼-drop] : ∀(n : ℕ) → ∀(α β : ₂ℕ) → α ∼ β → drop n α ∼ drop n β Lemma[∼-drop] 0 α β e = e Lemma[∼-drop] (succ n) α β e = Lemma[∼-drop] n (α ∘ succ) (β ∘ succ) (λ i → e (succ i))"Agree with" relation over infinite sequences, which is an equivalence relation and a deciable type:infixl 10 _＝⟦_⟧_ data _＝⟦_⟧_ {X : Set} : (ℕ → X) → ℕ → (ℕ → X) → Set where ＝⟦zero⟧ : {α β : ℕ → X} → α ＝⟦ 0 ⟧ β ＝⟦succ⟧ : {α β : ℕ → X}{n : ℕ} → α ＝⟦ n ⟧ β → α n ＝ β n → α ＝⟦ succ n ⟧ β ＝⟦⟧-refl : {n : ℕ}{α : ₂ℕ} → α ＝⟦ n ⟧ α ＝⟦⟧-refl {0} = ＝⟦zero⟧ ＝⟦⟧-refl {succ n} = ＝⟦succ⟧ ＝⟦⟧-refl refl ＝⟦⟧-sym : {n : ℕ}{α β : ₂ℕ} → α ＝⟦ n ⟧ β → β ＝⟦ n ⟧ α ＝⟦⟧-sym {0} ＝⟦zero⟧ = ＝⟦zero⟧ ＝⟦⟧-sym {succ n} (＝⟦succ⟧ en e) = ＝⟦succ⟧ (＝⟦⟧-sym en) (e ⁻¹) ＝⟦⟧-trans : {n : ℕ}{α₀ α₁ α₂ : ₂ℕ} → α₀ ＝⟦ n ⟧ α₁ → α₁ ＝⟦ n ⟧ α₂ → α₀ ＝⟦ n ⟧ α₂ ＝⟦⟧-trans {0} ＝⟦zero⟧ ＝⟦zero⟧ = ＝⟦zero⟧ ＝⟦⟧-trans {succ n} (＝⟦succ⟧ en e) (＝⟦succ⟧ en' e') = ＝⟦succ⟧ (＝⟦⟧-trans en en') (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 : ℕ} → ∀(α β : ₂ℕ) → is-decidable (α ＝⟦ m ⟧ β) Lemma[＝⟦⟧-decidable] {0} α β = inl ＝⟦zero⟧ Lemma[＝⟦⟧-decidable] {succ m} α β = cases claim₀ claim₁ IH where IH : is-decidable (α ＝⟦ m ⟧ β) IH = Lemma[＝⟦⟧-decidable] {m} α β claim₀ : α ＝⟦ m ⟧ β → is-decidable (α ＝⟦ succ m ⟧ β) claim₀ em = cases c₀ c₁ (𝟚-is-discrete (α m) (β m)) where c₀ : α m ＝ β m → is-decidable (α ＝⟦ succ m ⟧ β) c₀ e = inl (＝⟦succ⟧ em e) c₁ : ¬ (α m ＝ β m) → is-decidable (α ＝⟦ succ m ⟧ β) c₁ f = inr (λ e → f (Lemma[＝⟦succ⟧]₁ e)) claim₁ : ¬ (α ＝⟦ m ⟧ β) → is-decidable (α ＝⟦ succ m ⟧ β) claim₁ f = inr (λ e → f(Lemma[＝⟦succ⟧]₀ e)) Lemma[＝⟦⟧-zero] : ∀{n : ℕ}{α β : ₂ℕ} → α ＝⟦ succ n ⟧ β → α 0 ＝ β 0 Lemma[＝⟦⟧-zero] {0} (＝⟦succ⟧ ＝⟦zero⟧ e) = e Lemma[＝⟦⟧-zero] {succ n} (＝⟦succ⟧ en e) = Lemma[＝⟦⟧-zero] en Lemma[＝⟦⟧-succ] : ∀{n : ℕ}{α β : ₂ℕ} → α ＝⟦ succ n ⟧ β → (α ∘ succ) ＝⟦ n ⟧ (β ∘ succ) Lemma[＝⟦⟧-succ] {0} _ = ＝⟦zero⟧ Lemma[＝⟦⟧-succ] {succ n} (＝⟦succ⟧ en e) = ＝⟦succ⟧ (Lemma[＝⟦⟧-succ] en) eThe following lemmas give an equivalent definition of _＝⟦_⟧_:Lemma[<-＝⟦⟧] : ∀{n : ℕ}{α β : ₂ℕ} → (∀(i : ℕ) → i < n → α i ＝ β i) → α ＝⟦ n ⟧ β Lemma[<-＝⟦⟧] {0} {α} {β} f = ＝⟦zero⟧ Lemma[<-＝⟦⟧] {(succ n)} {α} {β} f = ＝⟦succ⟧ IH claim where f' : ∀(i : ℕ) → i < n → α i ＝ β i f' i r = f i (≤-trans r (Lemma[n≤n+1] n)) IH : α ＝⟦ n ⟧ β IH = Lemma[<-＝⟦⟧] {n} {α} {β} f' claim : α n ＝ β n claim = f n ≤-refl Lemma[＝⟦⟧-<] : ∀{n : ℕ}{α β : ₂ℕ} → α ＝⟦ n ⟧ β → ∀(i : ℕ) → i < n → α i ＝ β i Lemma[＝⟦⟧-<] {0} _ i () Lemma[＝⟦⟧-<] {succ n} e 0 r = Lemma[＝⟦⟧-zero] e Lemma[＝⟦⟧-<] {succ n} e (succ i) (≤-succ r) = Lemma[＝⟦⟧-<] (Lemma[＝⟦⟧-succ] e) i rSome useful lemmas about _＝⟦_⟧_: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 (≤-trans r' r) Lemma[＝⟦⟧-take] : ∀{n : ℕ}{α β : ₂ℕ} → α ＝⟦ n ⟧ β → take n α ＝ take n β Lemma[＝⟦⟧-take] {0} {α} {β} _ = refl Lemma[＝⟦⟧-take] {succ n} {α} {β} en = ₂Fin-＝ base IH where base : α 0 ＝ β 0 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} {0} {α} {β} _ = ＝⟦zero⟧ Lemma[＝⟦⟧-drop] {n} {succ m} {α} {β} (＝⟦succ⟧ enm e) = ＝⟦succ⟧ IH goal where IH : drop n α ＝⟦ m ⟧ drop n β IH = Lemma[＝⟦⟧-drop] enm claim : ∀ γ → drop n γ m ＝ γ (n + m) claim γ = transport (λ k → drop n γ m ＝ γ k) (addition-commutativity m n) (Lemma[drop+] n γ m) goal : drop n α m ＝ drop n β m goal = claim α ∙ e ∙ (claim β) ⁻¹Concatenation map:cons : {m : ℕ} → ₂Fin m → ₂ℕ → ₂ℕ cons ⟨⟩ α = α cons (h ∷ _) α 0 = h cons (_ ∷ t) α (succ i) = cons t α i cons₀ : ₂ℕ → ₂ℕ cons₀ α 0 = ₀ cons₀ α (succ i) = α i cons₁ : ₂ℕ → ₂ℕ cons₁ α 0 = ₁ cons₁ α (succ i) = α i Lemma[cons-take-drop] : ∀(n : ℕ) → ∀(α : ₂ℕ) → cons (take n α) (drop n α) ∼ α Lemma[cons-take-drop] 0 α i = refl Lemma[cons-take-drop] (succ n) α 0 = 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 0 = refl Lemma[cons-∼] (_ ∷ t) α β eq (succ i) = Lemma[cons-∼] t α β eq i lemma-blah : {n : ℕ}(s : ₂Fin n)(α β : ₂ℕ)(i : ℕ) → i < n → cons s α i ＝ cons s β i lemma-blah ⟨⟩ α β i () lemma-blah (b ∷ s) α β 0 r = refl lemma-blah (b ∷ s) α β (succ i) (≤-succ r) = lemma-blah s α β i r Lemma[cons-＝⟦⟧] : ∀{n : ℕ} → ∀(s : ₂Fin n) → ∀(α β : ₂ℕ) → cons s α ＝⟦ n ⟧ cons s β Lemma[cons-＝⟦⟧] s α β = Lemma[<-＝⟦⟧] (lemma-blah s α β) 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 0 α β i () lemma (succ n) α β 0 r = refl lemma (succ n) α β (succ i) (≤-succ r) = lemma n (α ∘ succ) β i r Lemma[cons-ftake-fdrop] : ∀(n k : ℕ) → ∀(s : ₂Fin (n + k)) → ∀(α : ₂ℕ) → cons (ftake n k s) (cons (fdrop n k s) α) ∼ cons s α Lemma[cons-ftake-fdrop] n 0 s α i = refl Lemma[cons-ftake-fdrop] n (succ k) (b ∷ _) α 0 = refl Lemma[cons-ftake-fdrop] n (succ k) (_ ∷ s) α (succ i) = Lemma[cons-ftake-fdrop] n k s α i Lemma[cons-ftake-fdrop]² : ∀(n m l k : ℕ) → (eq : k ＝ m + l) → ∀(s : ₂Fin (k + n)) → ∀(α : ₂ℕ) → cons (ftake k n s) (cons (ftake m l (transport ₂Fin eq (fdrop k n s))) (cons (fdrop m l ((transport ₂Fin eq (fdrop k n s)))) α)) ∼ cons s α Lemma[cons-ftake-fdrop]² n m l k eq s α = goal where ss : ₂Fin k ss = fdrop k n s ss' : ₂Fin (m + l) ss' = transport ₂Fin eq ss Q : (i : ℕ) → ₂Fin i → Set Q i t = cons (ftake k n s) (cons t α) ∼ cons s α claim₀ : cons (ftake k n s) (cons ss α) ∼ cons s α claim₀ = Lemma[cons-ftake-fdrop] k n s α transport² : {X : Set} (Y : X → Set) (Z : (x : X) → Y x → Set) → {x x' : X} {y : Y x} → (p : x ＝ x') → Z x y → Z x' (transport Y p y) transport² Y Z refl z = z claim₁ : cons (ftake k n s) (cons ss' α) ∼ cons s α claim₁ = transport² ₂Fin Q eq claim₀ claim₂ : cons (ftake m l ss') (cons (fdrop m l ss') α) ∼ cons ss' α claim₂ = Lemma[cons-ftake-fdrop] m l ss' α claim₃ : cons (ftake k n s) (cons (ftake m l ss') (cons (fdrop m l ss') α)) ∼ cons (ftake k n s) (cons ss' α) claim₃ = Lemma[cons-∼] (ftake k n s) (cons (ftake m l ss') (cons (fdrop m l ss') α)) (cons ss' α) claim₂ goal : cons (ftake k n s) (cons (ftake m l ss') (cons (fdrop m l ss') α)) ∼ cons s α goal i = (claim₃ i) ∙ (claim₁ i) Lemma[cons-＝⟦⟧-≤] : {n m : ℕ}{α β : ₂ℕ} → (s : ₂Fin n) → m ≤ n → cons s α ＝⟦ m ⟧ cons s β Lemma[cons-＝⟦⟧-≤] _ ≤-zero = ＝⟦zero⟧ Lemma[cons-＝⟦⟧-≤] s (≤-succ r) = ＝⟦succ⟧ (Lemma[cons-＝⟦⟧-≤] s (≤-r-succ r)) (lemma s r) where lemma : {n m : ℕ}{α β : ₂ℕ} → (s : ₂Fin (succ n)) → m ≤ n → cons s α m ＝ cons s β m lemma (b ∷ s) ≤-zero = refl lemma (b ∷ s) (≤-succ r) = lemma s r Lemma[＝⟦⟧-cons-take] : {α β : ₂ℕ} → ∀(n : ℕ) → α ＝⟦ n ⟧ cons (take n α) β Lemma[＝⟦⟧-cons-take] {α} {β} n = lemma₁ n n ≤-refl where lemma₀ : ∀(α β : ₂ℕ)(m k : ℕ) → succ m ≤ k → α m ＝ cons (take k α) β m lemma₀ α β m 0 () lemma₀ α β 0 (succ k) r = refl lemma₀ α β (succ m) (succ k) (≤-succ r) = lemma₀ (α ∘ succ) β m k r lemma₁ : ∀(m k : ℕ) → m ≤ k → α ＝⟦ m ⟧ cons (take k α) β lemma₁ 0 k ≤-zero = ＝⟦zero⟧ lemma₁ (succ m) 0 () lemma₁ (succ m) (succ k) (≤-succ r) = ＝⟦succ⟧ (lemma₁ m (succ k) (≤-r-succ r)) (lemma₀ α β m (succ k) (≤-succ r)) Lemma[＝⟦⟧-＝⟦⟧-take] : {α β γ : ₂ℕ} → ∀(n : ℕ) → α ＝⟦ n ⟧ β → β ＝⟦ n ⟧ cons (take n α) γ Lemma[＝⟦⟧-＝⟦⟧-take] n en = ＝⟦⟧-trans (＝⟦⟧-sym en) (Lemma[＝⟦⟧-cons-take] n) Lemma[cons-take-0] : {α β : ₂ℕ} → ∀(n : ℕ) → β 0 ＝ cons (take n α) β n Lemma[cons-take-0] 0 = refl Lemma[cons-take-0] (succ n) = Lemma[cons-take-0] nOverwriting map:overwrite : ₂ℕ → ℕ → 𝟚 → ₂ℕ overwrite α 0 b 0 = b overwrite α 0 b (succ i) = α (succ i) overwrite α (succ n) b 0 = α 0 overwrite α (succ n) b (succ i) = overwrite (α ∘ succ) n b i Lemma[overwrite] : ∀(α : ₂ℕ) → ∀(n : ℕ) → ∀(b : 𝟚) → overwrite α n b n ＝ b Lemma[overwrite] α 0 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-≠] α 0 b 0 r = 𝟘-elim (r refl) Lemma[overwrite-≠] α 0 b (succ i) r = refl Lemma[overwrite-≠] α (succ n) b 0 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)The product of a family of deciable sets, indexed by finite sequences, is also decidable.Lemma[₂Fin-decidability] : (n : ℕ) → (Y : ₂Fin n → Set) → (∀ s → is-decidable (Y s)) → is-decidable (∀ s → Y s) Lemma[₂Fin-decidability] 0 Y decY = cases (inl ∘ c₀) (inr ∘ c₁) (decY ⟨⟩) where c₀ : Y ⟨⟩ → ∀ s → Y s c₀ y ⟨⟩ = y c₁ : ¬ (Y ⟨⟩) → ¬ (∀ s → Y s) c₁ f g = f (g ⟨⟩) Lemma[₂Fin-decidability] (succ n) Y decY = cases c₀ c₁ IH₀ where Y₀ : ₂Fin n → Set Y₀ s = Y (₀ ∷ s) decY₀ : ∀ s → is-decidable (Y₀ s) decY₀ s = decY (₀ ∷ s) IH₀ : is-decidable (∀ s → Y₀ s) IH₀ = Lemma[₂Fin-decidability] n Y₀ decY₀ Y₁ : ₂Fin n → Set Y₁ s = Y (₁ ∷ s) decY₁ : ∀ s → is-decidable (Y₁ s) decY₁ s = decY (₁ ∷ s) IH₁ : is-decidable (∀ s → Y₁ s) IH₁ = Lemma[₂Fin-decidability] n Y₁ decY₁ c₀ : (∀ s → Y₀ s) → is-decidable (∀ s → Y s) c₀ y₀ = cases (inl ∘ sc₀) (inr ∘ sc₁) IH₁ where sc₀ : (∀ s → Y₁ s) → ∀ s → Y s sc₀ y₁ (₀ ∷ s) = y₀ s sc₀ y₁ (₁ ∷ s) = y₁ s sc₁ : ¬ (∀ s → Y₁ s) → ¬ (∀ s → Y s) sc₁ f₁ ys = f₁ (λ s → ys (₁ ∷ s)) c₁ : ¬ (∀ s → Y₀ s) → is-decidable (∀ s → Y s) c₁ f₀ = inr (λ ys → f₀ (λ s → ys (₀ ∷ s)))