ω-sequences a.k.a. infinite sequences

Most code below is adapted from Mathlib.Data.Stream.Init.

@[instance_reducible]

instance Cslib.ωSequence.instInhabited {α : Type u} [Inhabited α] : Inhabited (ωSequence α)

Equations

• Cslib.ωSequence.instInhabited = { default := Cslib.ωSequence.const default }

instance Cslib.ωSequence.instIsEmpty {α : Type u} [h : IsEmpty α] : IsEmpty (ωSequence α)

@[simp]

theorem Cslib.ωSequence.eta {α : Type u} (s : ωSequence α) : cons s.head s.tail = s

theorem Cslib.ωSequence.cons_head_tail {α : Type u} (s : ωSequence α) : cons s.head s.tail = s

Alias for ωSequence.eta to match List API.

theorem Cslib.ωSequence.ext {α : Type u} {s₁ s₂ : ωSequence α} : (∀ (n : ℕ), s₁ n = s₂ n) → s₁ = s₂

theorem Cslib.ωSequence.ext_iff {α : Type u} {s₁ s₂ : ωSequence α} : s₁ = s₂ ↔ ∀ (n : ℕ), s₁ n = s₂ n

@[simp]

theorem Cslib.ωSequence.get_fun {α : Type u} (f : ℕ → α) (n : ℕ) : { get := f } n = f n

@[simp]

theorem Cslib.ωSequence.get_zero_cons {α : Type u} (a : α) (s : ωSequence α) : (cons a s) 0 = a

@[simp]

theorem Cslib.ωSequence.head_cons {α : Type u} (a : α) (s : ωSequence α) : (cons a s).head = a

@[simp]

theorem Cslib.ωSequence.tail_cons {α : Type u} (a : α) (s : ωSequence α) : (cons a s).tail = s

@[simp]

theorem Cslib.ωSequence.get_drop {α : Type u} (n m : ℕ) (s : ωSequence α) : (drop m s) n = s (m + n)

theorem Cslib.ωSequence.tail_eq_drop {α : Type u} (s : ωSequence α) : s.tail = drop 1 s

@[simp]

theorem Cslib.ωSequence.drop_drop {α : Type u} (n m : ℕ) (s : ωSequence α) : drop n (drop m s) = drop (m + n) s

@[simp]

theorem Cslib.ωSequence.get_tail {α : Type u} {n : ℕ} {s : ωSequence α} : s.tail n = s (n + 1)

@[simp]

theorem Cslib.ωSequence.tail_drop' {α : Type u} {i : ℕ} {s : ωSequence α} : (drop i s).tail = drop (i + 1) s

@[simp]

theorem Cslib.ωSequence.drop_tail' {α : Type u} {i : ℕ} {s : ωSequence α} : drop i s.tail = drop (i + 1) s

theorem Cslib.ωSequence.tail_drop {α : Type u} (n : ℕ) (s : ωSequence α) : (drop n s).tail = drop n s.tail

theorem Cslib.ωSequence.get_succ {α : Type u} (n : ℕ) (s : ωSequence α) : s n.succ = s.tail n

@[simp]

theorem Cslib.ωSequence.get_succ_cons {α : Type u} (n : ℕ) (s : ωSequence α) (x : α) : (cons x s) n.succ = s n

@[simp]

theorem Cslib.ωSequence.get_cons_append_zero {α : Type u} {a : α} {x : List α} {s : ωSequence α} : (a :: x ++ω s) 0 = a

theorem Cslib.ωSequence.append_get_zero_of_ne_nil {α : Type u} {x : List α} {s : ωSequence α} (h : x ≠ []) : (x ++ω s) 0 = x.head h

@[simp]

theorem Cslib.ωSequence.append_eq_cons {α : Type u} {a : α} {as : ωSequence α} : [a] ++ω as = cons a as

@[simp]

theorem Cslib.ωSequence.drop_zero {α : Type u} {s : ωSequence α} : drop 0 s = s

theorem Cslib.ωSequence.drop_succ {α : Type u} (n : ℕ) (s : ωSequence α) : drop n.succ s = drop n s.tail

theorem Cslib.ωSequence.head_drop {α : Type u} (a : ωSequence α) (n : ℕ) : (drop n a).head = a n

theorem Cslib.ωSequence.cons_injective2 {α : Type u} : Function.Injective2 cons

theorem Cslib.ωSequence.cons_injective_left {α : Type u} (s : ωSequence α) : Function.Injective fun (x : α) => cons x s

theorem Cslib.ωSequence.cons_injective_right {α : Type u} (x : α) : Function.Injective (cons x)

theorem Cslib.ωSequence.drop_map {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : ωSequence α) : drop n (map f s) = map f (drop n s)

@[simp]

theorem Cslib.ωSequence.get_map {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : ωSequence α) : (map f s) n = f (s n)

theorem Cslib.ωSequence.tail_map {α : Type u} {β : Type v} (f : α → β) (s : ωSequence α) : (map f s).tail = map f s.tail

@[simp]

theorem Cslib.ωSequence.head_map {α : Type u} {β : Type v} (f : α → β) (s : ωSequence α) : (map f s).head = f s.head

theorem Cslib.ωSequence.map_eq {α : Type u} {β : Type v} (f : α → β) (s : ωSequence α) : map f s = cons (f s.head) (map f s.tail)

theorem Cslib.ωSequence.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : ωSequence α) : map f (cons a s) = cons (f a) (map f s)

@[simp]

theorem Cslib.ωSequence.map_id {α : Type u} (s : ωSequence α) : map id s = s

@[simp]

theorem Cslib.ωSequence.map_map {α : Type u} {β : Type v} {δ : Type w} (g : β → δ) (f : α → β) (s : ωSequence α) : map g (map f s) = map (g ∘ f) s

@[simp]

theorem Cslib.ωSequence.map_tail {α : Type u} {β : Type v} (f : α → β) (s : ωSequence α) : map f s.tail = (map f s).tail

theorem Cslib.ωSequence.drop_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ℕ) (s₁ : ωSequence α) (s₂ : ωSequence β) : drop n (zip f s₁ s₂) = zip f (drop n s₁) (drop n s₂)

@[simp]

theorem Cslib.ωSequence.get_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ℕ) (s₁ : ωSequence α) (s₂ : ωSequence β) : (zip f s₁ s₂) n = f (s₁ n) (s₂ n)

theorem Cslib.ωSequence.head_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : ωSequence α) (s₂ : ωSequence β) : (zip f s₁ s₂).head = f s₁.head s₂.head

theorem Cslib.ωSequence.tail_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : ωSequence α) (s₂ : ωSequence β) : (zip f s₁ s₂).tail = zip f s₁.tail s₂.tail

theorem Cslib.ωSequence.zip_eq {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : ωSequence α) (s₂ : ωSequence β) : zip f s₁ s₂ = cons (f s₁.head s₂.head) (zip f s₁.tail s₂.tail)

theorem Cslib.ωSequence.const_eq {α : Type u} (a : α) : const a = cons a (const a)

@[simp]

theorem Cslib.ωSequence.tail_const {α : Type u} (a : α) : (const a).tail = const a

@[simp]

theorem Cslib.ωSequence.map_const {α : Type u} {β : Type v} (f : α → β) (a : α) : map f (const a) = const (f a)

@[simp]

theorem Cslib.ωSequence.get_const {α : Type u} (n : ℕ) (a : α) : (const a) n = a

@[simp]

theorem Cslib.ωSequence.drop_const {α : Type u} (n : ℕ) (a : α) : drop n (const a) = const a

@[simp]

theorem Cslib.ωSequence.head_iterate {α : Type u} (f : α → α) (a : α) : (iterate f a).head = a

theorem Cslib.ωSequence.get_iterate {α : Type u} (f : α → α) (a : α) (n : ℕ) : (iterate f a) n = f^[n] a

theorem Cslib.ωSequence.get_succ_iterate' {α : Type u} (n : ℕ) (f : α → α) (a : α) : (iterate f a) n.succ = f ((iterate f a) n)

theorem Cslib.ωSequence.tail_iterate {α : Type u} (f : α → α) (a : α) : (iterate f a).tail = iterate f (f a)

theorem Cslib.ωSequence.iterate_eq {α : Type u} (f : α → α) (a : α) : iterate f a = cons a (iterate f (f a))

@[simp]

theorem Cslib.ωSequence.get_zero_iterate {α : Type u} (f : α → α) (a : α) : (iterate f a) 0 = a

theorem Cslib.ωSequence.get_succ_iterate {α : Type u} (n : ℕ) (f : α → α) (a : α) : (iterate f a) n.succ = (iterate f (f a)) n

@[simp]

theorem Cslib.ωSequence.iterate_id {α : Type u} (a : α) : iterate id a = const a

theorem Cslib.ωSequence.map_iterate {α : Type u} (f : α → α) (a : α) : iterate f (f a) = map f (iterate f a)

@[simp]

theorem Cslib.ωSequence.nil_append_ωSequence {α : Type u} (s : ωSequence α) : [] ++ω s = s

theorem Cslib.ωSequence.cons_append_ωSequence {α : Type u} (a : α) (l : List α) (s : ωSequence α) : a :: l ++ω s = cons a (l ++ω s)

@[simp]

theorem Cslib.ωSequence.singleton_append_ωSequence {α : Type u} (a : α) (s : ωSequence α) : [a] ++ω s = cons a s

@[simp]

theorem Cslib.ωSequence.append_append_ωSequence {α : Type u} (l₁ l₂ : List α) (s : ωSequence α) : l₁ ++ l₂ ++ω s = l₁ ++ω (l₂ ++ω s)

theorem Cslib.ωSequence.get_append_left {α : Type u} (n : ℕ) (x : List α) (a : ωSequence α) (h : n < x.length) : (x ++ω a) n = x[n]

@[simp]

theorem Cslib.ωSequence.get_append_right {α : Type u} (n : ℕ) (x : List α) (a : ωSequence α) : (x ++ω a) (x.length + n) = a n

theorem Cslib.ωSequence.get_append_right' {α : Type u} {xl : List α} {xs : ωSequence α} {k : ℕ} (h : xl.length ≤ k) : (xl ++ω xs) k = xs (k - xl.length)

@[simp]

theorem Cslib.ωSequence.get_append_length {α : Type u} (x : List α) (a : ωSequence α) : (x ++ω a) x.length = a 0

theorem Cslib.ωSequence.append_right_injective {α : Type u} (x : List α) (a b : ωSequence α) (h : x ++ω a = x ++ω b) : a = b

@[simp]

theorem Cslib.ωSequence.append_right_inj {α : Type u} (x : List α) (a b : ωSequence α) : x ++ω a = x ++ω b ↔ a = b

theorem Cslib.ωSequence.append_left_injective {α : Type u} (x y : List α) (a b : ωSequence α) (h : x ++ω a = y ++ω b) (hl : x.length = y.length) : x = y

theorem Cslib.ωSequence.append_left_right_injective {α : Type u} (l1 l2 : List α) (s1 s2 : ωSequence α) (h1 : l1 ++ω s1 = l2 ++ω s2) (h2 : l1.length = l2.length) : l1 = l2 ∧ s1 = s2

theorem Cslib.ωSequence.map_append_ωSequence {α : Type u} {β : Type v} (f : α → β) (l : List α) (s : ωSequence α) : map f (l ++ω s) = List.map f l ++ω map f s

theorem Cslib.ωSequence.drop_append_ωSequence {α : Type u} (l : List α) (s : ωSequence α) : drop l.length (l ++ω s) = s

theorem Cslib.ωSequence.append_ωSequence_head_tail {α : Type u} (s : ωSequence α) : [s.head] ++ω s.tail = s

@[simp]

theorem Cslib.ωSequence.take_zero {α : Type u} (s : ωSequence α) : take 0 s = []

theorem Cslib.ωSequence.take_succ {α : Type u} (n : ℕ) (s : ωSequence α) : take n.succ s = s.head :: take n s.tail

@[simp]

theorem Cslib.ωSequence.take_succ_cons {α : Type u} {a : α} (n : ℕ) (s : ωSequence α) : take (n + 1) (cons a s) = a :: take n s

theorem Cslib.ωSequence.take_succ' {α : Type u} {s : ωSequence α} (n : ℕ) : take (n + 1) s = take n s ++ [s n]

@[simp]

theorem Cslib.ωSequence.take_one {α : Type u} {xs : ωSequence α} : take 1 xs = [xs 0]

@[simp]

theorem Cslib.ωSequence.length_take {α : Type u} (n : ℕ) (s : ωSequence α) : (take n s).length = n

@[simp]

theorem Cslib.ωSequence.take_take {α : Type u} {s : ωSequence α} {m n : ℕ} : List.take m (take n s) = take (min n m) s

@[simp]

theorem Cslib.ωSequence.concat_take_get {α : Type u} {n : ℕ} {s : ωSequence α} : take n s ++ [s n] = take (n + 1) s

theorem Cslib.ωSequence.getElem?_take {α : Type u} {s : ωSequence α} {k n : ℕ} : k < n → (take n s)[k]? = some (s k)

theorem Cslib.ωSequence.getElem?_take_succ {α : Type u} (n : ℕ) (s : ωSequence α) : (take n.succ s)[n]? = some (s n)

@[simp]

theorem Cslib.ωSequence.dropLast_take {α : Type u} {n : ℕ} {xs : ωSequence α} : (take n xs).dropLast = take (n - 1) xs

@[simp]

theorem Cslib.ωSequence.append_take_drop {α : Type u} (n : ℕ) (s : ωSequence α) : take n s ++ω drop n s = s

theorem Cslib.ωSequence.append_take {α : Type u} (n : ℕ) (x : List α) (a : ωSequence α) : x ++ take n a = take (x.length + n) (x ++ω a)

@[simp]

theorem Cslib.ωSequence.take_get {α : Type u} (m n : ℕ) (a : ωSequence α) (h : m < (take n a).length) : (take n a)[m] = a m

theorem Cslib.ωSequence.take_append_of_le_length {α : Type u} (n : ℕ) (x : List α) (a : ωSequence α) (h : n ≤ x.length) : take n (x ++ω a) = List.take n x

theorem Cslib.ωSequence.take_add {α : Type u} (m n : ℕ) (a : ωSequence α) : take (m + n) a = take m a ++ take n (drop m a)

theorem Cslib.ωSequence.take_prefix_take_left {α : Type u} (m n : ℕ) (a : ωSequence α) (h : m ≤ n) : take m a <+: take n a

@[simp]

theorem Cslib.ωSequence.take_prefix {α : Type u} (m n : ℕ) (a : ωSequence α) : take m a <+: take n a ↔ m ≤ n

theorem Cslib.ωSequence.map_take {α : Type u} {β : Type v} (n : ℕ) (a : ωSequence α) (f : α → β) : List.map f (take n a) = take n (map f a)

theorem Cslib.ωSequence.take_drop {α : Type u} (m n : ℕ) (a : ωSequence α) : take n (drop m a) = List.drop m (take (m + n) a)

theorem Cslib.ωSequence.drop_append_of_le_length {α : Type u} (n : ℕ) (x : List α) (a : ωSequence α) (h : n ≤ x.length) : drop n (x ++ω a) = List.drop n x ++ω a

theorem Cslib.ωSequence.drop_append_of_ge_length {α : Type u} {xl : List α} {xs : ωSequence α} {n : ℕ} (h : xl.length ≤ n) : drop n (xl ++ω xs) = drop (n - xl.length) xs

theorem Cslib.ωSequence.take_theorem {α : Type u} (s₁ s₂ : ωSequence α) (h : ∀ (n : ℕ), take n s₁ = take n s₂) : s₁ = s₂

theorem Cslib.ωSequence.extract_eq_drop_take {α : Type u} {xs : ωSequence α} {m n : ℕ} : xs.extract m n = take (n - m) (drop m xs)

theorem Cslib.ωSequence.extract_eq_ofFn {α : Type u} {xs : ωSequence α} {m n : ℕ} : xs.extract m n = List.ofFn fun (k : Fin (n - m)) => xs (m + ↑k)

theorem Cslib.ωSequence.extract_eq_extract {α : Type u} {xs xs' : ωSequence α} {m n m' n' : ℕ} (h : xs.extract m n = xs'.extract m' n') : n - m = n' - m' ∧ ∀ k < n - m, xs (m + k) = xs' (m' + k)

theorem Cslib.ωSequence.extract_eq_take {α : Type u} {xs : ωSequence α} {n : ℕ} : xs.extract 0 n = take n xs

@[simp]

theorem Cslib.ωSequence.append_extract_drop {α : Type u} {xs : ωSequence α} {n : ℕ} : xs.extract 0 n ++ω drop n xs = xs

theorem Cslib.ωSequence.extract_append_right_right {α : Type u} {xl : List α} {xs : ωSequence α} {m n : ℕ} (h : xl.length ≤ m) : (xl ++ω xs).extract m n = xs.extract (m - xl.length) (n - xl.length)

theorem Cslib.ωSequence.extract_append_zero_right {α : Type u} {xl : List α} {xs : ωSequence α} {n : ℕ} (h : xl.length ≤ n) : (xl ++ω xs).extract 0 n = xl ++ xs.extract 0 (n - xl.length)

theorem Cslib.ωSequence.extract_drop {α : Type u} {xs : ωSequence α} {k m n : ℕ} : (drop k xs).extract m n = xs.extract (k + m) (k + n)

@[simp]

theorem Cslib.ωSequence.length_extract {α : Type u} {xs : ωSequence α} {m n : ℕ} : (xs.extract m n).length = n - m

@[simp]

theorem Cslib.ωSequence.extract_eq_nil {α : Type u} {xs : ωSequence α} {n : ℕ} : xs.extract n n = []

@[simp]

theorem Cslib.ωSequence.extract_eq_nil_iff {α : Type u} {xs : ωSequence α} {m n : ℕ} : xs.extract m n = [] ↔ n ≤ m

@[simp]

theorem Cslib.ωSequence.get_extract {α : Type u} {xs : ωSequence α} {m n k : ℕ} (h : k < n - m) : (xs.extract m n)[k] = xs (m + k)

theorem Cslib.ωSequence.append_extract_extract {α : Type u} {xs : ωSequence α} {k m n : ℕ} (h_km : k ≤ m) (h_mn : m ≤ n) : xs.extract k m ++ xs.extract m n = xs.extract k n

theorem Cslib.ωSequence.extract_succ_right {α : Type u} {xs : ωSequence α} {m n : ℕ} (h_mn : m ≤ n) : xs.extract m (n + 1) = xs.extract m n ++ [xs n]

@[simp]

theorem Cslib.ωSequence.extract_lu_extract_lu {α : Type u} {xs : ωSequence α} {m n i j : ℕ} (h : j ≤ n - m) : (xs.extract m n).extract i j = xs.extract (m + i) (m + j)

theorem Cslib.ωSequence.extract_0u_extract_lu {α : Type u} {xs : ωSequence α} {n i j : ℕ} (h : j ≤ n) : (xs.extract 0 n).extract i j = xs.extract i j

theorem Cslib.ωSequence.extract_0u_extract_l {α : Type u} {xs : ωSequence α} {n i : ℕ} : (xs.extract 0 n).extract i = xs.extract i n

@[simp]

theorem Cslib.ωSequence.take_extract {α : Type u} {xs : ωSequence α} {m n k : ℕ} (h : k ≤ n - m) : List.take k (xs.extract m n) = xs.extract m (m + k)

@[simp]

theorem Cslib.ωSequence.drop_extract {α : Type u} {xs : ωSequence α} {m n k : ℕ} (h : k ≤ n - m) : List.drop k (xs.extract m n) = xs.extract (m + k) n