mathlib documentation

core.data.stream

def stream  :
Type uType u

Equations
def stream.cons {α : Type u} :
α → stream α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} :
stream α → α

Equations
def stream.tail {α : Type u} :
stream αstream α

Equations
def stream.drop {α : Type u} :
stream αstream α

Equations
def stream.nth {α : Type u} :
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} :
(α → Prop)stream α → Prop

Equations
def stream.any {α : Type u} :
(α → Prop)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} :
α → 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} :
(α → β)stream α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} :
(α → β → δ)stream αstream β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} :
α → stream α

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} :
(α → α)α → stream α

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} :
(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} :
(α → β)(α → α)α → stream β

Equations
def stream.corec_on {α : Type u} {β : Type v} :
α → (α → β)(α → α)stream β

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} :
(α → β × α)α → stream β

Equations
theorem stream.corec'_eq {α : Type u} {β : Type v} (f : α → β × α) (a : α) :

def stream.unfolds {α : Type u} {β : Type v} :
(α → β)(α → α)α → stream β

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} :
stream αstream α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} :
stream αstream α

Equations
def stream.odd {α : Type u} :
stream α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} :
stream αstream (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} :
list αstream αstream (list α)

Equations
def stream.inits {α : Type u} :
stream αstream (list α)

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} :
α → stream α

Equations
def stream.apply {α : Type u} {β : Type v} :
stream (α → β)stream α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