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

Porting note: This file used to be in the core library. It was moved to mathlib and renamed to init to avoid name clashes.

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

theorem Stream'.drop_drop {α : Type u} (n m : ℕ) (s : Stream' α) : Stream'.drop n (Stream'.drop m s) = Stream'.drop (n + m) 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' α} : (Stream'.drop i s).tail = Stream'.drop (i + 1) s

@[simp]

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

theorem Stream'.tail_drop {α : Type u} (n : ℕ) (s : Stream' α) : (Stream'.drop n s).tail = Stream'.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 : α) : (Stream'.cons x s).get n.succ = s.get n

@[simp]

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

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

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

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

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

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

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

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

@[simp]

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

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

theorem Stream'.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : Stream' α} : a ∈ Stream'.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' α) : Stream'.drop n (Stream'.map f s) = Stream'.map f (Stream'.drop n s)

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem Stream'.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Stream' α} : b ∈ Stream'.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' β) : Stream'.drop n (Stream'.zip f s₁ s₂) = Stream'.zip f (Stream'.drop n s₁) (Stream'.drop n s₂)

@[simp]

theorem Stream'.get_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ℕ) (s₁ : Stream' α) (s₂ : Stream' β) : (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' β) : (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' β) : (Stream'.zip f s₁ s₂).tail = Stream'.zip f s₁.tail s₂.tail

theorem Stream'.zip_eq {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : Stream' α) (s₂ : Stream' β) : Stream'.zip f s₁ s₂ = Stream'.cons (f s₁.head s₂.head) (Stream'.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 = Stream'.zip Prod.mk Stream'.nats s

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

theorem Stream'.get_succ_iterate {α : Type u} (n : ℕ) (f : α → α) (a : α) : (Stream'.iterate f a).get n.succ = (Stream'.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 : Stream'.IsBisimulation R) {s₁ s₂ : Stream' α} (n : ℕ) : R s₁ s₂ → s₁.get n = s₂.get n ∧ R (Stream'.drop (n + 1) s₁) (Stream'.drop (n + 1) s₂)

theorem Stream'.eq_of_bisim {α : Type u} (R : Stream' α → Stream' α → Prop) (bisim : Stream'.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 : α) : Stream'.iterate id a = Stream'.const a

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

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

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

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

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

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

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

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

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

theorem Stream'.interleave_eq {α : Type u} (s₁ s₂ : Stream' α) : s₁ ⋈ s₂ = Stream'.cons s₁.head (Stream'.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' α) : (Stream'.cons a₁ (Stream'.cons a₂ s)).even = Stream'.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

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 = Stream'.cons a (l ++ₛ s)

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

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

theorem Stream'.drop_append_stream {α : Type u} (l : List α) (s : Stream' α) : 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' α) : Stream'.take 0 s = []

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

theorem Stream'.take_theorem {α : Type u} (s₁ s₂ : Stream' α) : (∀ (n : ℕ), Stream'.take n s₁ = Stream'.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 ≠ []) : Stream'.cycle l h = l ++ₛ Stream'.cycle l h

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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