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 0 = a
- Stream'.cons a s n.succ = s n
Instances For
Equations
- Stream'.«term_::_» = Lean.ParserDescr.trailingNode `Stream'.term_::_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))
Instances For
Head of a stream: Stream'.head s = Stream'.get s 0
.
Equations
- s.head = s.get 0
Instances For
Tail of a stream: Stream'.tail (h :: t) = t
.
Instances For
Proposition saying that all elements of a stream satisfy a predicate.
Equations
- Stream'.All p s = ∀ (n : ℕ), p (s.get n)
Instances For
Proposition saying that at least one element of a stream satisfies a predicate.
Equations
- Stream'.Any p s = ∃ (n : ℕ), p (s.get n)
Instances For
a ∈ s
means that a = Stream'.get n s
for some n
.
Equations
- Stream'.instMembership = { mem := fun (s : Stream' α) (a : α) => 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 (s.get n)
Instances For
Zip two streams using a binary operation:
Stream'.get n (Stream'.zip f s₁ s₂) = f (Stream'.get s₁) (Stream'.get s₂)
.
Equations
- Stream'.zip f s₁ s₂ n = f (s₁.get n) (s₂.get n)
Instances For
The constant stream: Stream'.get n (Stream'.const a) = a
.
Equations
- Stream'.const a x = a
Instances For
Iterates of a function as a stream.
Equations
- Stream'.iterate f a 0 = a
- Stream'.iterate f a n.succ = f (Stream'.iterate f a n)
Instances For
Equations
- Stream'.corec f g a = Stream'.map f (Stream'.iterate g a)
Instances For
Equations
- Stream'.corecOn a f g = Stream'.corec f g a
Instances For
Equations
- Stream'.corec' f = Stream'.corec (Prod.fst ∘ f) (Prod.snd ∘ f)
Instances For
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)
Instances For
Equations
- Stream'.«term_⋈_» = Lean.ParserDescr.trailingNode `Stream'.term_⋈_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋈ ") (Lean.ParserDescr.cat `term 66))
Instances For
Elements of a stream with even indices.
Equations
- s.even = Stream'.corec Stream'.head (fun (s : Stream' α) => s.tail.tail) s
Instances For
Equations
- Stream'.«term_++ₛ_» = Lean.ParserDescr.trailingNode `Stream'.term_++ₛ_ 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ₛ ") (Lean.ParserDescr.cat `term 66))
Instances For
take n s
returns a list of the n
first elements of stream s
Equations
- Stream'.take 0 x = []
- Stream'.take n.succ x = x.head :: Stream'.take n x.tail
Instances For
An auxiliary definition for Stream'.cycle
corecursive def
Equations
- Stream'.cycleF (v, fst, fst_1, snd) = v
Instances For
An auxiliary definition for Stream'.cycle
corecursive def
Equations
- Stream'.cycleG (fst, [], v₀, l₀) = (v₀, l₀, v₀, l₀)
- Stream'.cycleG (fst, v₂ :: l₂, v₀, l₀) = (v₂, l₂, v₀, l₀)
Instances For
Interpret a nonempty list as a cyclic stream.
Equations
- Stream'.cycle [] h = absurd ⋯ h
- Stream'.cycle (a :: l) x_2 = Stream'.corec Stream'.cycleF Stream'.cycleG (a, l, a, l)
Instances For
Tails of a stream, starting with Stream'.tail s
.
Equations
- s.tails = Stream'.corec id Stream'.tail s.tail
Instances For
An auxiliary definition for Stream'.inits
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Nonempty initial segments of a stream.
Equations
- s.inits = Stream'.initsCore [s.head] s.tail
Instances For
Equations
- Stream'.«term_⊛_» = Lean.ParserDescr.trailingNode `Stream'.term_⊛_ 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊛ ") (Lean.ParserDescr.cat `term 76))
Instances For
The stream of natural numbers: Stream'.get n Stream'.nats = n
.
Equations
- Stream'.nats n = n