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.
Prepend an element to a stream.
Equations
- Stream'.cons a s x = match x with | 0 => a | Nat.succ n => s n
Equations
- Stream'.«term_::_» = Lean.ParserDescr.trailingNode `Stream'.term_::_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))
Head of a stream: Stream'.head s = Stream'.nth s 0
.
Equations
- Stream'.head s = s 0
Tail of a stream: Stream'.tail (h :: t) = t
.
Equations
- Stream'.tail s i = s (i + 1)
Drop first n
elements of a stream.
Equations
- Stream'.drop n s i = s (i + n)
n
-th element of a stream.
Equations
- Stream'.nth s n = s n
Proposition saying that all elements of a stream satisfy a predicate.
Equations
- Stream'.All p s = ((n : ℕ) → p (Stream'.nth s n))
Proposition saying that at least one element of a stream satisfies a predicate.
Equations
- Stream'.Any p s = ∃ n, p (Stream'.nth s n)
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 }
Apply a function f
to all elements of a stream s
.
Equations
- Stream'.map f s n = f (Stream'.nth s n)
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)
Enumerate a stream by tagging each element with its index.
Equations
- Stream'.enum s n = (n, Stream'.nth s n)
The constant stream: Stream'.nth n (Stream'.const a) = a
.
Equations
- Stream'.const a x = 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)
Equations
- Stream'.corec f g a = Stream'.map f (Stream'.iterate g a)
Equations
- Stream'.corecOn a f g = Stream'.corec f g a
Equations
- Stream'.corec' f = Stream'.corec (Prod.fst ∘ f) (Prod.snd ∘ f)
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)
Equations
- Stream'.unfolds g f a = Stream'.corec g f a
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₁)
Equations
- Stream'.«term_⋈_» = Lean.ParserDescr.trailingNode `Stream'.term_⋈_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 66))
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
Elements of a stream with odd indices.
Equations
- Stream'.odd s = Stream'.even (Stream'.tail s)
Equations
- Stream'.«term_++ₛ_» = Lean.ParserDescr.trailingNode `Stream'.term_++ₛ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ₛ ") (Lean.ParserDescr.cat `term 66))
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)
An auxiliary definition for Stream'.cycle
corecursive def
Equations
- Stream'.cycleF x = match x with | (v, fst, fst_1, snd) => v
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)
Tails of a stream, starting with Stream'.tail s
.
Equations
- Stream'.tails s = Stream'.corec id Stream'.tail (Stream'.tail s)
An auxiliary definition for Stream'.inits
.
Equations
- One or more equations did not get rendered due to their size.
Nonempty initial segments of a stream.
Equations
- Stream'.inits s = Stream'.initsCore [Stream'.head s] (Stream'.tail s)
A constant stream, same as Stream'.const
.
Equations
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)
Equations
- Stream'.«term_⊛_» = Lean.ParserDescr.trailingNode `Stream'.term_⊛_ 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊛ ") (Lean.ParserDescr.cat `term 76))
The stream of natural numbers: Stream'.nth n Stream'.nats = n
.
Equations
- Stream'.nats n = n