Documentation

Mathlib.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. Note that we already have Stream to represent a similar object, hence the awkward naming.

def Stream' (α : Type u) :

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

Equations

Stream' α = (ℕ → α)

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

Prepend an element to a stream.

Equations

Stream'.cons a s x = match x with | 0 => a | Nat.succ n => s n

def Stream'.«term_::_» :

Lean.TrailingParserDescr

Equations

Stream'.«term_::_» = Lean.ParserDescr.trailingNode `Stream'.term_::_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))

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

α

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

Equations

Stream'.head s = s 0

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

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

Equations

Stream'.tail s 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

Stream'.nth s n = s n

def Stream'.All {α : Type u} (p : α → Prop) (s : Stream' α) :

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

Equations

Stream'.All p s = ((n : ℕ) → p (Stream'.nth s n))

def Stream'.Any {α : Type u} (p : α → Prop) (s : Stream' α) :

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

Equations

Stream'.Any p s = ∃ n, p (Stream'.nth s n)

instance Stream'.instMembershipStream' {α : Type u} :

Membership α (Stream' α)

a ∈ s means that a = Stream'.nth n s for some n.

Equations

Stream'.instMembershipStream' = { mem := fun a s => Stream'.Any (fun 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 (Stream'.nth s 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 (Stream'.nth s₁ n) (Stream'.nth s₂ n)

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

Stream' (ℕ × α)

Enumerate a stream by tagging each element with its index.

Equations

Stream'.enum s n = (n, Stream'.nth s n)

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

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

Equations

Stream'.const a x = a

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

Iterates of a function as a stream.

Equations

Stream'.iterate f a 0 = a
Stream'.iterate f a (Nat.succ n) = f (Stream'.iterate f a n)

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'.corecOn {α : Type u} {β : Type v} (a : α) (f : α → β) (g : α → α) :

Equations

Stream'.corecOn 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'.corecState {σ : Type u_1} {α : Type u_1} (cmd : StateM σ α) (s : σ) :

Use a state monad to generate a stream through corecursion

Equations

Stream'.corecState cmd s = Stream'.corec Prod.fst (StateT.run cmd ∘ Prod.snd) (StateT.run cmd 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₁ : Stream' α) (s₂ : Stream' α) :

Interleave two streams.

Equations

s₁ ⋈ s₂ = Stream'.corecOn (s₁, s₂) (fun x => match x with | (s₁, snd) => Stream'.head s₁) fun x => match x with | (s₁, s₂) => (s₂, Stream'.tail s₁)

def Stream'.«term_⋈_» :

Lean.TrailingParserDescr

Equations

Stream'.«term_⋈_» = Lean.ParserDescr.trailingNode `Stream'.term_⋈_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 66))

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

Elements of a stream with even indices.

Equations

Stream'.even s = Stream'.corec (fun s => Stream'.head s) (fun s => Stream'.tail (Stream'.tail s)) s

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

Elements of a stream with odd indices.

Equations

Stream'.odd s = Stream'.even (Stream'.tail s)

def Stream'.appendStream' {α : Type u} :

List α → Stream' α → Stream' α

Append a stream to a list.

Equations

[] ++ₛ x = x
a :: l ++ₛ x = Stream'.cons a (l ++ₛ x)

def Stream'.«term_++ₛ_» :

Lean.TrailingParserDescr

Equations

Stream'.«term_++ₛ_» = Lean.ParserDescr.trailingNode `Stream'.term_++ₛ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ₛ ") (Lean.ParserDescr.cat `term 66))

def Stream'.take {α : Type u} :

ℕ → Stream' α → List α

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

Equations

Stream'.take 0 x = []
Stream'.take (Nat.succ n) x = Stream'.head x :: Stream'.take n (Stream'.tail x)

def Stream'.cycleF {α : Type u} :

α × List α × α × List α → α

An auxiliary definition for Stream'.cycle corecursive def

Equations

Stream'.cycleF x = match x with | (v, fst, fst_1, snd) => v

def Stream'.cycleG {α : Type u} :

α × List α × α × List α → α × List α × α × List α

An auxiliary definition for Stream'.cycle corecursive def

Equations

Stream'.cycleG x = match x with | (fst, [], v₀, l₀) => (v₀, l₀, v₀, l₀) | (fst, v₂ :: l₂, v₀, l₀) => (v₂, l₂, v₀, l₀)

def Stream'.cycle {α : Type u} (l : List α) :

l ≠ [] → Stream' α

Interpret a nonempty list as a cyclic stream.

Equations

Stream'.cycle x x = match x, x with | [], h => absurd (_ : [] = []) h | a :: l, x => Stream'.corec Stream'.cycleF Stream'.cycleG (a, l, a, l)

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

Stream' (Stream' α)

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

Equations

Stream'.tails s = Stream'.corec id Stream'.tail (Stream'.tail s)

def Stream'.initsCore {α : Type u} (l : List α) (s : Stream' α) :

Stream' (List α)

An auxiliary definition for Stream'.inits.

Equations

One or more equations did not get rendered due to their size.

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

Stream' (List α)

Nonempty initial segments of a stream.

Equations

Stream'.inits s = Stream'.initsCore [Stream'.head s] (Stream'.tail s)

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 = Stream'.nth (α → β) f n (Stream'.nth s n)

def Stream'.«term_⊛_» :

Lean.TrailingParserDescr

Equations

Stream'.«term_⊛_» = Lean.ParserDescr.trailingNode `Stream'.term_⊛_ 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊛ ") (Lean.ParserDescr.cat `term 76))

def Stream'.nats :

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

Equations

Stream'.nats n = n