mathlib3 documentation

data.stream.defs

Definition of `stream` and functions on streams #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A stream stream α is an infinite sequence of elements of α. One can also think about it as an infinite list. In this file we define stream and some functions that take and/or return streams.

def stream (α : Type u) :

A stream stream α is an infinite sequence of elements of α.

Equations

stream α = (ℕ → α)

Instances for stream

def stream.cons {α : Type u} (a : α) (s : stream α) :

Prepend an element to a stream.

Equations

(a::s) (n + 1) = s n
(a::s) 0 = a

def stream.head {α : Type u} (s : stream α) :

α

Head of a stream: stream.head s = stream.nth 0 s.

Equations

s.head = s 0

def stream.tail {α : Type u} (s : stream α) :

Tail of a stream: stream.tail (h :: t) = t.

Equations

s.tail = λ (i : ℕ), s (i + 1)

def stream.drop {α : Type u} (n : ℕ) (s : stream α) :

Drop first n elements of a stream.

Equations

stream.drop n s = λ (i : ℕ), s (i + n)

def stream.nth {α : Type u} (s : stream α) (n : ℕ) :

α

n-th element of a stream.

Equations

s.nth n = s n

def stream.all {α : Type u} (p : α → Prop) (s : stream α) :

Prop

Proposition saying that all elements of a stream satisfy a predicate.

Equations

stream.all p s = ∀ (n : ℕ), p (s.nth n)

def stream.any {α : Type u} (p : α → Prop) (s : stream α) :

Prop

Proposition saying that at least one element of a stream satisfies a predicate.

Equations

stream.any p s = ∃ (n : ℕ), p (s.nth n)

@[protected, instance]

def stream.has_mem {α : Type u} :

has_mem α (stream α)

a ∈ s means that a = stream.nth n s for some n.

Equations

stream.has_mem = {mem := λ (a : α) (s : stream α), stream.any (λ (b : α), a = b) s}

def stream.map {α : Type u} {β : Type v} (f : α → β) (s : stream α) :

Apply a function f to all elements of a stream s.

Equations

stream.map f s = λ (n : ℕ), f (s.nth n)

def stream.zip {α : Type u} {β : Type v} {δ : Type w} (f : α → β → δ) (s₁ : stream α) (s₂ : stream β) :

Zip two streams using a binary operation: stream.nth n (stream.zip f s₁ s₂) = f (stream.nth s₁) (stream.nth s₂).

Equations

stream.zip f s₁ s₂ = λ (n : ℕ), f (s₁.nth n) (s₂.nth n)

def stream.enum {α : Type u} (s : stream α) :

stream (ℕ × α)

Enumerate a stream by tagging each element with its index.

Equations

s.enum = λ (n : ℕ), (n, s.nth n)

def stream.const {α : Type u} (a : α) :

The constant stream: stream.nth n (stream.const a) = a.

Equations

stream.const a = λ (n : ℕ), a

def stream.iterate {α : Type u} (f : α → α) (a : α) :

Iterates of a function as a stream.

Equations

stream.iterate f a = λ (n : ℕ), n.rec_on a (λ (n : ℕ) (r : α), f r)

def stream.corec {α : Type u} {β : Type v} (f : α → β) (g : α → α) :

α → stream β

Equations

stream.corec f g = λ (a : α), stream.map f (stream.iterate g a)

def stream.corec_on {α : Type u} {β : Type v} (a : α) (f : α → β) (g : α → α) :

Equations

stream.corec_on a f g = stream.corec f g a

def stream.corec' {α : Type u} {β : Type v} (f : α → β × α) :

α → stream β

Equations

stream.corec' f = stream.corec (prod.fst ∘ f) (prod.snd ∘ f)

def stream.corec_state {σ α : Type u_1} (cmd : state σ α) (s : σ) :

Use a state monad to generate a stream through corecursion

Equations

stream.corec_state cmd s = stream.corec prod.fst (cmd.run ∘ prod.snd) (cmd.run s)

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

Equations

stream.unfolds g f a = stream.corec g f a

def stream.interleave {α : Type u} (s₁ s₂ : stream α) :

Interleave two streams.

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)

def stream.even {α : Type u} (s : stream α) :

Elements of a stream with even indices.

Equations

s.even = stream.corec (λ (s : stream α), s.head) (λ (s : stream α), s.tail.tail) s

def stream.odd {α : Type u} (s : stream α) :

Elements of a stream with odd indices.

Equations

s.odd = s.tail.even

def stream.append_stream {α : Type u} :

list α → stream α → stream α

Append a stream to a list.

Equations

a :: l ++ₛ s = a::(l ++ₛ s)
list.nil ++ₛ s = s

def stream.take {α : Type u} :

ℕ → stream α → list α

take n s returns a list of the n first elements of stream s

Equations

stream.take (n + 1) s = s.head :: stream.take n s.tail
stream.take 0 s = list.nil

@[protected]

def stream.cycle_f {α : Type u} :

α × list α × α × list α → α

An auxiliary definition for stream.cycle corecursive def

Equations

stream.cycle_f (v, _x, _x_1, _x_2) = v

@[protected]

def stream.cycle_g {α : Type u} :

α × list α × α × list α → α × list α × α × list α

An auxiliary definition for stream.cycle corecursive def

Equations

stream.cycle_g (v₁, v₂ :: l₂, v₀, l₀) = (v₂, l₂, v₀, l₀)
stream.cycle_g (v₁, list.nil α, v₀, l₀) = (v₀, l₀, v₀, l₀)

def stream.cycle {α : Type u} (l : list α) :

l ≠ list.nil → stream α

Interpret a nonempty list as a cyclic stream.

Equations

stream.cycle (a :: l) h = stream.corec stream.cycle_f stream.cycle_g (a, l, a, l)
stream.cycle list.nil h = absurd stream.cycle._main._proof_1 h

def stream.tails {α : Type u} (s : stream α) :

stream (stream α)

Tails of a stream, starting with stream.tail s.

Equations

s.tails = stream.corec id stream.tail s.tail

def stream.inits_core {α : Type u} (l : list α) (s : stream α) :

stream (list α)

An auxiliary definition for stream.inits.

Equations

stream.inits_core l s = stream.corec_on (l, s) (λ (_x : list α × stream α), stream.inits_core._match_1 _x) (λ (p : list α × stream α), stream.inits_core._match_2 p)
stream.inits_core._match_1 (a, b) = a
stream.inits_core._match_2 (l', s') = (l' ++ [s'.head], s'.tail)

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

stream (list α)

Nonempty initial segments of a stream.

Equations

s.inits = stream.inits_core [s.head] s.tail

def stream.pure {α : Type u} (a : α) :

A constant stream, same as stream.const.

Equations

stream.pure a = stream.const a

def stream.apply {α : Type u} {β : Type v} (f : stream (α → β)) (s : stream α) :

Given a stream of functions and a stream of values, apply n-th function to n-th value.

Equations

f ⊛ s = λ (n : ℕ), f.nth n (s.nth n)

def stream.nats :

The stream of natural numbers: stream.nth n stream.nats = n.

Equations

stream.nats = λ (n : ℕ), n