mathlib documentation

data.stream.init

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

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

@[protected, instance]
def stream.inhabited {α : Type u_1} [inhabited α] :
Equations
@[protected]
theorem stream.eta {α : Type u} (s : stream α) :
theorem stream.nth_zero_cons {α : Type u} (a : α) (s : stream α) :
(a::s).nth 0 = a
theorem stream.head_cons {α : Type u} (a : α) (s : stream α) :
(a::s).head = a
theorem stream.tail_cons {α : Type u} (a : α) (s : stream α) :
(a::s).tail = s
theorem stream.tail_drop {α : Type u} (n : ) (s : stream α) :
theorem stream.nth_drop {α : Type u} (n m : ) (s : stream α) :
(stream.drop m s).nth n = s.nth (n + m)
theorem stream.tail_eq_drop {α : Type u} (s : stream α) :
theorem stream.drop_drop {α : Type u} (n m : ) (s : stream α) :
theorem stream.nth_succ {α : Type u} (n : ) (s : stream α) :
s.nth n.succ = s.tail.nth n
theorem stream.drop_succ {α : Type u} (n : ) (s : stream α) :
@[simp]
theorem stream.head_drop {α : Type u_1} (a : stream α) (n : ) :
(stream.drop n a).head = a.nth n
@[protected, ext]
theorem stream.ext {α : Type u} {s₁ s₂ : stream α} :
(∀ (n : ), s₁.nth n = s₂.nth n)s₁ = s₂
theorem stream.all_def {α : Type u} (p : α → Prop) (s : stream α) :
stream.all p s = ∀ (n : ), p (s.nth n)
theorem stream.any_def {α : Type u} (p : α → Prop) (s : stream α) :
stream.any p s = ∃ (n : ), p (s.nth n)
theorem stream.mem_cons {α : Type u} (a : α) (s : stream α) :
a a::s
theorem stream.mem_cons_of_mem {α : Type u} {a : α} {s : stream α} (b : α) :
a sa b::s
theorem stream.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : stream α} :
a b::sa = b a s
theorem stream.mem_of_nth_eq {α : Type u} {n : } {s : stream α} {a : α} :
a = s.nth na s
theorem stream.drop_map {α : Type u} {β : Type v} (f : α → β) (n : ) (s : stream α) :
theorem stream.nth_map {α : Type u} {β : Type v} (f : α → β) (n : ) (s : stream α) :
(stream.map f s).nth n = f (s.nth n)
theorem stream.tail_map {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
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 α) :
theorem stream.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : stream α) :
theorem stream.map_id {α : Type u} (s : stream α) :
theorem stream.map_map {α : Type u} {β : Type v} {δ : Type w} (g : β → δ) (f : α → β) (s : stream α) :
theorem stream.map_tail {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
theorem stream.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : stream α} :
a sf 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₂)
theorem stream.nth_zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (n : ) (s₁ : stream α) (s₂ : stream β) :
(stream.zip f s₁ s₂).nth n = f (s₁.nth n) (s₂.nth 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₂ = f s₁.head s₂.head::stream.zip f s₁.tail s₂.tail
theorem stream.mem_const {α : Type u} (a : α) :
theorem stream.const_eq {α : Type u} (a : α) :
theorem stream.tail_const {α : Type u} (a : α) :
theorem stream.map_const {α : Type u} {β : Type v} (f : α → β) (a : α) :
theorem stream.nth_const {α : Type u} (n : ) (a : α) :
theorem stream.drop_const {α : Type u} (n : ) (a : α) :
theorem stream.head_iterate {α : Type u} (f : α → α) (a : α) :
theorem stream.tail_iterate {α : Type u} (f : α → α) (a : α) :
theorem stream.iterate_eq {α : Type u} (f : α → α) (a : α) :
theorem stream.nth_zero_iterate {α : Type u} (f : α → α) (a : α) :
(stream.iterate f a).nth 0 = a
theorem stream.nth_succ_iterate {α : Type u} (n : ) (f : α → α) (a : α) :
def stream.is_bisimulation {α : Type u} (R : stream αstream α → Prop) :
Prop
Equations
theorem stream.nth_of_bisim {α : Type u} (R : stream αstream α → Prop) (bisim : stream.is_bisimulation R) {s₁ s₂ : stream α} (n : ) :
R s₁ s₂s₁.nth n = s₂.nth 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.is_bisimulation R) {s₁ s₂ : stream α} :
R s₁ s₂s₁ = s₂
theorem stream.bisim_simple {α : Type u} (s₁ s₂ : stream α) :
s₁.head = s₂.heads₁ = s₁.tails₂ = s₂.tails₁ = 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₂
theorem stream.iterate_id {α : Type u} (a : α) :
theorem stream.map_iterate {α : Type u} (f : α → α) (a : α) :
theorem stream.corec_def {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) :
theorem stream.corec_eq {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) :
stream.corec f g a = f a::stream.corec f g (g a)
theorem stream.corec_id_id_eq_const {α : Type u} (a : α) :
theorem stream.corec_id_f_eq_iterate {α : Type u} (f : α → α) (a : α) :
theorem stream.corec'_eq {α : Type u} {β : Type v} (f : α → β × α) (a : α) :
theorem stream.unfolds_eq {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) :
stream.unfolds g f a = g a::stream.unfolds g f (f a)
theorem stream.nth_unfolds_head_tail {α : Type u} (n : ) (s : stream α) :
theorem stream.interleave_eq {α : Type u} (s₁ s₂ : stream α) :
s₁ s₂ = s₁.head::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.nth_interleave_left {α : Type u} (n : ) (s₁ s₂ : stream α) :
(s₁ s₂).nth (2 * n) = s₁.nth n
theorem stream.nth_interleave_right {α : Type u} (n : ) (s₁ s₂ : stream α) :
(s₁ s₂).nth (2 * n + 1) = s₂.nth 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 α) :
theorem stream.head_even {α : Type u} (s : stream α) :
theorem stream.tail_even {α : Type u} (s : stream α) :
theorem stream.even_cons_cons {α : Type u} (a₁ a₂ : α) (s : stream α) :
(a₁::a₂::s).even = a₁::s.even
theorem stream.even_tail {α : Type u} (s : stream α) :
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.nth_even {α : Type u} (n : ) (s : stream α) :
s.even.nth n = s.nth (2 * n)
theorem stream.nth_odd {α : Type u} (n : ) (s : stream α) :
s.odd.nth n = s.nth (2 * n + 1)
theorem stream.mem_of_mem_even {α : Type u} (a : α) (s : stream α) :
a s.evena s
theorem stream.mem_of_mem_odd {α : Type u} (a : α) (s : stream α) :
a s.odda s
theorem stream.nil_append_stream {α : Type u} (s : stream α) :
theorem stream.cons_append_stream {α : Type u} (a : α) (l : list α) (s : stream α) :
a :: l ++ₛ s = 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 α) :
theorem stream.drop_append_stream {α : Type u} (l : list α) (s : stream α) :
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 sa l ++ₛ s
theorem stream.mem_append_stream_left {α : Type u} {a : α} {l : list α} (s : stream α) :
a la l ++ₛ s
@[simp]
theorem stream.take_zero {α : Type u} (s : stream α) :
@[simp]
theorem stream.take_succ {α : Type u} (n : ) (s : stream α) :
@[simp]
theorem stream.length_take {α : Type u} (n : ) (s : stream α) :
theorem stream.nth_take_succ {α : Type u} (n : ) (s : stream α) :
theorem stream.append_take_drop {α : Type u} (n : ) (s : stream α) :
theorem stream.take_theorem {α : Type u} (s₁ s₂ : stream α) :
(∀ (n : ), stream.take n s₁ = stream.take n s₂)s₁ = s₂
@[protected]
theorem stream.cycle_g_cons {α : Type u} (a a₁ : α) (l₁ : list α) (a₀ : α) (l₀ : list α) :
stream.cycle_g (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)
theorem stream.cycle_eq {α : Type u} (l : list α) (h : l list.nil) :
theorem stream.mem_cycle {α : Type u} {a : α} {l : list α} (h : l list.nil) :
a la stream.cycle l h
theorem stream.cycle_singleton {α : Type u} (a : α) (h : [a] list.nil) :
theorem stream.tails_eq {α : Type u} (s : stream α) :
theorem stream.nth_tails {α : Type u} (n : ) (s : stream α) :
theorem stream.tails_eq_iterate {α : Type u} (s : stream α) :
theorem stream.inits_core_eq {α : Type u} (l : list α) (s : stream α) :
theorem stream.tail_inits {α : Type u} (s : stream α) :
theorem stream.inits_tail {α : Type u} (s : stream α) :
theorem stream.cons_nth_inits_core {α : Type u} (a : α) (n : ) (l : list α) (s : stream α) :
theorem stream.nth_inits {α : Type u} (n : ) (s : stream α) :
theorem stream.inits_eq {α : Type u} (s : stream α) :
theorem stream.identity {α : Type u} (s : stream α) :
theorem stream.composition {α : Type u} {β : Type v} {δ : Type w} (g : stream (β → δ)) (f : stream (α → β)) (s : stream α) :
theorem stream.homomorphism {α : Type u} {β : Type v} (f : α → β) (a : α) :
theorem stream.interchange {α : Type u} {β : Type v} (fs : stream (α → β)) (a : α) :
fs stream.pure a = stream.pure (λ (f : α → β), f a) fs
theorem stream.map_eq_apply {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
theorem stream.nth_nats (n : ) :