# Documentation

Mathlib.Data.Seq.Seq

# Possibly infinite lists #

This file provides a Seq α type representing possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

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

A stream s : Option α is a sequence if s.nth n = none implies s.nth (n + 1) = none.

Instances For
def Stream'.Seq (α : Type u) :

Seq α is the type of possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

Instances For
def Stream'.Seq1 (α : Type u_1) :
Type u_1

Seq1 α is the type of nonempty sequences.

Instances For
def Stream'.Seq.nil {α : Type u} :

The empty sequence

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

Prepend an element to a sequence

Instances For
@[simp]
theorem Stream'.Seq.val_cons {α : Type u} (s : ) (x : α) :
↑() = Stream'.cons (some x) s
def Stream'.Seq.get? {α : Type u} :

Get the nth element of a sequence (if it exists)

Instances For
@[simp]
theorem Stream'.Seq.get?_mk {α : Type u} (f : Stream' ()) (hf : ) :
Stream'.Seq.get? { val := f, property := hf } = f
@[simp]
theorem Stream'.Seq.get?_nil {α : Type u} (n : ) :
Stream'.Seq.get? Stream'.Seq.nil n = none
@[simp]
theorem Stream'.Seq.get?_cons_zero {α : Type u} (a : α) (s : ) :
= some a
@[simp]
theorem Stream'.Seq.get?_cons_succ {α : Type u} (a : α) (s : ) (n : ) :
Stream'.Seq.get? () (n + 1) =
theorem Stream'.Seq.ext {α : Type u} {s : } {t : } (h : ∀ (n : ), ) :
s = t
theorem Stream'.Seq.cons_right_injective {α : Type u} (x : α) :
def Stream'.Seq.TerminatedAt {α : Type u} (s : ) (n : ) :

A sequence has terminated at position n if the value at position n equals none.

Instances For
instance Stream'.Seq.terminatedAtDecidable {α : Type u} (s : ) (n : ) :

It is decidable whether a sequence terminates at a given position.

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

A sequence terminates if there is some position n at which it has terminated.

Instances For
theorem Stream'.Seq.not_terminates_iff {α : Type u} {s : } :
∀ (n : ),
def Stream'.Seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : βγ) :
Option (α × β)Option (α × γ)

Functorial action of the functor Option (α × _)

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

Get the first element of a sequence

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

Get the tail of a sequence (or nil if the sequence is nil)

Instances For
def Stream'.Seq.Mem {α : Type u} (a : α) (s : ) :

member definition for Seq

Instances For
theorem Stream'.Seq.le_stable {α : Type u} (s : ) {m : } {n : } (h : m n) :
= none = none
theorem Stream'.Seq.terminated_stable {α : Type u} (s : ) {m : } {n : } :
m n

If a sequence terminated at position n, it also terminated at m ≥ n .

theorem Stream'.Seq.ge_stable {α : Type u} (s : ) {aₙ : α} {n : } {m : } (m_le_n : m n) (s_nth_eq_some : = some aₙ) :
aₘ, = some aₘ

If s.get? n = some aₙ for some value aₙ, then there is also some value aₘ such that s.get? = some aₘ for m ≤ n.

theorem Stream'.Seq.not_mem_nil {α : Type u} (a : α) :
¬a Stream'.Seq.nil
theorem Stream'.Seq.mem_cons {α : Type u} (a : α) (s : ) :
a
theorem Stream'.Seq.mem_cons_of_mem {α : Type u} (y : α) {a : α} {s : } :
a sa
theorem Stream'.Seq.eq_or_mem_of_mem_cons {α : Type u} {a : α} {b : α} {s : } :
a a = b a s
@[simp]
theorem Stream'.Seq.mem_cons_iff {α : Type u} {a : α} {b : α} {s : } :
a a = b a s
def Stream'.Seq.destruct {α : Type u} (s : ) :

Destructor for a sequence, resulting in either none (for nil) or some (a, s) (for cons a s).

Instances For
theorem Stream'.Seq.destruct_eq_nil {α : Type u} {s : } :
= nones = Stream'.Seq.nil
theorem Stream'.Seq.destruct_eq_cons {α : Type u} {s : } {a : α} {s' : } :
= some (a, s')s =
@[simp]
theorem Stream'.Seq.destruct_nil {α : Type u} :
Stream'.Seq.destruct Stream'.Seq.nil = none
@[simp]
theorem Stream'.Seq.destruct_cons {α : Type u} (a : α) (s : ) :
= some (a, s)
theorem Stream'.Seq.head_eq_destruct {α : Type u} (s : ) :
= Prod.fst <\$>
@[simp]
theorem Stream'.Seq.head_nil {α : Type u} :
@[simp]
theorem Stream'.Seq.head_cons {α : Type u} (a : α) (s : ) :
@[simp]
theorem Stream'.Seq.tail_nil {α : Type u} :
Stream'.Seq.tail Stream'.Seq.nil = Stream'.Seq.nil
@[simp]
theorem Stream'.Seq.tail_cons {α : Type u} (a : α) (s : ) :
@[simp]
theorem Stream'.Seq.get?_tail {α : Type u} (s : ) (n : ) :
def Stream'.Seq.recOn {α : Type u} {C : Sort v} (s : ) (h1 : C Stream'.Seq.nil) (h2 : (x : α) → (s : ) → C ()) :
C s

Recursion principle for sequences, compare with List.recOn.

Instances For
theorem Stream'.Seq.mem_rec_on {α : Type u} {C : } {a : α} {s : } (M : a s) (h1 : (b : α) → (s' : ) → a = b C s'C ()) :
C s
def Stream'.Seq.Corec.f {α : Type u} {β : Type v} (f : βOption (α × β)) :
×

Corecursor over pairs of Option values

Instances For
def Stream'.Seq.corec {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) :

Corecursor for Seq α as a coinductive type. Iterates f to produce new elements of the sequence until none is obtained.

Instances For
@[simp]
theorem Stream'.Seq.corec_eq {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) :
def Stream'.Seq.BisimO {α : Type u} (R : ) :
Prop

Bisimilarity relation over Option of Seq1 α

Instances For
def Stream'.Seq.IsBisimulation {α : Type u} (R : ) :

a relation is bisimilar if it meets the BisimO test

Instances For
theorem Stream'.Seq.eq_of_bisim {α : Type u} (R : ) (bisim : ) {s₁ : } {s₂ : } (r : R s₁ s₂) :
s₁ = s₂
theorem Stream'.Seq.coinduction {α : Type u} {s₁ : } {s₂ : } :
(∀ (β : Type u) (fr : β), fr s₁ = fr s₂fr () = fr ()) → s₁ = s₂
theorem Stream'.Seq.coinduction2 {α : Type u} {β : Type v} (s : ) (f : ) (g : ) (H : ∀ (s : ), Stream'.Seq.BisimO (fun s1 s2 => s, s1 = f s s2 = g s) (Stream'.Seq.destruct (f s)) (Stream'.Seq.destruct (g s))) :
f s = g s
def Stream'.Seq.ofList {α : Type u} (l : List α) :

Embed a list as a sequence

Instances For
instance Stream'.Seq.coeList {α : Type u} :
Coe (List α) ()
@[simp]
theorem Stream'.Seq.ofList_nil {α : Type u} :
[] = Stream'.Seq.nil
@[simp]
theorem Stream'.Seq.ofList_nth {α : Type u} (l : List α) (n : ) :
@[simp]
theorem Stream'.Seq.ofList_cons {α : Type u} (a : α) (l : List α) :
↑(a :: l) =
def Stream'.Seq.ofStream {α : Type u} (s : ) :

Embed an infinite stream as a sequence

Instances For
instance Stream'.Seq.coeStream {α : Type u} :
Coe () ()
def Stream'.Seq.ofLazyList {α : Type u} :

Embed a LazyList α as a sequence. Note that even though this is non-meta, it will produce infinite sequences if used with cyclic LazyLists created by meta constructions.

Instances For
instance Stream'.Seq.coeLazyList {α : Type u} :
Coe () ()
unsafe def Stream'.Seq.toLazyList {α : Type u} :

Translate a sequence into a LazyList. Since LazyList and List are isomorphic as non-meta types, this function is necessarily meta.

Instances For
unsafe def Stream'.Seq.forceToList {α : Type u} (s : ) :
List α

Translate a sequence to a list. This function will run forever if run on an infinite sequence.

Instances For

The sequence of natural numbers some 0, some 1, ...

Instances For
@[simp]
theorem Stream'.Seq.nats_get? (n : ) :
def Stream'.Seq.append {α : Type u} (s₁ : ) (s₂ : ) :

Append two sequences. If s₁ is infinite, then s₁ ++ s₂ = s₁, otherwise it puts s₂ at the location of the nil in s₁.

Instances For
def Stream'.Seq.map {α : Type u} {β : Type v} (f : αβ) :

Map a function over a sequence.

Instances For
def Stream'.Seq.join {α : Type u} :

Flatten a sequence of sequences. (It is required that the sequences be nonempty to ensure productivity; in the case of an infinite sequence of nil, the first element is never generated.)

Instances For
def Stream'.Seq.drop {α : Type u} (s : ) :

Remove the first n elements from the sequence.

Equations
Instances For
def Stream'.Seq.take {α : Type u} :
List α

Take the first n elements of the sequence (producing a list)

Equations
• = []
• = match with | none => [] | some (x, r) => x ::
Instances For
def Stream'.Seq.splitAt {α : Type u} :
List α ×

Split a sequence at n, producing a finite initial segment and an infinite tail.

Equations
• One or more equations did not get rendered due to their size.
• = ([], x)
Instances For
def Stream'.Seq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s₁ : ) (s₂ : ) :

Combine two sequences with a function

Instances For
@[simp]
theorem Stream'.Seq.get?_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s : ) (s' : ) (n : ) :
def Stream'.Seq.zip {α : Type u} {β : Type v} :
Stream'.Seq (α × β)

Pair two sequences into a sequence of pairs

Instances For
theorem Stream'.Seq.get?_zip {α : Type u} {β : Type v} (s : ) (t : ) (n : ) :
= Option.map₂ Prod.mk () ()
def Stream'.Seq.unzip {α : Type u} {β : Type v} (s : Stream'.Seq (α × β)) :

Separate a sequence of pairs into two sequences

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

Enumerate a sequence by tagging each element with its index.

Instances For
@[simp]
theorem Stream'.Seq.get?_enum {α : Type u} (s : ) (n : ) :
= Option.map () ()
@[simp]
theorem Stream'.Seq.enum_nil {α : Type u} :
Stream'.Seq.enum Stream'.Seq.nil = Stream'.Seq.nil
def Stream'.Seq.toList {α : Type u} (s : ) (h : ) :
List α

Convert a sequence which is known to terminate into a list

Instances For
def Stream'.Seq.toStream {α : Type u} (s : ) (h : ) :

Convert a sequence which is known not to terminate into a stream

Instances For
def Stream'.Seq.toListOrStream {α : Type u} (s : ) :
List α

Convert a sequence into either a list or a stream depending on whether it is finite or infinite. (Without decidability of the infiniteness predicate, this is not constructively possible.)

Instances For
@[simp]
theorem Stream'.Seq.nil_append {α : Type u} (s : ) :
Stream'.Seq.append Stream'.Seq.nil s = s
@[simp]
theorem Stream'.Seq.cons_append {α : Type u} (a : α) (s : ) (t : ) :
=
@[simp]
theorem Stream'.Seq.append_nil {α : Type u} (s : ) :
Stream'.Seq.append s Stream'.Seq.nil = s
@[simp]
theorem Stream'.Seq.append_assoc {α : Type u} (s : ) (t : ) (u : ) :
@[simp]
theorem Stream'.Seq.map_nil {α : Type u} {β : Type v} (f : αβ) :
Stream'.Seq.map f Stream'.Seq.nil = Stream'.Seq.nil
@[simp]
theorem Stream'.Seq.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (s : ) :
@[simp]
theorem Stream'.Seq.map_id {α : Type u} (s : ) :
= s
@[simp]
theorem Stream'.Seq.map_tail {α : Type u} {β : Type v} (f : αβ) (s : ) :
theorem Stream'.Seq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : ) :
@[simp]
theorem Stream'.Seq.map_append {α : Type u} {β : Type v} (f : αβ) (s : ) (t : ) :
@[simp]
theorem Stream'.Seq.map_get? {α : Type u} {β : Type v} (f : αβ) (s : ) (n : ) :
@[simp]
theorem Stream'.Seq.join_nil {α : Type u} :
Stream'.Seq.join Stream'.Seq.nil = Stream'.Seq.nil
theorem Stream'.Seq.join_cons_nil {α : Type u} (a : α) (S : ) :
Stream'.Seq.join (Stream'.Seq.cons (a, Stream'.Seq.nil) S) =
theorem Stream'.Seq.join_cons_cons {α : Type u} (a : α) (b : α) (s : ) (S : ) :
@[simp]
theorem Stream'.Seq.join_cons {α : Type u} (a : α) (s : ) (S : ) :
@[simp]
theorem Stream'.Seq.join_append {α : Type u} (S : ) (T : ) :
@[simp]
theorem Stream'.Seq.ofStream_cons {α : Type u} (a : α) (s : ) :
↑() =
@[simp]
theorem Stream'.Seq.ofList_append {α : Type u} (l : List α) (l' : List α) :
↑(l ++ l') = Stream'.Seq.append l l'
@[simp]
theorem Stream'.Seq.ofStream_append {α : Type u} (l : List α) (s : ) :
↑(l ++ₛ s) =
def Stream'.Seq.toList' {α : Type u_1} (s : ) :

Convert a sequence into a list, embedded in a computation to allow for the possibility of infinite sequences (in which case the computation never returns anything).

Instances For
theorem Stream'.Seq.dropn_add {α : Type u} (s : ) (m : ) (n : ) :
theorem Stream'.Seq.dropn_tail {α : Type u} (s : ) (n : ) :
@[simp]
theorem Stream'.Seq.head_dropn {α : Type u} (s : ) (n : ) :
theorem Stream'.Seq.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : } :
a sf a
theorem Stream'.Seq.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : } :
b a, a s f a = b
theorem Stream'.Seq.of_mem_append {α : Type u} {s₁ : } {s₂ : } {a : α} (h : a ) :
a s₁ a s₂
theorem Stream'.Seq.mem_append_left {α : Type u} {s₁ : } {s₂ : } {a : α} (h : a s₁) :
a
@[simp]
theorem Stream'.Seq.enum_cons {α : Type u} (s : ) (x : α) :
= Stream'.Seq.cons (0, x) ()
def Stream'.Seq1.toSeq {α : Type u} :

Convert a Seq1 to a sequence.

Instances For
instance Stream'.Seq1.coeSeq {α : Type u} :
Coe () ()
def Stream'.Seq1.map {α : Type u} {β : Type v} (f : αβ) :

Map a function on a Seq1

Instances For
theorem Stream'.Seq1.map_pair {α : Type u} {β : Type v} {f : αβ} {a : α} {s : } :
Stream'.Seq1.map f (a, s) = (f a, )
theorem Stream'.Seq1.map_id {α : Type u} (s : ) :
= s
def Stream'.Seq1.join {α : Type u} :

Flatten a nonempty sequence of nonempty sequences

Instances For
@[simp]
theorem Stream'.Seq1.join_nil {α : Type u} (a : α) (S : ) :
Stream'.Seq1.join ((a, Stream'.Seq.nil), S) = (a, )
@[simp]
theorem Stream'.Seq1.join_cons {α : Type u} (a : α) (b : α) (s : ) (S : ) :
def Stream'.Seq1.ret {α : Type u} (a : α) :

The return operator for the Seq1 monad, which produces a singleton sequence.

Instances For
def Stream'.Seq1.bind {α : Type u} {β : Type v} (s : ) (f : α) :

The bind operator for the Seq1 monad, which maps f on each element of s and appends the results together. (Not all of s may be evaluated, because the first few elements of s may already produce an infinite result.)

Instances For
@[simp]
theorem Stream'.Seq1.join_map_ret {α : Type u} (s : ) :
Stream'.Seq.join (Stream'.Seq.map Stream'.Seq1.ret s) = s
@[simp]
theorem Stream'.Seq1.bind_ret {α : Type u} {β : Type v} (f : αβ) (s : ) :
Stream'.Seq1.bind s (Stream'.Seq1.ret f) =
@[simp]
theorem Stream'.Seq1.ret_bind {α : Type u} {β : Type v} (a : α) (f : α) :
= f a
@[simp]
theorem Stream'.Seq1.map_join' {α : Type u} {β : Type v} (f : αβ) (S : ) :
@[simp]
theorem Stream'.Seq1.map_join {α : Type u} {β : Type v} (f : αβ) (S : ) :
@[simp]
theorem Stream'.Seq1.join_join {α : Type u} (SS : ) :
= Stream'.Seq.join (Stream'.Seq.map Stream'.Seq1.join SS)
@[simp]
theorem Stream'.Seq1.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : ) (f : α) (g : β) :