Definition of ωSequence and functions on infinite sequences

An ωSequence α is an infinite sequence of elements of α. It is basically a wrapper around the type ℕ → α which supports the dot-notation and the analogues of many familiar API functions of List α. In particular, the element at postion n : ℕ of s : ωSequence α is obtained using the function application notation s n.

In this file we define ωSequence and its API functions. Most code below is adapted from Mathlib.Data.Stream.Defs.

structure Cslib.ωSequence (α : Type u) : Type u

An ωSequence α is an infinite sequence of elements of α.

• get : ℕ → α

  The function that defines this infinite sequence.

instance Cslib.instFunLikeωSequenceNat {α : Type u} : FunLike (ωSequence α) ℕ α

Equations

• Cslib.instFunLikeωSequenceNat = { coe := Cslib.ωSequence.get, coe_injective' := ⋯ }

instance Cslib.instCoeForallNatωSequence {α : Type u} : Coe (ℕ → α) (ωSequence α)

Equations

• Cslib.instCoeForallNatωSequence = { coe := fun (f : ℕ → α) => { get := f } }

@[reducible, inline]

abbrev Cslib.ωSequence.head {α : Type u} (s : ωSequence α) : α

Head of an ω-sequence: ωSequence.head s = ωSequence s 0.

Equations

• s.head = s 0

def Cslib.ωSequence.tail {α : Type u} (s : ωSequence α) : ωSequence α

Tail of an ω-sequence: ωSequence.tail (h :: t) = t.

Equations

• s.tail = { get := fun (i : ℕ) => s (i + 1) }

def Cslib.ωSequence.drop {α : Type u} (n : ℕ) (s : ωSequence α) : ωSequence α

Drop first n elements of an ω-sequence.

Equations

• Cslib.ωSequence.drop n s = { get := fun (i : ℕ) => s (i + n) }

def Cslib.ωSequence.take {α : Type u} : ℕ → ωSequence α → List α

take n s returns a list of the n first elements of ω-sequence s

Equations

• Cslib.ωSequence.take 0 x✝ = []
• Cslib.ωSequence.take n.succ x✝ = x✝.head :: Cslib.ωSequence.take n x✝.tail

def Cslib.ωSequence.extract {α : Type u} (xs : ωSequence α) (m n : ℕ) : List α

Get the list containing the elements of xs from position m to n - 1.

Equations

• xs.extract m n = Cslib.ωSequence.take (n - m) (Cslib.ωSequence.drop m xs)

def Cslib.ωSequence.cons {α : Type u} (a : α) (s : ωSequence α) : ωSequence α

Prepend an element to an ω-sequence.

Equations

• Cslib.ωSequence.cons a s = { get := fun (x : ℕ) => match x with | 0 => a | n.succ => s n }

def Cslib.ωSequence.«term_::ω_» : Lean.TrailingParserDescr

Prepend an element to an ω-sequence.

Equations

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

def Cslib.ωSequence.appendωSequence {α : Type u} : List α → ωSequence α → ωSequence α

Append an ω-sequence to a list.

Equations

• [] ++ω x✝ = x✝
• a :: l ++ω x✝ = Cslib.ωSequence.cons a (l ++ω x✝)

def Cslib.ωSequence.«term_++ω_» : Lean.TrailingParserDescr

Append an ω-sequence to a list.

Equations

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

def Cslib.ωSequence.const {α : Type u} (a : α) : ωSequence α

The constant ω-sequence: ωSequence n (ωSequence.const a) = a.

Equations

• Cslib.ωSequence.const a = { get := fun (x : ℕ) => a }

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

Apply a function f to all elements of an ω-sequence s.

Equations

• Cslib.ωSequence.map f s = { get := fun (n : ℕ) => f (s n) }

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

Zip two ω-sequences using a binary operation: ωSequence n (ωSequence.zip f s₁ s₂) = f (ωSequence s₁) (ωSequence s₂).

Equations

• Cslib.ωSequence.zip f s₁ s₂ = { get := fun (n : ℕ) => f (s₁ n) (s₂ n) }

def Cslib.ωSequence.iterate {α : Type u} (f : α → α) (a : α) : ωSequence α

Iterates of a function as an ω-sequence.

Equations

• Cslib.ωSequence.iterate f a = { get := fun (n : ℕ) => f^[n] a }