mathlib documentation

core / data.stream

def stream (α : Type u) :
Type u
Equations
def stream.cons {α : Type u} (a : α) (s : stream α) :
Equations
  • a :: s = λ (i : ), stream.cons._match_1 a s i
  • stream.cons._match_1 a s n.succ = s n
  • stream.cons._match_1 a s 0 = a
def stream.head {α : Type u} (s : stream α) :
α
Equations
def stream.tail {α : Type u} (s : stream α) :
Equations
def stream.drop {α : Type u} (n : ) (s : stream α) :
Equations
def stream.nth {α : Type u} (n : ) (s : stream α) :
α
Equations
theorem stream.eta {α : Type u} (s : stream α) :
s.head :: s.tail = s
theorem stream.nth_zero_cons {α : Type u} (a : α) (s : stream α) :
stream.nth 0 (a :: s) = 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 α) :
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 α) :
theorem stream.drop_succ {α : Type u} (n : ) (s : stream α) :
@[ext]
theorem stream.ext {α : Type u} {s₁ s₂ : stream α} :
(∀ (n : ), stream.nth n s₁ = stream.nth n s₂)s₁ = s₂
def stream.all {α : Type u} (p : α → Prop) (s : stream α) :
Prop
Equations
def stream.any {α : Type u} (p : α → Prop) (s : stream α) :
Prop
Equations
theorem stream.all_def {α : Type u} (p : α → Prop) (s : stream α) :
stream.all p s = ∀ (n : ), p (stream.nth n s)
theorem stream.any_def {α : Type u} (p : α → Prop) (s : stream α) :
stream.any p s = ∃ (n : ), p (stream.nth n s)
def stream.mem {α : Type u} (a : α) (s : stream α) :
Prop
Equations
@[instance]
def stream.has_mem {α : Type u} :
has_mem α (stream α)
Equations
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 = stream.nth n sa s
def stream.map {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
Equations
theorem stream.drop_map {α : Type u} {β : Type v} (f : α → β) (n : ) (s : stream α) :
theorem stream.nth_map {α : Type u} {β : Type v} (f : α → β) (n : ) (s : stream α) :
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 α) :
stream.map f (a :: s) = f a :: stream.map f s
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)
def stream.zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : stream α) (s₂ : stream β) :
Equations
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.nth n (stream.zip f s₁ s₂) = f (stream.nth n s₁) (stream.nth n s₂)
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
def stream.const {α : Type u} (a : α) :
Equations
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 : α) :
def stream.iterate {α : Type u} (f : α → α) (a : α) :
Equations
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 : α) :
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₂stream.nth n s₁ = stream.nth n s₂ 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 : α) :
def stream.corec {α : Type u} {β : Type v} (f : α → β) (g : α → α) :
α → stream β
Equations
def stream.corec_on {α : Type u} {β : Type v} (a : α) (f : α → β) (g : α → α) :
Equations
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 : α) :
def stream.corec' {α : Type u} {β : Type v} (f : α → β × α) :
α → stream β
Equations
theorem stream.corec'_eq {α : Type u} {β : Type v} (f : α → β × α) (a : α) :
def stream.unfolds {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) :
Equations
theorem stream.unfolds_eq {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) :
stream.unfolds g f a = g a :: stream.unfolds g f (f a)
def stream.interleave {α : Type u} (s₁ s₂ : stream α) :
Equations
  • s₁s₂ = stream.corec_on (s₁, s₂) (λ (_x : stream α × stream α), stream.interleave._match_1 _x) (λ (_x : stream α × stream α), stream.interleave._match_2 _x)
  • stream.interleave._match_1 (s₁, s₂) = s₁.head
  • stream.interleave._match_2 (s₁, s₂) = (s₂, s₁.tail)
theorem stream.interleave_eq {α : Type u} (s₁ s₂ : stream α) :
s₁s₂ = s₁.head :: s₂.head :: (s₁.tails₂.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₁.tails₂.tail = (s₁s₂).tail.tail
theorem stream.nth_interleave_left {α : Type u} (n : ) (s₁ s₂ : stream α) :
stream.nth (2 * n) (s₁s₂) = stream.nth n s₁
theorem stream.nth_interleave_right {α : Type u} (n : ) (s₁ s₂ : stream α) :
stream.nth (2 * n + 1) (s₁s₂) = stream.nth n s₂
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₂
def stream.even {α : Type u} (s : stream α) :
Equations
def stream.odd {α : Type u} (s : stream α) :
Equations
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₁.evens₁.odd = s₁
theorem stream.nth_even {α : Type u} (n : ) (s : stream α) :
theorem stream.nth_odd {α : Type u} (n : ) (s : stream α) :
stream.nth n s.odd = stream.nth (2 * n + 1) s
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
def stream.append_stream {α : Type u} :
list αstream αstream α
Equations
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 α) :
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
def stream.approx {α : Type u} :
stream αlist α
Equations
theorem stream.approx_zero {α : Type u} (s : stream α) :
theorem stream.approx_succ {α : Type u} (n : ) (s : stream α) :
theorem stream.nth_approx {α : Type u} (n : ) (s : stream α) :
theorem stream.append_approx_drop {α : Type u} (n : ) (s : stream α) :
theorem stream.take_theorem {α : Type u} (s₁ s₂ : stream α) :
(∀ (n : ), stream.approx n s₁ = stream.approx n s₂)s₁ = s₂
def stream.cycle {α : Type u} (l : list α) :
Equations
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) :
def stream.tails {α : Type u} (s : stream α) :
Equations
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 α) :
def stream.inits_core {α : Type u} (l : list α) (s : stream α) :
Equations
def stream.inits {α : Type u} (s : stream α) :
Equations
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 α) :
def stream.pure {α : Type u} (a : α) :
Equations
def stream.apply {α : Type u} {β : Type v} (f : stream (α → β)) (s : stream α) :
Equations
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 : α) :
fsstream.pure a = stream.pure (λ (f : α → β), f a)fs
theorem stream.map_eq_apply {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
Equations