data.seq.seq - mathlib3 docs

source

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

s.is_seq = ∀ {n : ℕ}, s n = option.none → s (n + 1) = option.none

source

def stream.seq (α : Type u) :

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

stream.seq α = {f // f.is_seq}

Instances for stream.seq

source

def stream.seq1 (α : Type u_1) :

Type u_1

seq1 α is the type of nonempty sequences.

Equations

stream.seq1 α = (α × stream.seq α)

Instances for stream.seq1

source

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

stream.seq α

The empty sequence

Equations

stream.seq.nil = ⟨stream.const option.none, _⟩

source

@[protected, instance]

def stream.seq.inhabited {α : Type u} :

inhabited (stream.seq α)

Equations

stream.seq.inhabited = {default := stream.seq.nil α}

source

def stream.seq.cons {α : Type u} (a : α) (s : stream.seq α) :

stream.seq α

Prepend an element to a sequence

Equations

stream.seq.cons a s = ⟨option.some a::s.val, _⟩

source

@[simp]

theorem stream.seq.val_cons {α : Type u} (s : stream.seq α) (x : α) :

(stream.seq.cons x s).val = option.some x::s.val

source

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

stream.seq α → ℕ → option α

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

Equations

stream.seq.nth = subtype.val

source

@[simp]

theorem stream.seq.nth_mk {α : Type u} (f : stream (option α)) (hf : f.is_seq) :

stream.seq.nth ⟨f, hf⟩ = f

source

@[simp]

theorem stream.seq.nth_nil {α : Type u} (n : ℕ) :

stream.seq.nil.nth n = option.none

source

@[simp]

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

(stream.seq.cons a s).nth 0 = option.some a

source

@[simp]

theorem stream.seq.nth_cons_succ {α : Type u} (a : α) (s : stream.seq α) (n : ℕ) :

(stream.seq.cons a s).nth (n + 1) = s.nth n

source

@[protected, ext]

theorem stream.seq.ext {α : Type u} {s t : stream.seq α} (h : ∀ (n : ℕ), s.nth n = t.nth n) :

s = t

source

theorem stream.seq.cons_injective2 {α : Type u} :

function.injective2 stream.seq.cons

source

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

function.injective (λ (x : α), stream.seq.cons x s)

source

theorem stream.seq.cons_right_injective {α : Type u} (x : α) :

function.injective (stream.seq.cons x)

source

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

s.terminated_at n = (s.nth n = option.none)

Instances for stream.seq.terminated_at

stream.seq.terminated_at_decidable

source

@[protected, instance]

def stream.seq.terminated_at_decidable {α : Type u} (s : stream.seq α) (n : ℕ) :

decidable (s.terminated_at n)

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

Equations

s.terminated_at_decidable n = decidable_of_iff' ↥((s.nth n).is_none) _

source

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

s.terminates = ∃ (n : ℕ), s.terminated_at n

source

theorem stream.seq.not_terminates_iff {α : Type u} {s : stream.seq α} :

¬s.terminates ↔ ∀ (n : ℕ), ↥((s.nth n).is_some)

source

@[simp]

def stream.seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) :

option (α × β) → option (α × γ)

Functorial action of the functor option (α × _)

Equations

stream.seq.omap f (option.some (a, b)) = option.some (a, f b)
stream.seq.omap f option.none = option.none

source

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

option α

Get the first element of a sequence

Equations

s.head = s.nth 0

source

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

stream.seq α

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

Equations

s.tail = ⟨s.val.tail, _⟩

source

@[protected]

def stream.seq.mem {α : Type u} (a : α) (s : stream.seq α) :

Prop

member definition for seq

Equations

stream.seq.mem a s = (option.some a ∈ s.val)

source

@[protected, instance]

def stream.seq.has_mem {α : Type u} :

has_mem α (stream.seq α)

Equations

stream.seq.has_mem = {mem := stream.seq.mem α}

source

theorem stream.seq.le_stable {α : Type u} (s : stream.seq α) {m n : ℕ} (h : m ≤ n) :

s.nth m = option.none → s.nth n = option.none

source

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

m ≤ n → s.terminated_at m → s.terminated_at n

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

source

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 = option.some aₙ) :

∃ (aₘ : α), s.nth m = option.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.

source

theorem stream.seq.not_mem_nil {α : Type u} (a : α) :

a ∉ stream.seq.nil

source

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

a ∈ stream.seq.cons a s

source

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

a ∈ s → a ∈ stream.seq.cons y s

source

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

a ∈ stream.seq.cons b s → a = b ∨ a ∈ s

source

@[simp]

theorem stream.seq.mem_cons_iff {α : Type u} {a b : α} {s : stream.seq α} :

a ∈ stream.seq.cons b s ↔ a = b ∨ a ∈ s

source

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

option (stream.seq1 α)

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

Equations

s.destruct = (λ (a' : α), (a', s.tail)) <$> s.nth 0

source

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

s.destruct = option.none → s = stream.seq.nil

source

theorem stream.seq.destruct_eq_cons {α : Type u} {s : stream.seq α} {a : α} {s' : stream.seq α} :

s.destruct = option.some (a, s') → s = stream.seq.cons a s'

source

@[simp]

theorem stream.seq.destruct_nil {α : Type u} :

stream.seq.nil.destruct = option.none

source

@[simp]

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

(stream.seq.cons a s).destruct = option.some (a, s)

source

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

s.head = prod.fst <$> s.destruct

source

@[simp]

theorem stream.seq.head_nil {α : Type u} :

stream.seq.nil.head = option.none

source

@[simp]

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

(stream.seq.cons a s).head = option.some a

source

@[simp]

theorem stream.seq.tail_nil {α : Type u} :

stream.seq.nil.tail = stream.seq.nil

source

@[simp]

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

(stream.seq.cons a s).tail = s

source

@[simp]

theorem stream.seq.nth_tail {α : Type u} (s : stream.seq α) (n : ℕ) :

s.tail.nth n = s.nth (n + 1)

source

def stream.seq.rec_on {α : Type u} {C : stream.seq α → Sort v} (s : stream.seq α) (h1 : C stream.seq.nil) (h2 : Π (x : α) (s : stream.seq α), C (stream.seq.cons x s)) :

C s

Recursion principle for sequences, compare with list.rec_on.

Equations

s.rec_on h1 h2 = (λ (_x : option (stream.seq1 α)) (H : s.destruct = _x), option.rec (λ (H : s.destruct = option.none), _.mpr h1) (λ (v : stream.seq1 α) (H : s.destruct = option.some v), prod.cases_on v (λ (a : α) (s' : stream.seq α) (H : s.destruct = option.some (a, s')), _.mpr (h2 a s')) H) _x H) s.destruct _

source

theorem stream.seq.mem_rec_on {α : Type u} {C : stream.seq α → Prop} {a : α} {s : stream.seq α} (M : a ∈ s) (h1 : ∀ (b : α) (s' : stream.seq α), a = b ∨ C s' → C (stream.seq.cons b s')) :

C s

source

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

option β → option α × option β

Corecursor over pairs of option values

Equations

stream.seq.corec.F f (option.some b) = stream.seq.corec.F._match_1 (f b)
stream.seq.corec.F f option.none = (option.none α, option.none β)
stream.seq.corec.F._match_1 (option.some (a, b')) = (option.some a, option.some b')
stream.seq.corec.F._match_1 option.none = (option.none α, option.none β)

source

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

stream.seq α

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

Equations

stream.seq.corec f b = ⟨stream.corec' (stream.seq.corec.F f) (option.some b), _⟩

source

@[simp]

theorem stream.seq.corec_eq {α : Type u} {β : Type v} (f : β → option (α × β)) (b : β) :

(stream.seq.corec f b).destruct = stream.seq.omap (stream.seq.corec f) (f b)

source

@[simp]

def stream.seq.bisim_o {α : Type u} (R : stream.seq α → stream.seq α → Prop) :

option (stream.seq1 α) → option (stream.seq1 α) → Prop

Bisimilarity relation over option of seq1 α

Equations

stream.seq.bisim_o R (option.some (a, s)) (option.some (a', s')) = (a = a' ∧ R s s')
stream.seq.bisim_o R (option.some (fst, snd)) option.none = false
stream.seq.bisim_o R option.none (option.some val) = false
stream.seq.bisim_o R option.none option.none = true

source

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

Prop

a relation is bisimiar if it meets the bisim_o test

Equations

stream.seq.is_bisimulation R = ∀ ⦃s₁ s₂ : stream.seq α⦄, R s₁ s₂ → stream.seq.bisim_o R s₁.destruct s₂.destruct

source

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

s₁ = s₂

source

theorem stream.seq.coinduction {α : Type u} {s₁ s₂ : stream.seq α} :

s₁.head = s₂.head → (∀ (β : Type u) (fr : stream.seq α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂

source

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

f s = g s

source

def stream.seq.of_list {α : Type u} (l : list α) :

stream.seq α

Embed a list as a sequence

Equations

stream.seq.of_list l = ⟨l.nth, _⟩

source

@[protected, instance]

def stream.seq.coe_list {α : Type u} :

has_coe (list α) (stream.seq α)

Equations

stream.seq.coe_list = {coe := stream.seq.of_list α}

source

@[simp]

theorem stream.seq.of_list_nil {α : Type u} :

stream.seq.of_list list.nil = stream.seq.nil

source

@[simp]

theorem stream.seq.of_list_nth {α : Type u} (l : list α) (n : ℕ) :

(stream.seq.of_list l).nth n = l.nth n

source

@[simp]

theorem stream.seq.of_list_cons {α : Type u} (a : α) (l : list α) :

stream.seq.of_list (a :: l) = stream.seq.cons a (stream.seq.of_list l)

source

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

stream.seq α

Embed an infinite stream as a sequence

Equations

stream.seq.of_stream s = ⟨stream.map option.some s, _⟩

source

@[protected, instance]

def stream.seq.coe_stream {α : Type u} :

has_coe (stream α) (stream.seq α)

Equations

stream.seq.coe_stream = {coe := stream.seq.of_stream α}

source

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

lazy_list α → stream.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

stream.seq.of_lazy_list = stream.seq.corec (λ (l : lazy_list α), stream.seq.of_lazy_list._match_1 l)
stream.seq.of_lazy_list._match_1 (lazy_list.cons a l') = option.some (a, l' unit.star())
stream.seq.of_lazy_list._match_1 lazy_list.nil = option.none

source

@[protected, instance]

def stream.seq.coe_lazy_list {α : Type u} :

has_coe (lazy_list α) (stream.seq α)

Equations

stream.seq.coe_lazy_list = {coe := stream.seq.of_lazy_list α}

source

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

stream.seq α → lazy_list α

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

source

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.

source

def stream.seq.nats :

stream.seq ℕ

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

Equations

stream.seq.nats = ↑stream.nats

source

@[simp]

theorem stream.seq.nats_nth (n : ℕ) :

stream.seq.nats.nth n = option.some n

source

def stream.seq.append {α : Type u} (s₁ s₂ : stream.seq α) :

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

s₁.append s₂ = stream.seq.corec (λ (_x : stream.seq α × stream.seq α), stream.seq.append._match_2 _x) (s₁, s₂)
stream.seq.append._match_2 (s₁, s₂) = stream.seq.append._match_1 s₂ s₁.destruct
stream.seq.append._match_1 s₂ (option.some (a, s₁')) = option.some (a, s₁', s₂)
stream.seq.append._match_1 s₂ option.none = stream.seq.omap (λ (s₂ : stream.seq α), (stream.seq.nil α, s₂)) s₂.destruct

source

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

stream.seq α → stream.seq β

Map a function over a sequence.

Equations

stream.seq.map f ⟨s, al⟩ = ⟨stream.map (option.map f) s, _⟩

source

def stream.seq.join {α : Type u} :

stream.seq (stream.seq1 α) → stream.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

stream.seq.join = stream.seq.corec (λ (S : stream.seq (stream.seq1 α)), stream.seq.join._match_1 S.destruct)
stream.seq.join._match_1 (option.some ((a, s), S')) = option.some (a, stream.seq.join._match_2 S' s.destruct)
stream.seq.join._match_1 option.none = option.none
stream.seq.join._match_2 S' (option.some s') = stream.seq.cons s' S'
stream.seq.join._match_2 S' option.none = S'

source

@[simp]

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

ℕ → stream.seq α

Remove the first n elements from the sequence.

Equations

s.drop (n + 1) = (s.drop n).tail
s.drop 0 = s

source

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

ℕ → stream.seq α → list α

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

Equations

stream.seq.take (n + 1) s = stream.seq.take._match_1 (λ (r : stream.seq α), stream.seq.take n r) s.destruct
stream.seq.take 0 s = list.nil
stream.seq.take._match_1 _f_1 (option.some (x, r)) = x :: _f_1 r
stream.seq.take._match_1 _f_1 option.none = list.nil

source

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

ℕ → stream.seq α → list α × stream.seq α

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

Equations

stream.seq.split_at (n + 1) s = stream.seq.split_at._match_1 (λ (s' : stream.seq α), stream.seq.split_at n s') s.destruct
stream.seq.split_at 0 s = (list.nil α, s)
stream.seq.split_at._match_1 _f_1 (option.some (x, s')) = stream.seq.split_at._match_2 x (_f_1 s')
stream.seq.split_at._match_1 _f_1 option.none = (list.nil α, stream.seq.nil α)
stream.seq.split_at._match_2 x (l, r) = (x :: l, r)

source

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

stream.seq γ

Combine two sequences with a function

Equations

stream.seq.zip_with f s₁ s₂ = ⟨λ (n : ℕ), option.map₂ f (s₁.nth n) (s₂.nth n), _⟩

source

@[simp]

theorem stream.seq.nth_zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s : stream.seq α) (s' : stream.seq β) (n : ℕ) :

(stream.seq.zip_with f s s').nth n = option.map₂ f (s.nth n) (s'.nth n)

source

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

stream.seq α → stream.seq β → stream.seq (α × β)

Pair two sequences into a sequence of pairs

Equations

stream.seq.zip = stream.seq.zip_with prod.mk

source

theorem stream.seq.nth_zip {α : Type u} {β : Type v} (s : stream.seq α) (t : stream.seq β) (n : ℕ) :

(s.zip t).nth n = option.map₂ prod.mk (s.nth n) (t.nth n)

source

def stream.seq.unzip {α : Type u} {β : Type v} (s : stream.seq (α × β)) :

stream.seq α × stream.seq β

Separate a sequence of pairs into two sequences

Equations

s.unzip = (stream.seq.map prod.fst s, stream.seq.map prod.snd s)

source

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

stream.seq (ℕ × α)

Enumerate a sequence by tagging each element with its index.

Equations

s.enum = stream.seq.nats.zip s

source

@[simp]

theorem stream.seq.nth_enum {α : Type u} (s : stream.seq α) (n : ℕ) :

s.enum.nth n = option.map (prod.mk n) (s.nth n)

source

@[simp]

theorem stream.seq.enum_nil {α : Type u} :

stream.seq.nil.enum = stream.seq.nil

source

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

s.to_list h = stream.seq.take (nat.find h) s

source

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

stream α

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

Equations

s.to_stream h = λ (n : ℕ), option.get _

source

def stream.seq.to_list_or_stream {α : Type u} (s : stream.seq α) [decidable s.terminates] :

list α ⊕ stream α

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

s.to_list_or_stream = dite s.terminates (λ (h : s.terminates), sum.inl (s.to_list h)) (λ (h : ¬s.terminates), sum.inr (s.to_stream h))

source

@[simp]

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

stream.seq.nil.append s = s

source

@[simp]

theorem stream.seq.cons_append {α : Type u} (a : α) (s t : stream.seq α) :

(stream.seq.cons a s).append t = stream.seq.cons a (s.append t)

source

@[simp]

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

s.append stream.seq.nil = s

source

@[simp]

theorem stream.seq.append_assoc {α : Type u} (s t u : stream.seq α) :

(s.append t).append u = s.append (t.append u)

source

@[simp]

theorem stream.seq.map_nil {α : Type u} {β : Type v} (f : α → β) :

stream.seq.map f stream.seq.nil = stream.seq.nil

source

@[simp]

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

stream.seq.map f (stream.seq.cons a s) = stream.seq.cons (f a) (stream.seq.map f s)

source

@[simp]

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

stream.seq.map id s = s

source

@[simp]

theorem stream.seq.map_tail {α : Type u} {β : Type v} (f : α → β) (s : stream.seq α) :

stream.seq.map f s.tail = (stream.seq.map f s).tail

source

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

stream.seq.map (g ∘ f) s = stream.seq.map g (stream.seq.map f s)

source

@[simp]

theorem stream.seq.map_append {α : Type u} {β : Type v} (f : α → β) (s t : stream.seq α) :

stream.seq.map f (s.append t) = (stream.seq.map f s).append (stream.seq.map f t)

source

@[simp]

theorem stream.seq.map_nth {α : Type u} {β : Type v} (f : α → β) (s : stream.seq α) (n : ℕ) :

(stream.seq.map f s).nth n = option.map f (s.nth n)

source

@[protected, instance]

def stream.seq.functor :

functor stream.seq

Equations

stream.seq.functor = {map := stream.seq.map, map_const := λ (α β : Type u_1), stream.seq.map ∘ function.const β}

source

@[protected, instance]

def stream.seq.is_lawful_functor :

is_lawful_functor stream.seq

source

@[simp]

theorem stream.seq.join_nil {α : Type u} :

stream.seq.nil.join = stream.seq.nil

source

@[simp]

theorem stream.seq.join_cons_nil {α : Type u} (a : α) (S : stream.seq (stream.seq1 α)) :

(stream.seq.cons (a, stream.seq.nil α) S).join = stream.seq.cons a S.join

source

@[simp]

theorem stream.seq.join_cons_cons {α : Type u} (a b : α) (s : stream.seq α) (S : stream.seq (stream.seq1 α)) :

(stream.seq.cons (a, stream.seq.cons b s) S).join = stream.seq.cons a (stream.seq.cons (b, s) S).join

source

@[simp]

theorem stream.seq.join_cons {α : Type u} (a : α) (s : stream.seq α) (S : stream.seq (stream.seq1 α)) :

(stream.seq.cons (a, s) S).join = stream.seq.cons a (s.append S.join)

source

@[simp]

theorem stream.seq.join_append {α : Type u} (S T : stream.seq (stream.seq1 α)) :

(S.append T).join = S.join.append T.join

source

@[simp]

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

stream.seq.of_stream (a::s) = stream.seq.cons a (stream.seq.of_stream s)

source

@[simp]

theorem stream.seq.of_list_append {α : Type u} (l l' : list α) :

stream.seq.of_list (l ++ l') = (stream.seq.of_list l).append (stream.seq.of_list l')

source

@[simp]

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

stream.seq.of_stream (l ++ₛ s) = (stream.seq.of_list l).append (stream.seq.of_stream s)

source

def stream.seq.to_list' {α : Type u_1} (s : stream.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

s.to_list' = computation.corec (λ (_x : list α × stream.seq α), stream.seq.to_list'._match_2 _x) (list.nil α, s)
stream.seq.to_list'._match_2 (l, s) = stream.seq.to_list'._match_1 l s.destruct
stream.seq.to_list'._match_1 l (option.some (a, s')) = sum.inr (a :: l, s')
stream.seq.to_list'._match_1 l option.none = sum.inl l.reverse

source

theorem stream.seq.dropn_add {α : Type u} (s : stream.seq α) (m n : ℕ) :

s.drop (m + n) = (s.drop m).drop n

source

theorem stream.seq.dropn_tail {α : Type u} (s : stream.seq α) (n : ℕ) :

s.tail.drop n = s.drop (n + 1)

source

@[simp]

theorem stream.seq.head_dropn {α : Type u} (s : stream.seq α) (n : ℕ) :

(s.drop n).head = s.nth n

source

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

a ∈ s → f a ∈ stream.seq.map f s

source

theorem stream.seq.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : stream.seq α} :

b ∈ stream.seq.map f s → (∃ (a : α), a ∈ s ∧ f a = b)

source

theorem stream.seq.of_mem_append {α : Type u} {s₁ s₂ : stream.seq α} {a : α} (h : a ∈ s₁.append s₂) :

a ∈ s₁ ∨ a ∈ s₂

source

theorem stream.seq.mem_append_left {α : Type u} {s₁ s₂ : stream.seq α} {a : α} (h : a ∈ s₁) :

a ∈ s₁.append s₂

source

@[simp]

theorem stream.seq.enum_cons {α : Type u} (s : stream.seq α) (x : α) :

(stream.seq.cons x s).enum = stream.seq.cons (0, x) (stream.seq.map (prod.map nat.succ id) s.enum)

source

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

stream.seq1 α → stream.seq α

Convert a seq1 to a sequence.

Equations

stream.seq1.to_seq (a, s) = stream.seq.cons a s

source

@[protected, instance]

def stream.seq1.coe_seq {α : Type u} :

has_coe (stream.seq1 α) (stream.seq α)

Equations

stream.seq1.coe_seq = {coe := stream.seq1.to_seq α}

source

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

stream.seq1 α → stream.seq1 β

Map a function on a seq1

Equations

stream.seq1.map f (a, s) = (f a, stream.seq.map f s)

source

theorem stream.seq1.map_id {α : Type u} (s : stream.seq1 α) :

stream.seq1.map id s = s

source

def stream.seq1.join {α : Type u} :

stream.seq1 (stream.seq1 α) → stream.seq1 α

Flatten a nonempty sequence of nonempty sequences

Equations

stream.seq1.join ((a, s), S) = stream.seq1.join._match_3 a S s.destruct
stream.seq1.join._match_3 a S (option.some s') = (a, (stream.seq.cons s' S).join)
stream.seq1.join._match_3 a S option.none = (a, S.join)

source

@[simp]

theorem stream.seq1.join_nil {α : Type u} (a : α) (S : stream.seq (stream.seq1 α)) :

stream.seq1.join ((a, stream.seq.nil α), S) = (a, S.join)

source

@[simp]

theorem stream.seq1.join_cons {α : Type u} (a b : α) (s : stream.seq α) (S : stream.seq (stream.seq1 α)) :

stream.seq1.join ((a, stream.seq.cons b s), S) = (a, (stream.seq.cons (b, s) S).join)

source

def stream.seq1.ret {α : Type u} (a : α) :

stream.seq1 α

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

Equations

stream.seq1.ret a = (a, stream.seq.nil α)

source

@[protected, instance]

def stream.seq1.inhabited {α : Type u} [inhabited α] :

inhabited (stream.seq1 α)

Equations

stream.seq1.inhabited = {default := stream.seq1.ret inhabited.default}

source

def stream.seq1.bind {α : Type u} {β : Type v} (s : stream.seq1 α) (f : α → stream.seq1 β) :

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