# mathlib3documentation

data.seq.seq

def stream.is_seq {α : Type u} (s : stream (option α)) :
Prop

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

Equations
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.

Equations
Instances for stream.seq
def stream.seq1 (α : Type u_1) :
Type u_1

seq1 α is the type of nonempty sequences.

Equations
Instances for stream.seq1
def stream.seq.nil {α : Type u} :

The empty sequence

Equations
@[protected, instance]
def stream.seq.inhabited {α : Type u} :
Equations
def stream.seq.cons {α : Type u} (a : α) (s : stream.seq α) :

Prepend an element to a sequence

Equations
@[simp]
theorem stream.seq.val_cons {α : Type u} (s : stream.seq α) (x : α) :
s).val = ::s.val
def stream.seq.nth {α : Type u} :

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

Equations
@[simp]
theorem stream.seq.nth_mk {α : Type u} (f : stream (option α)) (hf : f.is_seq) :
stream.seq.nth f, hf⟩ = f
@[simp]
theorem stream.seq.nth_nil {α : Type u} (n : ) :
@[simp]
theorem stream.seq.nth_cons_zero {α : Type u} (a : α) (s : stream.seq α) :
s).nth 0 =
@[simp]
theorem stream.seq.nth_cons_succ {α : Type u} (a : α) (s : stream.seq α) (n : ) :
s).nth (n + 1) = s.nth n
@[protected, ext]
theorem stream.seq.ext {α : Type u} {s t : stream.seq α} (h : (n : ), s.nth n = t.nth n) :
s = t
theorem stream.seq.cons_injective2 {α : Type u} :
theorem stream.seq.cons_left_injective {α : Type u} (s : stream.seq α) :
function.injective (λ (x : α), s)
theorem stream.seq.cons_right_injective {α : Type u} (x : α) :
def stream.seq.terminated_at {α : Type u} (s : stream.seq α) (n : ) :
Prop

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

Equations
Instances for stream.seq.terminated_at
@[protected, instance]

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

Equations
def stream.seq.terminates {α : Type u} (s : stream.seq α) :
Prop

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

Equations
theorem stream.seq.not_terminates_iff {α : Type u} {s : stream.seq α} :
@[simp]
def stream.seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : β γ) :
option × β) option × γ)

Functorial action of the functor option (α × _)

Equations
def stream.seq.head {α : Type u} (s : stream.seq α) :

Get the first element of a sequence

Equations
def stream.seq.tail {α : Type u} (s : stream.seq α) :

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

Equations
@[protected]
def stream.seq.mem {α : Type u} (a : α) (s : stream.seq α) :
Prop

member definition for seq

Equations
@[protected, instance]
def stream.seq.has_mem {α : Type u} :
Equations
theorem stream.seq.le_stable {α : Type u} (s : stream.seq α) {m n : } (h : m n) :
theorem stream.seq.terminated_stable {α : Type u} (s : stream.seq α) {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 : stream.seq α) {aₙ : α} {n m : } (m_le_n : m n) (s_nth_eq_some : s.nth n = ) :
(aₘ : α), s.nth m =

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

theorem stream.seq.not_mem_nil {α : Type u} (a : α) :
theorem stream.seq.mem_cons {α : Type u} (a : α) (s : stream.seq α) :
a
theorem stream.seq.mem_cons_of_mem {α : Type u} (y : α) {a : α} {s : stream.seq α} :
a s a
theorem stream.seq.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : stream.seq α} :
a a = b a s
@[simp]
theorem stream.seq.mem_cons_iff {α : Type u} {a b : α} {s : stream.seq α} :
a a = b a s
def stream.seq.destruct {α : Type u} (s : stream.seq α) :

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

Equations
theorem stream.seq.destruct_eq_nil {α : Type u} {s : stream.seq α} :
theorem stream.seq.destruct_eq_cons {α : Type u} {s : stream.seq α} {a : α} {s' : stream.seq α} :
s.destruct = option.some (a, s') s = s'
@[simp]
theorem stream.seq.destruct_nil {α : Type u} :
@[simp]
theorem stream.seq.destruct_cons {α : Type u} (a : α) (s : stream.seq α) :
theorem stream.seq.head_eq_destruct {α : Type u} (s : stream.seq α) :
@[simp]
theorem stream.seq.head_nil {α : Type u} :
@[simp]
theorem stream.seq.head_cons {α : Type u} (a : α) (s : stream.seq α) :
@[simp]
theorem stream.seq.tail_nil {α : Type u} :
@[simp]
theorem stream.seq.tail_cons {α : Type u} (a : α) (s : stream.seq α) :
s).tail = s
@[simp]
theorem stream.seq.nth_tail {α : Type u} (s : stream.seq α) (n : ) :
s.tail.nth n = s.nth (n + 1)
def stream.seq.rec_on {α : Type u} {C : Sort v} (s : stream.seq α) (h1 : C stream.seq.nil) (h2 : Π (x : α) (s : , C s)) :
C s

Recursion principle for sequences, compare with list.rec_on.

Equations
theorem stream.seq.mem_rec_on {α : Type u} {C : Prop} {a : α} {s : stream.seq α} (M : a s) (h1 : (b : α) (s' : , a = b C s' C s')) :
C s
def stream.seq.corec.F {α : Type u} {β : Type v} (f : β option × β)) :

Corecursor over pairs of option values

Equations
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.

Equations
@[simp]
theorem stream.seq.corec_eq {α : Type u} {β : Type v} (f : β option × β)) (b : β) :
b).destruct = (f b)
@[simp]
def stream.seq.bisim_o {α : Type u} (R : Prop) :
Prop

Bisimilarity relation over option of seq1 α

Equations
def stream.seq.is_bisimulation {α : Type u} (R : Prop) :
Prop

a relation is bisimiar if it meets the bisim_o test

Equations
theorem stream.seq.eq_of_bisim {α : Type u} (R : Prop) (bisim : stream.seq.is_bisimulation R) {s₁ s₂ : stream.seq α} (r : R s₁ s₂) :
s₁ = s₂
theorem stream.seq.coinduction {α : Type u} {s₁ s₂ : stream.seq α} :
s₁.head = s₂.head ( (β : Type u) (fr : β), fr s₁ = fr s₂ fr s₁.tail = fr s₂.tail) s₁ = s₂
theorem stream.seq.coinduction2 {α : Type u} {β : Type v} (s : stream.seq α) (f g : ) (H : (s : , stream.seq.bisim_o (λ (s1 s2 : , (s : , s1 = f s s2 = g s) (f s).destruct (g s).destruct) :
f s = g s
def stream.seq.of_list {α : Type u} (l : list α) :

Embed a list as a sequence

Equations
@[protected, instance]
def stream.seq.coe_list {α : Type u} :
Equations
@[simp]
theorem stream.seq.of_list_nil {α : Type u} :
@[simp]
theorem stream.seq.of_list_nth {α : Type u} (l : list α) (n : ) :
n = l.nth n
@[simp]
theorem stream.seq.of_list_cons {α : Type u} (a : α) (l : list α) :
def stream.seq.of_stream {α : Type u} (s : stream α) :

Embed an infinite stream as a sequence

Equations
@[protected, instance]
def stream.seq.coe_stream {α : Type u} :
Equations
def stream.seq.of_lazy_list {α : Type u} :

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

Equations
@[protected, instance]
Equations
meta def stream.seq.to_lazy_list {α : Type u} :

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

meta def stream.seq.force_to_list {α : Type u} (s : stream.seq α) :
list α

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

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

Equations
@[simp]
theorem stream.seq.nats_nth (n : ) :
def stream.seq.append {α : Type u} (s₁ s₂ : stream.seq α) :

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

Equations
def stream.seq.map {α : Type u} {β : Type v} (f : α β) :

Map a function over a sequence.

Equations
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.)

Equations
@[simp]
def stream.seq.drop {α : Type u} (s : stream.seq α) :

Remove the first n elements from the sequence.

Equations
def stream.seq.take {α : Type u} :

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

Equations
def stream.seq.split_at {α : Type u} :

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

Equations
def stream.seq.zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) (s₁ : stream.seq α) (s₂ : stream.seq β) :

Combine two sequences with a function

Equations
@[simp]
theorem stream.seq.nth_zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) (s : stream.seq α) (s' : stream.seq β) (n : ) :
s').nth n = (s.nth n) (s'.nth n)
def stream.seq.zip {α : Type u} {β : Type v} :
stream.seq × β)

Pair two sequences into a sequence of pairs

Equations
theorem stream.seq.nth_zip {α : Type u} {β : Type v} (s : stream.seq α) (t : stream.seq β) (n : ) :
(s.zip t).nth n = (s.nth n) (t.nth n)
def stream.seq.unzip {α : Type u} {β : Type v} (s : stream.seq × β)) :

Separate a sequence of pairs into two sequences

Equations
def stream.seq.enum {α : Type u} (s : stream.seq α) :

Enumerate a sequence by tagging each element with its index.

Equations
@[simp]
theorem stream.seq.nth_enum {α : Type u} (s : stream.seq α) (n : ) :
s.enum.nth n = (s.nth n)
@[simp]
theorem stream.seq.enum_nil {α : Type u} :
def stream.seq.to_list {α : Type u} (s : stream.seq α) (h : s.terminates) :
list α

Convert a sequence which is known to terminate into a list

Equations
def stream.seq.to_stream {α : Type u} (s : stream.seq α) (h : ¬s.terminates) :

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

Equations
def stream.seq.to_list_or_stream {α : Type u} (s : stream.seq α)  :
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.)

Equations
@[simp]
theorem stream.seq.nil_append {α : Type u} (s : stream.seq α) :
@[simp]
theorem stream.seq.cons_append {α : Type u} (a : α) (s t : stream.seq α) :
s).append t = (s.append t)
@[simp]
theorem stream.seq.append_nil {α : Type u} (s : stream.seq α) :
@[simp]
theorem stream.seq.append_assoc {α : Type u} (s t u : stream.seq α) :
(s.append t).append u = s.append (t.append u)
@[simp]
theorem stream.seq.map_nil {α : Type u} {β : Type v} (f : α β) :
@[simp]
theorem stream.seq.map_cons {α : Type u} {β : Type v} (f : α β) (a : α) (s : stream.seq α) :
s) = stream.seq.cons (f a) s)
@[simp]
theorem stream.seq.map_id {α : Type u} (s : stream.seq α) :
@[simp]
theorem stream.seq.map_tail {α : Type u} {β : Type v} (f : α β) (s : stream.seq α) :
= s).tail
theorem stream.seq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : α β) (g : β γ) (s : stream.seq α) :
stream.seq.map (g f) s = s)
@[simp]
theorem stream.seq.map_append {α : Type u} {β : Type v} (f : α β) (s t : stream.seq α) :
(s.append t) = s).append t)
@[simp]
theorem stream.seq.map_nth {α : Type u} {β : Type v} (f : α β) (s : stream.seq α) (n : ) :
s).nth n = (s.nth n)
@[protected, instance]
Equations
@[protected, instance]
@[simp]
theorem stream.seq.join_nil {α : Type u} :
@[simp]
theorem stream.seq.join_cons_nil {α : Type u} (a : α) (S : stream.seq (stream.seq1 α)) :
@[simp]
theorem stream.seq.join_cons_cons {α : Type u} (a b : α) (s : stream.seq α) (S : stream.seq (stream.seq1 α)) :
(stream.seq.cons (a, s) S).join = (stream.seq.cons (b, s) S).join
@[simp]
theorem stream.seq.join_cons {α : Type u} (a : α) (s : stream.seq α) (S : stream.seq (stream.seq1 α)) :
(stream.seq.cons (a, s) S).join = (s.append S.join)
@[simp]
theorem stream.seq.join_append {α : Type u} (S T : stream.seq (stream.seq1 α)) :
@[simp]
theorem stream.seq.of_stream_cons {α : Type u} (a : α) (s : stream α) :
@[simp]
theorem stream.seq.of_list_append {α : Type u} (l l' : list α) :
@[simp]
theorem stream.seq.of_stream_append {α : Type u} (l : list α) (s : stream α) :
def stream.seq.to_list' {α : Type u_1} (s : stream.seq α) :

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).

Equations
theorem stream.seq.dropn_add {α : Type u} (s : stream.seq α) (m n : ) :
s.drop (m + n) = (s.drop m).drop n
theorem stream.seq.dropn_tail {α : Type u} (s : stream.seq α) (n : ) :
s.tail.drop n = s.drop (n + 1)
@[simp]
theorem stream.seq.head_dropn {α : Type u} (s : stream.seq α) (n : ) :
theorem stream.seq.mem_map {α : Type u} {β : Type v} (f : α β) {a : α} {s : stream.seq α} :
a s f a
theorem stream.seq.exists_of_mem_map {α : Type u} {β : Type v} {f : α β} {b : β} {s : stream.seq α} :
b ( (a : α), a s f a = b)
theorem stream.seq.of_mem_append {α : Type u} {s₁ s₂ : stream.seq α} {a : α} (h : a s₁.append s₂) :
a s₁ a s₂
theorem stream.seq.mem_append_left {α : Type u} {s₁ s₂ : stream.seq α} {a : α} (h : a s₁) :
a s₁.append s₂
@[simp]
theorem stream.seq.enum_cons {α : Type u} (s : stream.seq α) (x : α) :
s).enum = stream.seq.cons (0, x) s.enum)
def stream.seq1.to_seq {α : Type u} :

Convert a seq1 to a sequence.

Equations
@[protected, instance]
def stream.seq1.coe_seq {α : Type u} :
Equations
def stream.seq1.map {α : Type u} {β : Type v} (f : α β) :

Map a function on a seq1

Equations
• (a, s) = (f a, s)
theorem stream.seq1.map_id {α : Type u} (s : stream.seq1 α) :
def stream.seq1.join {α : Type u} :

Flatten a nonempty sequence of nonempty sequences

Equations
@[simp]
theorem stream.seq1.join_nil {α : Type u} (a : α) (S : stream.seq (stream.seq1 α)) :
stream.seq1.join ((a, , S) = (a, S.join)
@[simp]
theorem stream.seq1.join_cons {α : Type u} (a b : α) (s : stream.seq α) (S : stream.seq (stream.seq1 α)) :
stream.seq1.join ((a, s), S) = (a, (stream.seq.cons (b, s) S).join)
def stream.seq1.ret {α : Type u} (a : α) :

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

Equations
• = (a,
@[protected, instance]
def stream.seq1.inhabited {α : Type u} [inhabited α] :
Equations
def stream.seq1.bind {α : Type u} {β : Type v} (s : stream.seq1 α) (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.)

Equations
@[simp]
theorem stream.seq1.join_map_ret {α : Type u} (s : stream.seq α) :
@[simp]
theorem stream.seq1.bind_ret {α : Type u} {β : Type v} (f : α β) (s : stream.seq1 α) :
s.bind =
@[simp]
theorem stream.seq1.ret_bind {α : Type u} {β : Type v} (a : α) (f : α ) :
.bind f = f a
@[simp]
theorem stream.seq1.map_join' {α : Type u} {β : Type v} (f : α β) (S : stream.seq (stream.seq1 α)) :
= S).join
@[simp]
theorem stream.seq1.map_join {α : Type u} {β : Type v} (f : α β) (S : stream.seq1 (stream.seq1 α)) :
= S).join
@[simp]
theorem stream.seq1.join_join {α : Type u} (SS : stream.seq (stream.seq1 (stream.seq1 α))) :
SS.join.join =
@[simp]
theorem stream.seq1.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : stream.seq1 α) (f : α ) (g : β ) :
(s.bind f).bind g = s.bind (λ (x : α), (f x).bind g)
@[protected, instance]
Equations
@[protected, instance]