# mathlibdocumentation

data.seq.seq

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

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

Equations
def seq  :
Type uType 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
def seq1  :
Type u_1Type u_1

seq1 α is the type of nonempty sequences.

Equations
def seq.nil {α : Type u} :
seq α

The empty sequence

Equations
@[instance]
def seq.inhabited {α : Type u} :

Equations
def seq.cons {α : Type u} :
α → seq αseq α

Prepend an element to a sequence

Equations
def seq.nth {α : Type u} :
seq α

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

Equations
def seq.terminated_at {α : Type u} :
seq α → Prop

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

Equations
@[instance]
def seq.terminated_at_decidable {α : Type u} (s : seq α) (n : ) :

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

Equations
def seq.terminates {α : Type u} :
seq α → Prop

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

Equations
@[simp]
def seq.omap {α : Type u} {β : Type v} {γ : Type w} :
(β → γ)option × β)option × γ)

Functorial action of the functor option (α × _)

Equations
def seq.head {α : Type u} :
seq α

Get the first element of a sequence

Equations
def seq.tail {α : Type u} :
seq αseq α

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

Equations
def seq.mem {α : Type u} :
α → seq α → Prop

Equations
@[instance]
def seq.has_mem {α : Type u} :
(seq α)

Equations
theorem seq.le_stable {α : Type u} (s : seq α) {m n : } :
m ns.nth m = nones.nth n = none

theorem seq.terminated_stable {α : Type u} (s : seq α) {m n : } :
m n

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

theorem seq.ge_stable {α : Type u} (s : seq α) {aₙ : α} {n m : } :
m ns.nth n = some aₙ(∃ (aₘ : α), s.nth m = some aₘ)

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 seq.not_mem_nil {α : Type u} (a : α) :

theorem seq.mem_cons {α : Type u} (a : α) (s : seq α) :
a s

theorem seq.mem_cons_of_mem {α : Type u} (y : α) {a : α} {s : seq α} :
a sa s

theorem seq.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : seq α} :
a sa = b a s

@[simp]
theorem seq.mem_cons_iff {α : Type u} {a b : α} {s : seq α} :
a s a = b a s

def seq.destruct {α : Type u} :
seq αoption (seq1 α)

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

Equations
theorem seq.destruct_eq_nil {α : Type u} {s : seq α} :

theorem seq.destruct_eq_cons {α : Type u} {s : seq α} {a : α} {s' : seq α} :
s.destruct = some (a, s')s = s'

@[simp]
theorem seq.destruct_nil {α : Type u} :

@[simp]
theorem seq.destruct_cons {α : Type u} (a : α) (s : seq α) :
(seq.cons a s).destruct = some (a, s)

theorem seq.head_eq_destruct {α : Type u} (s : seq α) :

@[simp]
theorem seq.head_nil {α : Type u} :

@[simp]
theorem seq.head_cons {α : Type u} (a : α) (s : seq α) :

@[simp]
theorem seq.tail_nil {α : Type u} :

@[simp]
theorem seq.tail_cons {α : Type u} (a : α) (s : seq α) :
(seq.cons a s).tail = s

def seq.cases_on {α : Type u} {C : seq αSort v} (s : seq α) :
(Π (x : α) (s : seq α), C (seq.cons x s))C s

Equations
theorem seq.mem_rec_on {α : Type u} {C : seq α → Prop} {a : α} {s : seq α} :
a s(∀ (b : α) (s' : seq α), a = b C s'C (seq.cons b s'))C s

def seq.corec.F {α : Type u} {β : Type v} :
(β → option × β)) ×

Equations
def seq.corec {α : Type u} {β : Type v} :
(β → option × β))β → seq α

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

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

def seq.of_list {α : Type u} :
list αseq α

Embed a list as a sequence

Equations
@[instance]
def seq.coe_list {α : Type u} :
has_coe (list α) (seq α)

Equations
@[simp]
def seq.bisim_o {α : Type u} :
(seq αseq α → Prop)option (seq1 α)option (seq1 α) → Prop

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

Equations
theorem seq.eq_of_bisim {α : Type u} (R : seq αseq α → Prop) (bisim : seq.is_bisimulation R) {s₁ s₂ : seq α} :
R s₁ s₂s₁ = s₂

theorem seq.coinduction {α : Type u} {s₁ s₂ : seq α} :
s₁.head = s₂.head(∀ (β : Type u) (fr : seq α → β), fr s₁ = fr s₂fr s₁.tail = fr s₂.tail)s₁ = s₂

theorem seq.coinduction2 {α : Type u} {β : Type v} (s : seq α) (f g : seq αseq β) :
(∀ (s : seq α), seq.bisim_o (λ (s1 s2 : seq β), ∃ (s : seq α), s1 = f s s2 = g s) (f s).destruct (g s).destruct)f s = g s

def seq.of_stream {α : Type u} :
seq α

Embed an infinite stream as a sequence

Equations
@[instance]
def seq.coe_stream {α : Type u} :
has_coe (stream α) (seq α)

Equations
def seq.of_lazy_list {α : Type u} :
seq α

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
@[instance]
def seq.coe_lazy_list {α : Type u} :

Equations
meta def seq.to_lazy_list {α : Type u} :
seq α

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 seq.force_to_list {α : Type u} :
seq αlist α

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

def seq.nats  :

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

Equations
@[simp]
theorem seq.nats_nth (n : ) :
= some n

def seq.append {α : Type u} :
seq αseq α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 seq.map {α : Type u} {β : Type v} :
(α → β)seq αseq β

Map a function over a sequence.

Equations
def seq.join {α : Type u} :
seq (seq1 α)seq α

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 seq.drop {α : Type u} :
seq αseq α

Remove the first n elements from the sequence.

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

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

Equations
def seq.split_at {α : Type u} :
seq αlist α × seq α

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

Equations
def seq.zip_with {α : Type u} {β : Type v} {γ : Type w} :
(α → β → γ)seq αseq βseq γ

Combine two sequences with a function

Equations
• f₁, a₁⟩ f₂, a₂⟩ = λ (n : ), seq.zip_with._match_1 f (f₁ n) (f₂ n), _⟩
• seq.zip_with._match_1 f (some a) (some b) = some (f a b)
• seq.zip_with._match_1 f (some val) none = none
• seq.zip_with._match_1 f none _x = none
theorem seq.zip_with_nth_some {α : Type u} {β : Type v} {γ : Type w} {s : seq α} {s' : seq β} {n : } {a : α} {b : β} (s_nth_eq_some : s.nth n = some a) (s_nth_eq_some' : s'.nth n = some b) (f : α → β → γ) :
s s').nth n = some (f a b)

theorem seq.zip_with_nth_none {α : Type u} {β : Type v} {γ : Type w} {s : seq α} {s' : seq β} {n : } (s_nth_eq_none : s.nth n = none) (f : α → β → γ) :
s s').nth n = none

theorem seq.zip_with_nth_none' {α : Type u} {β : Type v} {γ : Type w} {s : seq α} {s' : seq β} {n : } (s'_nth_eq_none : s'.nth n = none) (f : α → β → γ) :
s s').nth n = none

def seq.zip {α : Type u} {β : Type v} :
seq αseq βseq × β)

Pair two sequences into a sequence of pairs

Equations
def seq.unzip {α : Type u} {β : Type v} :
seq × β)seq α × seq β

Separate a sequence of pairs into two sequences

Equations
def seq.to_list {α : Type u} (s : seq α) :
(∃ (n : ), ¬((s.nth n).is_some))list α

Convert a sequence which is known to terminate into a list

Equations
def seq.to_stream {α : Type u} (s : seq α) :
(∀ (n : ), ((s.nth n).is_some))

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

Equations
def seq.to_list_or_stream {α : Type u} (s : seq α) [decidable (∃ (n : ), ¬((s.nth n).is_some))] :
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 seq.nil_append {α : Type u} (s : seq α) :
= s

@[simp]
theorem seq.cons_append {α : Type u} (a : α) (s t : seq α) :
(seq.cons a s).append t = (s.append t)

@[simp]
theorem seq.append_nil {α : Type u} (s : seq α) :
= s

@[simp]
theorem seq.append_assoc {α : Type u} (s t u : seq α) :
(s.append t).append u = s.append (t.append u)

@[simp]
theorem seq.map_nil {α : Type u} {β : Type v} (f : α → β) :

@[simp]
theorem seq.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : seq α) :
(seq.cons a s) = seq.cons (f a) (seq.map f s)

@[simp]
theorem seq.map_id {α : Type u} (s : seq α) :
= s

@[simp]
theorem seq.map_tail {α : Type u} {β : Type v} (f : α → β) (s : seq α) :
s.tail = (seq.map f s).tail

theorem seq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : seq α) :
seq.map (g f) s = (seq.map f s)

@[simp]
theorem seq.map_append {α : Type u} {β : Type v} (f : α → β) (s t : seq α) :
(s.append t) = (seq.map f s).append (seq.map f t)

@[simp]
theorem seq.map_nth {α : Type u} {β : Type v} (f : α → β) (s : seq α) (n : ) :
(seq.map f s).nth n = (s.nth n)

@[instance]

Equations
@[instance]

@[simp]
theorem seq.join_nil {α : Type u} :

@[simp]
theorem seq.join_cons_nil {α : Type u} (a : α) (S : seq (seq1 α)) :
(seq.cons (a, seq.nil α) S).join = S.join

@[simp]
theorem seq.join_cons_cons {α : Type u} (a b : α) (s : seq α) (S : seq (seq1 α)) :
(seq.cons (a, s) S).join = (seq.cons (b, s) S).join

@[simp]
theorem seq.join_cons {α : Type u} (a : α) (s : seq α) (S : seq (seq1 α)) :
(seq.cons (a, s) S).join = (s.append S.join)

@[simp]
theorem seq.join_append {α : Type u} (S T : seq (seq1 α)) :

@[simp]
theorem seq.of_list_nil {α : Type u} :

@[simp]
theorem seq.of_list_cons {α : Type u} (a : α) (l : list α) :

@[simp]
theorem seq.of_stream_cons {α : Type u} (a : α) (s : stream α) :

@[simp]
theorem seq.of_list_append {α : Type u} (l l' : list α) :

@[simp]
theorem seq.of_stream_append {α : Type u} (l : list α) (s : stream α) :

def seq.to_list' {α : Type u_1} :
seq αcomputation (list α)

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 seq.dropn_add {α : Type u} (s : seq α) (m n : ) :
s.drop (m + n) = (s.drop m).drop n

theorem seq.dropn_tail {α : Type u} (s : seq α) (n : ) :
s.tail.drop n = s.drop (n + 1)

theorem seq.nth_tail {α : Type u} (s : seq α) (n : ) :
s.tail.nth n = s.nth (n + 1)

@[ext]
theorem seq.ext {α : Type u} (s s' : seq α) :
(∀ (n : ), s.nth n = s'.nth n)s = s'

@[simp]
theorem seq.head_dropn {α : Type u} (s : seq α) (n : ) :

theorem seq.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : seq α} :
a sf a s

theorem seq.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : seq α} :
b s(∃ (a : α), a s f a = b)

theorem seq.of_mem_append {α : Type u} {s₁ s₂ : seq α} {a : α} :
a s₁.append s₂a s₁ a s₂

theorem seq.mem_append_left {α : Type u} {s₁ s₂ : seq α} {a : α} :
a s₁a s₁.append s₂

def seq1.to_seq {α : Type u} :
seq1 αseq α

Convert a seq1 to a sequence.

Equations
@[instance]
def seq1.coe_seq {α : Type u} :
has_coe (seq1 α) (seq α)

Equations
def seq1.map {α : Type u} {β : Type v} :
(α → β)seq1 αseq1 β

Map a function on a seq1

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

def seq1.join {α : Type u} :
seq1 (seq1 α)seq1 α

Flatten a nonempty sequence of nonempty sequences

Equations
@[simp]
theorem seq1.join_nil {α : Type u} (a : α) (S : seq (seq1 α)) :
seq1.join ((a, seq.nil α), S) = (a, S.join)

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

def seq1.ret {α : Type u} :
α → seq1 α

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

Equations
@[instance]
def seq1.inhabited {α : Type u} [inhabited α] :

Equations
def seq1.bind {α : Type u} {β : Type v} :
seq1 α(α → seq1 β)seq1 β

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 seq1.join_map_ret {α : Type u} (s : seq α) :
s).join = s

@[simp]
theorem seq1.bind_ret {α : Type u} {β : Type v} (f : α → β) (s : seq1 α) :
s.bind (seq1.ret f) = s

@[simp]
theorem seq1.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → seq1 β) :
(seq1.ret a).bind f = f a

@[simp]
theorem seq1.map_join' {α : Type u} {β : Type v} (f : α → β) (S : seq (seq1 α)) :

@[simp]
theorem seq1.map_join {α : Type u} {β : Type v} (f : α → β) (S : seq1 (seq1 α)) :

@[simp]
theorem seq1.join_join {α : Type u} (SS : seq (seq1 (seq1 α))) :
SS.join.join = SS).join

@[simp]
theorem seq1.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : seq1 α) (f : α → seq1 β) (g : β → seq1 γ) :
(s.bind f).bind g = s.bind (λ (x : α), (f x).bind g)

@[instance]