data.stream.defs

# Definition of stream and functions on streams #

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) :
Type u

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

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

Prepend an element to a 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 α) :
α

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

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

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

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

Drop first n elements of a stream.

Equations
• s = λ (i : ), s (i + n)
def stream.nth {α : Type u} (s : stream α) (n : ) :
α

n-th element of a stream.

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

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

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

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

Equations
@[protected, instance]
def stream.has_mem {α : Type u} :
(stream α)

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

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

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

Equations
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
• s₁ s₂ = λ (n : ), f (s₁.nth n) (s₂.nth n)
def stream.const {α : Type u} (a : α) :

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

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

Iterates of a function as a stream.

Equations
• = λ (n : ), n.rec_on a (λ (n : ) (r : α), f r)
def stream.corec {α : Type u} {β : Type v} (f : α → β) (g : α → α) :
α →
Equations
• g = λ (a : α), a)
def stream.corec_on {α : Type u} {β : Type v} (a : α) (f : α → β) (g : α → α) :
Equations
• g = g a
def stream.corec' {α : Type u} {β : Type v} (f : α → β × α) :
α →
Equations
def stream.corec_state {σ α : Type u_1} (cmd : α) (s : σ) :

Use a state monad to generate a stream through corecursion

Equations
def stream.unfolds {α : Type u} {β : Type v} (g : α → β) (f : α → α) (a : α) :
Equations
• a = f a
def stream.interleave {α : Type u} (s₁ s₂ : stream α) :

Interleave two streams.

Equations
• s₁ s₂ = stream.corec_on (s₁, s₂) (λ (_x : × stream α), stream.interleave._match_1 _x) (λ (_x : × 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
def stream.odd {α : Type u} (s : stream α) :

Elements of a stream with odd indices.

Equations
def stream.append_stream {α : Type u} :
list α

Append a stream to a list.

Equations
def stream.take {α : Type u} :
list α

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

Equations
@[protected]
def stream.cycle_f {α : Type u} :
α × list α × α × list α → α

An auxiliary definition for stream.cycle corecursive def

Equations
@[protected]
def stream.cycle_g {α : Type u} :
α × list α × α × list αα × list α × α × list α

An auxiliary definition for stream.cycle corecursive def

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

Interpret a nonempty list as a cyclic stream.

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

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

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

An auxiliary definition for stream.inits.

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

Nonempty initial segments of a stream.

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

A constant stream, same as stream.const.

Equations
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
def stream.nats  :

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

Equations