mathlib documentation

core / data.stream

source
def stream (α : Type u) :
Type u
Equations
source
def stream.cons {α : Type u} (a : α) (s : 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
source
def stream.head {α : Type u} (s : stream α) :
α
Equations
source
def stream.tail {α : Type u} (s : stream α) :
stream α
Equations
source
def stream.drop {α : Type u} (n : ℕ) (s : stream α) :
stream α
Equations
source
def stream.nth {α : Type u} (n : ℕ) (s : stream α) :
α
Equations
source
@[protected]
theorem stream.eta {α : Type u} (s : stream α) :
s.head :: s.tail = s
source
theorem stream.nth_zero_cons {α : Type u} (a : α) (s : stream α) :
stream.nth 0 (a :: s) = a
source
theorem stream.head_cons {α : Type u} (a : α) (s : stream α) :
(a :: s).head = a
source
theorem stream.tail_cons {α : Type u} (a : α) (s : stream α) :
(a :: s).tail = s
source
theorem stream.tail_drop {α : Type u} (n : ℕ) (s : stream α) :
(stream.drop n s).tail = stream.drop n s.tail
source
theorem stream.nth_drop {α : Type u} (n m : ℕ) (s : stream α) :
stream.nth n (stream.drop m s) = stream.nth (n + m) s
source
theorem stream.tail_eq_drop {α : Type u} (s : stream α) :
s.tail = stream.drop 1 s
source
theorem stream.drop_drop {α : Type u} (n m : ℕ) (s : stream α) :
stream.drop n (stream.drop m s) = stream.drop (n + m) s
source
theorem stream.nth_succ {α : Type u} (n : ℕ) (s : stream α) :
stream.nth n.succ s = stream.nth n s.tail
source
theorem stream.drop_succ {α : Type u} (n : ℕ) (s : stream α) :
stream.drop n.succ s = stream.drop n s.tail
source
@[protected, ext]
theorem stream.ext {α : Type u} {s₁ s₂ : stream α} :
(∀ (n : ℕ), stream.nth n s₁ = stream.nth n s₂) → s₁ = s₂
source
def stream.all {α : Type u} (p : α → Prop) (s : stream α) :
Prop
Equations
source
def stream.any {α : Type u} (p : α → Prop) (s : stream α) :
Prop
Equations
source
theorem stream.all_def {α : Type u} (p : α → Prop) (s : stream α) :
stream.all p s = ∀ (n : ℕ), p (stream.nth n s)
source
theorem stream.any_def {α : Type u} (p : α → Prop) (s : stream α) :
stream.any p s = ∃ (n : ℕ), p (stream.nth n s)
source
@[protected]
def stream.mem {α : Type u} (a : α) (s : stream α) :
Prop
Equations
source
@[protected, instance]
def stream.has_mem {α : Type u} :
has_mem α (stream α)
Equations
source
theorem stream.mem_cons {α : Type u} (a : α) (s : stream α) :
a ∈ a :: s
source
theorem stream.mem_cons_of_mem {α : Type u} {a : α} {s : stream α} (b : α) :
a ∈ s → a ∈ b :: s
source
theorem stream.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : stream α} :
a ∈ b :: s → a = b ∨ a ∈ s
source
theorem stream.mem_of_nth_eq {α : Type u} {n : ℕ} {s : stream α} {a : α} :
a = stream.nth n s → a ∈ s
source
def stream.map {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
stream β
Equations
source
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)
source
theorem stream.nth_map {α : Type u} {β : Type v} (f : α → β) (n : ℕ) (s : stream α) :
stream.nth n (stream.map f s) = f (stream.nth n s)
source
theorem stream.tail_map {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
(stream.map f s).tail = stream.map f s.tail
source
theorem stream.head_map {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
(stream.map f s).head = f s.head
source
theorem stream.map_eq {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
stream.map f s = f s.head :: stream.map f s.tail
source
theorem stream.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : stream α) :
stream.map f (a :: s) = f a :: stream.map f s
source
theorem stream.map_id {α : Type u} (s : stream α) :
stream.map id s = s
source
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
source
theorem stream.map_tail {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
stream.map f s.tail = (stream.map f s).tail
source
theorem stream.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : stream α} :
a ∈ s → f a ∈ stream.map f s
source
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)
source
def stream.zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : stream α) (s₂ : stream β) :
stream δ
Equations
source
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₂)
source
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₂)
source
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
source
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
source
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
source
def stream.const {α : Type u} (a : α) :
stream α
Equations
source
theorem stream.mem_const {α : Type u} (a : α) :
a ∈ stream.const a
source
theorem stream.const_eq {α : Type u} (a : α) :
stream.const a = a :: stream.const a
source
theorem stream.tail_const {α : Type u} (a : α) :
(stream.const a).tail = stream.const a
source
theorem stream.map_const {α : Type u} {β : Type v} (f : α → β) (a : α) :
stream.map f (stream.const a) = stream.const (f a)
source
theorem stream.nth_const {α : Type u} (n : ℕ) (a : α) :
stream.nth n (stream.const a) = a
source
theorem stream.drop_const {α : Type u} (n : ℕ) (a : α) :
stream.drop n (stream.const a) = stream.const a
source
def stream.iterate {α : Type u} (f : α → α) (a : α) :
stream α
Equations
source
theorem stream.head_iterate {α : Type u} (f : α → α) (a : α) :
(stream.iterate f a).head = a
source
theorem stream.tail_iterate {α : Type u} (f : α → α) (a : α) :
(stream.iterate f a).tail = stream.iterate f (f a)
source
theorem stream.iterate_eq {α : Type u} (f : α → α) (a : α) :
stream.iterate f a = a :: stream.iterate f (f a)
source
theorem stream.nth_zero_iterate {α : Type u} (f : α → α) (a : α) :
stream.nth 0 (stream.iterate f a) = a
source
theorem stream.nth_succ_iterate {α : Type u} (n : ℕ) (f : α → α) (a : α) :
stream.nth n.succ (stream.iterate f a) = stream.nth n (stream.iterate f (f a))
source
def stream.is_bisimulation {α : Type u} (R : stream α → stream α → Prop) :
Prop
Equations
source
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₂)
source
theorem stream.eq_of_bisim {α : Type u} (R : stream α → stream α → Prop) (bisim : stream.is_bisimulation R) {s₁ s₂ : stream α} :
R s₁ s₂ → s₁ = s₂
source
theorem stream.bisim_simple {α : Type u} (s₁ s₂ : stream α) :
s₁.head = s₂.head → s₁ = s₁.tail → s₂ = s₂.tail → s₁ = s₂
source
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₂
source
theorem stream.iterate_id {α : Type u} (a : α) :
stream.iterate id a = stream.const a
source
theorem stream.map_iterate {α : Type u} (f : α → α) (a : α) :
stream.iterate f (f a) = stream.map f (stream.iterate f a)
source
def stream.corec {α : Type u} {β : Type v} (f : α → β) (g : α → α) :
α → stream β
Equations
source
def stream.corec_on {α : Type u} {β : Type v} (a : α) (f : α → β) (g : α → α) :
stream β
Equations
source
theorem stream.corec_def {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) :
stream.corec f g a = stream.map f (stream.iterate g a)
source
theorem stream.corec_eq {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α) :
stream.corec f g a = f a :: stream.corec f g (g a)
source
theorem stream.corec_id_id_eq_const {α : Type u} (a : α) :
stream.corec id id a = stream.const a
source
theorem stream.corec_id_f_eq_iterate {α : Type u} (f : α → α) (a : α) :
stream.corec id f a = stream.iterate f a
source
def stream.corec' {α : Type u} {β : Type v} (f : α → β × α) :
α → stream β
Equations
source
theorem stream.corec'_eq {α : Type u} {β : Type v} (f : α → β × α) (a : α) :
stream.corec' f a = (f a).fst :: stream.corec' f (f a).snd
source
def stream.unfolds {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) :
stream β
Equations
source
theorem stream.unfolds_eq {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) :
stream.unfolds g f a = g a :: stream.unfolds g f (f a)
source
theorem stream.nth_unfolds_head_tail {α : Type u} (n : ℕ) (s : stream α) :
stream.nth n (stream.unfolds stream.head stream.tail s) = stream.nth n s
source
theorem stream.unfolds_head_eq {α : Type u} (s : stream α) :
stream.unfolds stream.head stream.tail s = s
source
def stream.interleave {α : Type u} (s₁ s₂ : 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)
source
theorem stream.interleave_eq {α : Type u} (s₁ s₂ : stream α) :
s₁⋈s₂ = s₁.head :: s₂.head :: (s₁.tail⋈s₂.tail)
source
theorem stream.tail_interleave {α : Type u} (s₁ s₂ : stream α) :
(s₁⋈s₂).tail = s₂⋈s₁.tail
source
theorem stream.interleave_tail_tail {α : Type u} (s₁ s₂ : stream α) :
s₁.tail⋈s₂.tail = (s₁⋈s₂).tail.tail
source
theorem stream.nth_interleave_left {α : Type u} (n : ℕ) (s₁ s₂ : stream α) :
stream.nth (2 * n) (s₁⋈s₂) = stream.nth n s₁
source
theorem stream.nth_interleave_right {α : Type u} (n : ℕ) (s₁ s₂ : stream α) :
stream.nth (2 * n + 1) (s₁⋈s₂) = stream.nth n s₂
source
theorem stream.mem_interleave_left {α : Type u} {a : α} {s₁ : stream α} (s₂ : stream α) :
a ∈ s₁ → a ∈ s₁⋈s₂
source
theorem stream.mem_interleave_right {α : Type u} {a : α} {s₁ : stream α} (s₂ : stream α) :
a ∈ s₂ → a ∈ s₁⋈s₂
source
def stream.even {α : Type u} (s : stream α) :
stream α
Equations
source
def stream.odd {α : Type u} (s : stream α) :
stream α
Equations
source
theorem stream.odd_eq {α : Type u} (s : stream α) :
s.odd = s.tail.even
source
theorem stream.head_even {α : Type u} (s : stream α) :
s.even.head = s.head
source
theorem stream.tail_even {α : Type u} (s : stream α) :
s.even.tail = s.tail.tail.even
source
theorem stream.even_cons_cons {α : Type u} (a₁ a₂ : α) (s : stream α) :
(a₁ :: a₂ :: s).even = a₁ :: s.even
source
theorem stream.even_tail {α : Type u} (s : stream α) :
s.tail.even = s.odd
source
theorem stream.even_interleave {α : Type u} (s₁ s₂ : stream α) :
(s₁⋈s₂).even = s₁
source
theorem stream.interleave_even_odd {α : Type u} (s₁ : stream α) :
s₁.even⋈s₁.odd = s₁
source
theorem stream.nth_even {α : Type u} (n : ℕ) (s : stream α) :
stream.nth n s.even = stream.nth (2 * n) s
source
theorem stream.nth_odd {α : Type u} (n : ℕ) (s : stream α) :
stream.nth n s.odd = stream.nth (2 * n + 1) s
source
theorem stream.mem_of_mem_even {α : Type u} (a : α) (s : stream α) :
a ∈ s.even → a ∈ s
source
theorem stream.mem_of_mem_odd {α : Type u} (a : α) (s : stream α) :
a ∈ s.odd → a ∈ s
source
def stream.append_stream {α : Type u} :
list α → stream α → stream α
Equations
source
theorem stream.nil_append_stream {α : Type u} (s : stream α) :
list.nil++ₛs = s
source
theorem stream.cons_append_stream {α : Type u} (a : α) (l : list α) (s : stream α) :
a :: l++ₛs = a :: (l++ₛs)
source
theorem stream.append_append_stream {α : Type u} (l₁ l₂ : list α) (s : stream α) :
l₁ ++ l₂++ₛs = l₁++ₛ(l₂++ₛs)
source
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
source
theorem stream.drop_append_stream {α : Type u} (l : list α) (s : stream α) :
stream.drop l.length (l++ₛs) = s
source
theorem stream.append_stream_head_tail {α : Type u} (s : stream α) :
[s.head]++ₛs.tail = s
source
theorem stream.mem_append_stream_right {α : Type u} {a : α} (l : list α) {s : stream α} :
a ∈ s → a ∈ l++ₛs
source
theorem stream.mem_append_stream_left {α : Type u} {a : α} {l : list α} (s : stream α) :
a ∈ l → a ∈ l++ₛs
source
def stream.approx {α : Type u} :
ℕ → stream α → list α
Equations
source
theorem stream.approx_zero {α : Type u} (s : stream α) :
stream.approx 0 s = list.nil
source
theorem stream.approx_succ {α : Type u} (n : ℕ) (s : stream α) :
stream.approx n.succ s = s.head :: stream.approx n s.tail
source
theorem stream.nth_approx {α : Type u} (n : ℕ) (s : stream α) :
(stream.approx n.succ s).nth n = some (stream.nth n s)
source
theorem stream.append_approx_drop {α : Type u} (n : ℕ) (s : stream α) :
stream.approx n s++ₛstream.drop n s = s
source
theorem stream.take_theorem {α : Type u} (s₁ s₂ : stream α) :
(∀ (n : ℕ), stream.approx n s₁ = stream.approx n s₂) → s₁ = s₂
source
def stream.cycle {α : Type u} (l : list α) :
l ≠ list.nil → stream α
Equations
source
theorem stream.cycle_eq {α : Type u} (l : list α) (h : l ≠ list.nil) :
stream.cycle l h = l++ₛstream.cycle l h
source
theorem stream.mem_cycle {α : Type u} {a : α} {l : list α} (h : l ≠ list.nil) :
a ∈ l → a ∈ stream.cycle l h
source
theorem stream.cycle_singleton {α : Type u} (a : α) (h : [a] ≠ list.nil) :
stream.cycle [a] h = stream.const a
source
def stream.tails {α : Type u} (s : stream α) :
stream (stream α)
Equations
source
theorem stream.tails_eq {α : Type u} (s : stream α) :
s.tails = s.tail :: s.tail.tails
source
theorem stream.nth_tails {α : Type u} (n : ℕ) (s : stream α) :
stream.nth n s.tails = stream.drop n s.tail
source
theorem stream.tails_eq_iterate {α : Type u} (s : stream α) :
s.tails = stream.iterate stream.tail s.tail
source
def stream.inits_core {α : Type u} (l : list α) (s : stream α) :
stream (list α)
Equations
source
def stream.inits {α : Type u} (s : stream α) :
stream (list α)
Equations
source
theorem stream.inits_core_eq {α : Type u} (l : list α) (s : stream α) :
stream.inits_core l s = l :: stream.inits_core (l ++ [s.head]) s.tail
source
theorem stream.tail_inits {α : Type u} (s : stream α) :
s.inits.tail = stream.inits_core [s.head, s.tail.head] s.tail.tail
source
theorem stream.inits_tail {α : Type u} (s : stream α) :
s.tail.inits = stream.inits_core [s.tail.head] s.tail.tail
source
theorem stream.cons_nth_inits_core {α : Type u} (a : α) (n : ℕ) (l : list α) (s : stream α) :
a :: stream.nth n (stream.inits_core l s) = stream.nth n (stream.inits_core (a :: l) s)
source
theorem stream.nth_inits {α : Type u} (n : ℕ) (s : stream α) :
stream.nth n s.inits = stream.approx n.succ s
source
theorem stream.inits_eq {α : Type u} (s : stream α) :
s.inits = [s.head] :: stream.map (list.cons s.head) s.tail.inits
source
theorem stream.zip_inits_tails {α : Type u} (s : stream α) :
stream.zip stream.append_stream s.inits s.tails = stream.const s
source
def stream.pure {α : Type u} (a : α) :
stream α
Equations
source
def stream.apply {α : Type u} {β : Type v} (f : stream (α → β)) (s : stream α) :
stream β
Equations
source
theorem stream.identity {α : Type u} (s : stream α) :
stream.pure id⊛s = s
source
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)
source
theorem stream.homomorphism {α : Type u} {β : Type v} (f : α → β) (a : α) :
stream.pure f⊛stream.pure a = stream.pure (f a)
source
theorem stream.interchange {α : Type u} {β : Type v} (fs : stream (α → β)) (a : α) :
fs⊛stream.pure a = stream.pure (λ (f : α → β), f a)⊛fs
source
theorem stream.map_eq_apply {α : Type u} {β : Type v} (f : α → β) (s : stream α) :
stream.map f s = stream.pure f⊛s
source
def stream.nats  :
stream ℕ
Equations
source
theorem stream.nth_nats (n : ℕ) :
stream.nth n stream.nats = n
source
theorem stream.nats_eq  :
stream.nats = 0 :: stream.map nat.succ stream.nats