Streams a.k.a. infinite lists a.k.a. infinite sequences

instance Stream'.instInhabited {α : Type u} [Inhabited α] : Inhabited (Stream' α)

Equations

• Stream'.instInhabited = { default := Stream'.const default }

@[simp]

theorem Stream'.eta {α : Type u} (s : Stream' α) : cons s.head s.tail = s

theorem Stream'.cons_head_tail {α : Type u} (s : Stream' α) : cons s.head s.tail = s

Alias for Stream'.eta to match List API.

theorem Stream'.ext {α : Type u} {s₁ s₂ : Stream' α} : (∀ (n : ℕ), s₁.get n = s₂.get n) → s₁ = s₂

theorem Stream'.ext_iff {α : Type u} {s₁ s₂ : Stream' α} : s₁ = s₂ ↔ ∀ (n : ℕ), s₁.get n = s₂.get n

@[simp]

theorem Stream'.get_zero_cons {α : Type u} (a : α) (s : Stream' α) : (cons a s).get 0 = a

@[simp]

theorem Stream'.head_cons {α : Type u} (a : α) (s : Stream' α) : (cons a s).head = a

@[simp]

theorem Stream'.tail_cons {α : Type u} (a : α) (s : Stream' α) : (cons a s).tail = s

@[simp]

theorem Stream'.get_drop {α : Type u} (n m : ℕ) (s : Stream' α) : (drop m s).get n = s.get (m + n)

theorem Stream'.tail_eq_drop {α : Type u} (s : Stream' α) : s.tail = drop 1 s

@[simp]

theorem Stream'.drop_drop {α : Type u} (n m : ℕ) (s : Stream' α) : drop n (drop m s) = drop (m + n) s

@[simp]

theorem Stream'.get_tail {α : Type u} {n : ℕ} {s : Stream' α} : s.tail.get n = s.get (n + 1)

@[simp]

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

@[simp]

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

theorem Stream'.tail_drop {α : Type u} (n : ℕ) (s : Stream' α) : (drop n s).tail = drop n s.tail

theorem Stream'.get_succ {α : Type u} (n : ℕ) (s : Stream' α) : s.get n.succ = s.tail.get n

@[simp]

theorem Stream'.get_succ_cons {α : Type u} (n : ℕ) (s : Stream' α) (x : α) : (cons x s).get n.succ = s.get n

@[simp]

theorem Stream'.get_cons_append_zero {α : Type u} {a : α} {x : List α} {s : Stream' α} : (a :: x ++ₛ s).get 0 = a

@[simp]

theorem Stream'.append_eq_cons {α : Type u} {a : α} {as : Stream' α} : [a] ++ₛ as = cons a as

@[simp]

theorem Stream'.drop_zero {α : Type u} {s : Stream' α} : drop 0 s = s

theorem Stream'.drop_succ {α : Type u} (n : ℕ) (s : Stream' α) : drop n.succ s = drop n s.tail

theorem Stream'.head_drop {α : Type u} (a : Stream' α) (n : ℕ) : (drop n a).head = a.get n

theorem Stream'.cons_injective2 {α : Type u} : Function.Injective2 cons

theorem Stream'.cons_injective_left {α : Type u} (s : Stream' α) : Function.Injective fun (x : α) => cons x s

theorem Stream'.cons_injective_right {α : Type u} (x : α) : Function.Injective (cons x)

theorem Stream'.all_def {α : Type u} (p : α → Prop) (s : Stream' α) : All p s = ∀ (n : ℕ), p (s.get n)

theorem Stream'.any_def {α : Type u} (p : α → Prop) (s : Stream' α) : Any p s = ∃ (n : ℕ), p (s.get n)

@[simp]

theorem Stream'.mem_cons {α : Type u} (a : α) (s : Stream' α) : a ∈ cons a s

theorem Stream'.mem_cons_of_mem {α : Type u} {a : α} {s : Stream' α} (b : α) : a ∈ s → a ∈ cons b s

theorem Stream'.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : Stream' α} : a ∈ cons b s → a = b ∨ a ∈ s

theorem Stream'.mem_of_get_eq {α : Type u} {n : ℕ} {s : Stream' α} {a : α} : a = s.get n → a ∈ s

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

@[simp]

theorem Stream'.get_map {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : Stream' α) : (map f s).get n = f (s.get n)

theorem Stream'.tail_map {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : (map f s).tail = map f s.tail

@[simp]

theorem Stream'.head_map {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : (map f s).head = f s.head

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

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

@[simp]

theorem Stream'.map_id {α : Type u} (s : Stream' α) : map id s = s

@[simp]

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

@[simp]

theorem Stream'.map_tail {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : map f s.tail = (map f s).tail

theorem Stream'.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Stream' α} : a ∈ s → f a ∈ map f s

theorem Stream'.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Stream' α} : b ∈ map f s → ∃ (a : α), a ∈ s ∧ f a = b

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

@[simp]

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

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

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

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

@[simp]

theorem Stream'.get_enum {α : Type u} (s : Stream' α) (n : ℕ) : s.enum.get n = (n, s.get n)

theorem Stream'.enum_eq_zip {α : Type u} (s : Stream' α) : s.enum = zip Prod.mk nats s

@[simp]

theorem Stream'.mem_const {α : Type u} (a : α) : a ∈ const a

theorem Stream'.const_eq {α : Type u} (a : α) : const a = cons a (const a)

@[simp]

theorem Stream'.tail_const {α : Type u} (a : α) : (const a).tail = const a

@[simp]

theorem Stream'.map_const {α : Type u} {β : Type v} (f : α → β) (a : α) : map f (const a) = const (f a)

@[simp]

theorem Stream'.get_const {α : Type u} (n : ℕ) (a : α) : (const a).get n = a

@[simp]

theorem Stream'.drop_const {α : Type u} (n : ℕ) (a : α) : drop n (const a) = const a

@[simp]

theorem Stream'.head_iterate {α : Type u} (f : α → α) (a : α) : (iterate f a).head = a

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

theorem Stream'.tail_iterate {α : Type u} (f : α → α) (a : α) : (iterate f a).tail = iterate f (f a)

theorem Stream'.iterate_eq {α : Type u} (f : α → α) (a : α) : iterate f a = cons a (iterate f (f a))

@[simp]

theorem Stream'.get_zero_iterate {α : Type u} (f : α → α) (a : α) : (iterate f a).get 0 = a

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

def Stream'.IsBisimulation {α : Type u} (R : Stream' α → Stream' α → Prop) : Prop

Streams s₁ and s₂ are defined to be bisimulations if their heads are equal and tails are bisimulations.

Equations

• Stream'.IsBisimulation R = ∀ ⦃s₁ s₂ : Stream' α⦄, R s₁ s₂ → s₁.head = s₂.head ∧ R s₁.tail s₂.tail

theorem Stream'.get_of_bisim {α : Type u} (R : Stream' α → Stream' α → Prop) (bisim : IsBisimulation R) {s₁ s₂ : Stream' α} (n : ℕ) : R s₁ s₂ → s₁.get n = s₂.get n ∧ R (drop (n + 1) s₁) (drop (n + 1) s₂)

theorem Stream'.eq_of_bisim {α : Type u} (R : Stream' α → Stream' α → Prop) (bisim : IsBisimulation R) {s₁ s₂ : Stream' α} : R s₁ s₂ → s₁ = s₂

theorem Stream'.bisim_simple {α : Type u} (s₁ s₂ : Stream' α) : s₁.head = s₂.head → s₁ = s₁.tail → s₂ = s₂.tail → s₁ = s₂

theorem Stream'.coinduction {α : Type u} {s₁ s₂ : Stream' α} : s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂

@[simp]

theorem Stream'.iterate_id {α : Type u} (a : α) : iterate id a = const a

theorem Stream'.map_iterate {α : Type u} (f : α → α) (a : α) : iterate f (f a) = map f (iterate f a)

theorem Stream'.corec_def {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) : corec f g a = map f (iterate g a)

theorem Stream'.corec_eq {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) : corec f g a = cons (f a) (corec f g (g a))

theorem Stream'.corec_id_id_eq_const {α : Type u} (a : α) : corec id id a = const a

theorem Stream'.corec_id_f_eq_iterate {α : Type u} (f : α → α) (a : α) : corec id f a = iterate f a

theorem Stream'.corec'_eq {α : Type u} {β : Type v} (f : α → β × α) (a : α) : corec' f a = cons (f a).fst (corec' f (f a).snd)

theorem Stream'.unfolds_eq {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) : unfolds g f a = cons (g a) (unfolds g f (f a))

theorem Stream'.get_unfolds_head_tail {α : Type u} (n : ℕ) (s : Stream' α) : (unfolds head tail s).get n = s.get n

theorem Stream'.unfolds_head_eq {α : Type u} (s : Stream' α) : unfolds head tail s = s

theorem Stream'.interleave_eq {α : Type u} (s₁ s₂ : Stream' α) : s₁ ⋈ s₂ = cons s₁.head (cons s₂.head (s₁.tail ⋈ s₂.tail))

theorem Stream'.tail_interleave {α : Type u} (s₁ s₂ : Stream' α) : (s₁ ⋈ s₂).tail = s₂ ⋈ s₁.tail

theorem Stream'.interleave_tail_tail {α : Type u} (s₁ s₂ : Stream' α) : s₁.tail ⋈ s₂.tail = (s₁ ⋈ s₂).tail.tail

theorem Stream'.get_interleave_left {α : Type u} (n : ℕ) (s₁ s₂ : Stream' α) : (s₁ ⋈ s₂).get (2 * n) = s₁.get n

theorem Stream'.get_interleave_right {α : Type u} (n : ℕ) (s₁ s₂ : Stream' α) : (s₁ ⋈ s₂).get (2 * n + 1) = s₂.get n

theorem Stream'.mem_interleave_left {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α) : a ∈ s₁ → a ∈ s₁ ⋈ s₂

theorem Stream'.mem_interleave_right {α : Type u} {a : α} {s₁ : Stream' α} (s₂ : Stream' α) : a ∈ s₂ → a ∈ s₁ ⋈ s₂

theorem Stream'.odd_eq {α : Type u} (s : Stream' α) : s.odd = s.tail.even

@[simp]

theorem Stream'.head_even {α : Type u} (s : Stream' α) : s.even.head = s.head

theorem Stream'.tail_even {α : Type u} (s : Stream' α) : s.even.tail = s.tail.tail.even

theorem Stream'.even_cons_cons {α : Type u} (a₁ a₂ : α) (s : Stream' α) : (cons a₁ (cons a₂ s)).even = cons a₁ s.even

theorem Stream'.even_tail {α : Type u} (s : Stream' α) : s.tail.even = s.odd

theorem Stream'.even_interleave {α : Type u} (s₁ s₂ : Stream' α) : (s₁ ⋈ s₂).even = s₁

theorem Stream'.interleave_even_odd {α : Type u} (s₁ : Stream' α) : s₁.even ⋈ s₁.odd = s₁

theorem Stream'.get_even {α : Type u} (n : ℕ) (s : Stream' α) : s.even.get n = s.get (2 * n)

theorem Stream'.get_odd {α : Type u} (n : ℕ) (s : Stream' α) : s.odd.get n = s.get (2 * n + 1)

theorem Stream'.mem_of_mem_even {α : Type u} (a : α) (s : Stream' α) : a ∈ s.even → a ∈ s

theorem Stream'.mem_of_mem_odd {α : Type u} (a : α) (s : Stream' α) : a ∈ s.odd → a ∈ s

@[simp]

theorem Stream'.nil_append_stream {α : Type u} (s : Stream' α) : [] ++ₛ s = s

theorem Stream'.cons_append_stream {α : Type u} (a : α) (l : List α) (s : Stream' α) : a :: l ++ₛ s = cons a (l ++ₛ s)

@[simp]

theorem Stream'.append_append_stream {α : Type u} (l₁ l₂ : List α) (s : Stream' α) : l₁ ++ l₂ ++ₛ s = l₁ ++ₛ (l₂ ++ₛ s)

theorem Stream'.get_append_left {α : Type u} (n : ℕ) (x : List α) (a : Stream' α) (h : n < x.length) : (x ++ₛ a).get n = x[n]

@[simp]

theorem Stream'.get_append_right {α : Type u} (n : ℕ) (x : List α) (a : Stream' α) : (x ++ₛ a).get (x.length + n) = a.get n

@[simp]

theorem Stream'.get_append_length {α : Type u} (x : List α) (a : Stream' α) : (x ++ₛ a).get x.length = a.get 0

theorem Stream'.append_right_injective {α : Type u} (x : List α) (a b : Stream' α) (h : x ++ₛ a = x ++ₛ b) : a = b

@[simp]

theorem Stream'.append_right_inj {α : Type u} (x : List α) (a b : Stream' α) : x ++ₛ a = x ++ₛ b ↔ a = b

theorem Stream'.append_left_injective {α : Type u} (x y : List α) (a b : Stream' α) (h : x ++ₛ a = y ++ₛ b) (hl : x.length = y.length) : x = y

theorem Stream'.map_append_stream {α : Type u} {β : Type v} (f : α → β) (l : List α) (s : Stream' α) : map f (l ++ₛ s) = List.map f l ++ₛ map f s

theorem Stream'.drop_append_stream {α : Type u} (l : List α) (s : Stream' α) : drop l.length (l ++ₛ s) = s

theorem Stream'.append_stream_head_tail {α : Type u} (s : Stream' α) : [s.head] ++ₛ s.tail = s

theorem Stream'.mem_append_stream_right {α : Type u} {a : α} (l : List α) {s : Stream' α} : a ∈ s → a ∈ l ++ₛ s

theorem Stream'.mem_append_stream_left {α : Type u} {a : α} {l : List α} (s : Stream' α) : a ∈ l → a ∈ l ++ₛ s

@[simp]

theorem Stream'.take_zero {α : Type u} (s : Stream' α) : take 0 s = []

theorem Stream'.take_succ {α : Type u} (n : ℕ) (s : Stream' α) : take n.succ s = s.head :: take n s.tail

@[simp]

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

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

@[simp]

theorem Stream'.length_take {α : Type u} (n : ℕ) (s : Stream' α) : (take n s).length = n

@[simp]

theorem Stream'.take_take {α : Type u} {s : Stream' α} {m n : ℕ} : List.take m (take n s) = take (min n m) s

@[simp]

theorem Stream'.concat_take_get {α : Type u} {n : ℕ} {s : Stream' α} : take n s ++ [s.get n] = take (n + 1) s

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

@[deprecated Stream'.getElem?_take (since := "2025-02-14")]

theorem Stream'.get?_take {α : Type u} {s : Stream' α} {k n : ℕ} : k < n → (take n s)[k]? = some (s.get k)

Alias of Stream'.getElem?_take.

theorem Stream'.getElem?_take_succ {α : Type u} (n : ℕ) (s : Stream' α) : (take n.succ s)[n]? = some (s.get n)

@[deprecated Stream'.getElem?_take_succ (since := "2025-02-14")]

theorem Stream'.get?_take_succ {α : Type u} (n : ℕ) (s : Stream' α) : (take n.succ s)[n]? = some (s.get n)

Alias of Stream'.getElem?_take_succ.

@[simp]

theorem Stream'.dropLast_take {α : Type u} {n : ℕ} {xs : Stream' α} : (take n xs).dropLast = take (n - 1) xs

@[simp]

theorem Stream'.append_take_drop {α : Type u} (n : ℕ) (s : Stream' α) : take n s ++ₛ drop n s = s

theorem Stream'.append_take {α : Type u} (n : ℕ) (x : List α) (a : Stream' α) : x ++ take n a = take (x.length + n) (x ++ₛ a)

@[simp]

theorem Stream'.take_get {α : Type u} (m n : ℕ) (a : Stream' α) (h : m < (take n a).length) : (take n a)[m] = a.get m

theorem Stream'.take_append_of_le_length {α : Type u} (n : ℕ) (x : List α) (a : Stream' α) (h : n ≤ x.length) : take n (x ++ₛ a) = List.take n x

theorem Stream'.take_add {α : Type u} (m n : ℕ) (a : Stream' α) : take (m + n) a = take m a ++ take n (drop m a)

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

@[simp]

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

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

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

theorem Stream'.drop_append_of_le_length {α : Type u} (n : ℕ) (x : List α) (a : Stream' α) (h : n ≤ x.length) : drop n (x ++ₛ a) = List.drop n x ++ₛ a

theorem Stream'.take_theorem {α : Type u} (s₁ s₂ : Stream' α) : (∀ (n : ℕ), take n s₁ = take n s₂) → s₁ = s₂

theorem Stream'.cycle_g_cons {α : Type u} (a a₁ : α) (l₁ : List α) (a₀ : α) (l₀ : List α) : Stream'.cycleG (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)

theorem Stream'.cycle_eq {α : Type u} (l : List α) (h : l ≠ []) : cycle l h = l ++ₛ cycle l h

theorem Stream'.mem_cycle {α : Type u} {a : α} {l : List α} (h : l ≠ []) : a ∈ l → a ∈ cycle l h

@[simp]

theorem Stream'.cycle_singleton {α : Type u} (a : α) : cycle [a] ⋯ = const a

theorem Stream'.tails_eq {α : Type u} (s : Stream' α) : s.tails = cons s.tail s.tail.tails

@[simp]

theorem Stream'.get_tails {α : Type u} (n : ℕ) (s : Stream' α) : s.tails.get n = drop n s.tail

theorem Stream'.tails_eq_iterate {α : Type u} (s : Stream' α) : s.tails = iterate tail s.tail

theorem Stream'.inits_core_eq {α : Type u} (l : List α) (s : Stream' α) : initsCore l s = cons l (initsCore (l ++ [s.head]) s.tail)

theorem Stream'.tail_inits {α : Type u} (s : Stream' α) : s.inits.tail = initsCore [s.head, s.tail.head] s.tail.tail

theorem Stream'.inits_tail {α : Type u} (s : Stream' α) : s.tail.inits = initsCore [s.tail.head] s.tail.tail

theorem Stream'.cons_get_inits_core {α : Type u} (a : α) (n : ℕ) (l : List α) (s : Stream' α) : a :: (initsCore l s).get n = (initsCore (a :: l) s).get n

@[simp]

theorem Stream'.get_inits {α : Type u} (n : ℕ) (s : Stream' α) : s.inits.get n = take n.succ s

theorem Stream'.inits_eq {α : Type u} (s : Stream' α) : s.inits = cons [s.head] (map (List.cons s.head) s.tail.inits)

theorem Stream'.zip_inits_tails {α : Type u} (s : Stream' α) : zip appendStream' s.inits s.tails = const s

theorem Stream'.identity {α : Type u} (s : Stream' α) : pure id ⊛ s = s

theorem Stream'.composition {α : Type u} {β : Type v} {δ : Type w} (g : Stream' (β → δ)) (f : Stream' (α → β)) (s : Stream' α) : pure Function.comp ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s)

theorem Stream'.homomorphism {α : Type u} {β : Type v} (f : α → β) (a : α) : pure f ⊛ pure a = pure (f a)

theorem Stream'.interchange {α : Type u} {β : Type v} (fs : Stream' (α → β)) (a : α) : fs ⊛ pure a = (pure fun (f : α → β) => f a) ⊛ fs

theorem Stream'.map_eq_apply {α : Type u} {β : Type v} (f : α → β) (s : Stream' α) : map f s = pure f ⊛ s

theorem Stream'.get_nats (n : ℕ) : nats.get n = n

theorem Stream'.nats_eq : nats = cons 0 (map Nat.succ nats)