Flattening an infinite sequence of lists

Given ls : ωSequence (List α), ls.flatten is the infinite sequence formed by concatenating all members of ls. For this definition to make proper sense, we will consistently assume that all lists in ls are nonempty. Furthermore, in order to simplify the definition, we will also assume [Inhabited α].

def Cslib.ωSequence.cumLen {α : Type u} (ls : ωSequence (List α)) : ℕ → ℕ

Given an ω-sequence ls of lists, ls.cumLen k is the cumulative sum of (ls k).length for k = 0, ..., k - 1.

Equations

• ls.cumLen 0 = 0
• ls.cumLen k.succ = ls.cumLen k + (ls k).length

@[simp]

theorem Cslib.ωSequence.cumLen_zero {α : Type u} {ls : ωSequence (List α)} : ls.cumLen 0 = 0

theorem Cslib.ωSequence.cumLen_succ {α : Type u} (ls : ωSequence (List α)) (k : ℕ) : ls.cumLen (k + 1) = ls.cumLen k + (ls k).length

theorem Cslib.ωSequence.cumLen_one_add_drop {α : Type u} (ls : ωSequence (List α)) (k : ℕ) : ls.cumLen (1 + k) = (ls 0).length + (drop 1 ls).cumLen k

theorem Cslib.ωSequence.cumLen_strictMono {α : Type u} {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) : StrictMono ls.cumLen

If all lists in ls are nonempty, then ls.cumLen is strictly monotonic.

@[simp]

theorem Cslib.ωSequence.cumLen_segment_zero {α : Type u} {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) (h_n : n < (ls 0).length) : Nat.segment ls.cumLen n = 0

theorem Cslib.ωSequence.cumLen_segment_one_add {α : Type u} {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) (h_n : (ls 0).length ≤ n) : Nat.segment ls.cumLen n = 1 + Nat.segment (drop 1 ls).cumLen (n - (ls 0).length)

noncomputable def Cslib.ωSequence.flatten {α : Type u} [Inhabited α] (ls : ωSequence (List α)) : ωSequence α

Given an ω-sequence ls of lists, ls.flatten is the infinite sequence formed by the concatenation of all of them. For the definition to make proper sense, we will consistently assume that all lists in ls are nonempty.

Equations

• ls.flatten = { get := fun (n : ℕ) => (ls (Nat.segment ls.cumLen n))[n - ls.cumLen (Nat.segment ls.cumLen n)]! }

theorem Cslib.ωSequence.flatten_def {α : Type u} [Inhabited α] (ls : ωSequence (List α)) (n : ℕ) : ls.flatten n = (ls (Nat.segment ls.cumLen n))[n - ls.cumLen (Nat.segment ls.cumLen n)]!

@[simp]

theorem Cslib.ωSequence.cons_flatten {α : Type u} [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) : ls.head ++ω ls.tail.flatten = ls.flatten

ls.flatten equals the concatenation of ls.head and ls.tail.flatten.

@[simp]

theorem Cslib.ωSequence.append_flatten {α : Type u} [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) : (take n ls).flatten ++ω (drop n ls).flatten = ls.flatten

ls.flatten equals the concatenation of (ls.take n).flatten and (ls.drop n).flatten.

@[simp]

theorem Cslib.ωSequence.length_flatten_take {α : Type u} {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) : (take n ls).flatten.length = ls.cumLen n

The length of (ls.take n).flatten is ls.cumLen n.

theorem Cslib.ωSequence.flatten_take_drop {α : Type u} [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) : (take n ls).flatten = take (ls.cumLen n) ls.flatten ∧ (drop n ls).flatten = drop (ls.cumLen n) ls.flatten

In fact, (ls.take n).flatten is ls.flatten.take (ls.cumLen n) and (ls.drop n).flattenisls.flatten.drop (ls.cumLen n)`.

theorem Cslib.ωSequence.flatten_take {α : Type u} [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) : (take n ls).flatten = take (ls.cumLen n) ls.flatten

theorem Cslib.ωSequence.flatten_drop {α : Type u} [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) : (drop n ls).flatten = drop (ls.cumLen n) ls.flatten

@[simp]

theorem Cslib.ωSequence.extract_flatten {α : Type u} [Inhabited α] {ls : ωSequence (List α)} (h_ls : ∀ (k : ℕ), (ls k).length > 0) (n : ℕ) : ls.flatten.extract (ls.cumLen n) (ls.cumLen (n + 1)) = ls n

ls n is the segement from position ls.cumLen n to position ls.cumLen (n + 1) - 1 of ls.flatten`

def Cslib.ωSequence.toSegs {α : Type u} (s : ωSequence α) (f : ℕ → ℕ) : ωSequence (List α)

Given an ω-sequence s and a function f : ℕ → ℕ, s.toSegs f is the ω-sequence whose n-th element is the list s.extract (f n) (f (n + 1)). In all its uses, the function f will always be assumed to be strictly monotonic with f 0 = 0.

Equations

• s.toSegs f = { get := fun (n : ℕ) => s.extract (f n) (f (n + 1)) }

theorem Cslib.ωSequence.toSegs_def {α : Type u} (s : ωSequence α) (f : ℕ → ℕ) (n : ℕ) : (s.toSegs f) n = s.extract (f n) (f (n + 1))

@[simp]

theorem Cslib.ωSequence.segment_toSegs_cumLen {α : Type u} {f : ℕ → ℕ} (hm : StrictMono f) (h0 : f 0 = 0) (s : ωSequence α) : (s.toSegs f).cumLen = f

(s.toSegs f).cumLen is f itself.

@[simp]

theorem Cslib.ωSequence.strictMono_flatten {α : Type u} [Inhabited α] {f : ℕ → ℕ} (hm : StrictMono f) (h0 : f 0 = 0) (s : ωSequence α) : (s.toSegs f).flatten = s

(s.toSegs f).flatten is s itself.