Basic properties of sequences (possibly infinite lists)

This file provides some basic lemmas about possibly infinite lists represented by the type Stream'.Seq.

theorem Stream'.Seq.length'_of_terminates {α : Type u} {s : Seq α} (h : s.Terminates) : s.length' = ↑(s.length h)

theorem Stream'.Seq.length'_of_not_terminates {α : Type u} {s : Seq α} (h : ¬s.Terminates) : s.length' = ⊤

@[simp]

theorem Stream'.Seq.length_nil {α : Type u} : nil.length ⋯ = 0

@[simp]

theorem Stream'.Seq.length'_nil {α : Type u} : nil.length' = 0

theorem Stream'.Seq.length_cons {α : Type u} {x : α} {s : Seq α} (h : s.Terminates) : (cons x s).length ⋯ = s.length h + 1

@[simp]

theorem Stream'.Seq.length'_cons {α : Type u} (x : α) (s : Seq α) : (cons x s).length' = s.length' + 1

@[simp]

theorem Stream'.Seq.length_eq_zero {α : Type u} {s : Seq α} {h : s.Terminates} : s.length h = 0 ↔ s = nil

@[simp]

theorem Stream'.Seq.length'_eq_zero_iff_nil {α : Type u} (s : Seq α) : s.length' = 0 ↔ s = nil

theorem Stream'.Seq.length'_ne_zero_iff_cons {α : Type u} (s : Seq α) : s.length' ≠ 0 ↔ ∃ (x : α) (s' : Seq α), s = cons x s'

theorem Stream'.Seq.length_le_iff' {α : Type u} {s : Seq α} {n : ℕ} : (∃ (h : s.Terminates), s.length h ≤ n) ↔ s.TerminatedAt n

The statement of length_le_iff' does not assume that the sequence terminates. For a simpler statement of the theorem where the sequence is known to terminate see length_le_iff.

theorem Stream'.Seq.length_le_iff {α : Type u} {s : Seq α} {n : ℕ} {h : s.Terminates} : s.length h ≤ n ↔ s.TerminatedAt n

The statement of length_le_iff assumes that the sequence terminates. For a statement of the where the sequence is not known to terminate see length_le_iff'.

theorem Stream'.Seq.length'_le_iff {α : Type u} {s : Seq α} {n : ℕ} : s.length' ≤ ↑n ↔ s.TerminatedAt n

theorem Stream'.Seq.lt_length_iff' {α : Type u} {s : Seq α} {n : ℕ} : (∀ (h : s.Terminates), n < s.length h) ↔ ∃ (a : α), a ∈ s.get? n

The statement of lt_length_iff' does not assume that the sequence terminates. For a simpler statement of the theorem where the sequence is known to terminate see lt_length_iff.

theorem Stream'.Seq.lt_length_iff {α : Type u} {s : Seq α} {n : ℕ} {h : s.Terminates} : n < s.length h ↔ ∃ (a : α), a ∈ s.get? n

The statement of length_le_iff assumes that the sequence terminates. For a statement of the where the sequence is not known to terminate see length_le_iff'.

theorem Stream'.Seq.lt_length'_iff {α : Type u} {s : Seq α} {n : ℕ} : ↑n < s.length' ↔ ∃ (a : α), a ∈ s.get? n

@[simp]

theorem Stream'.Seq.ofStream_cons {α : Type u} (a : α) (s : Stream' α) : ↑(Stream'.cons a s) = cons a ↑s

theorem Stream'.Seq.terminatedAt_ofList {α : Type u} (l : List α) : (↑l).TerminatedAt l.length

theorem Stream'.Seq.terminates_ofList {α : Type u} (l : List α) : (↑l).Terminates

@[simp]

theorem Stream'.Seq.take_nil {α : Type u} {n : ℕ} : take n nil = []

@[simp]

theorem Stream'.Seq.take_zero {α : Type u} {s : Seq α} : take 0 s = []

@[simp]

theorem Stream'.Seq.take_succ_cons {α : Type u} {n : ℕ} {x : α} {s : Seq α} : take (n + 1) (cons x s) = x :: take n s

@[simp]

theorem Stream'.Seq.getElem?_take {α : Type u} (n k : ℕ) (s : Seq α) : (take k s)[n]? = if n < k then s.get? n else none

theorem Stream'.Seq.get?_mem_take {α : Type u} {s : Seq α} {m n : ℕ} (h_mn : m < n) {x : α} (h_get : s.get? m = some x) : x ∈ take n s

theorem Stream'.Seq.length_take_le {α : Type u} {s : Seq α} {n : ℕ} : (take n s).length ≤ n

theorem Stream'.Seq.length_take_of_le_length {α : Type u} {s : Seq α} {n : ℕ} (hle : ∀ (h : s.Terminates), n ≤ s.length h) : (take n s).length = n

@[simp]

theorem Stream'.Seq.length_toList {α : Type u} (s : Seq α) (h : s.Terminates) : (s.toList h).length = s.length h

@[simp]

theorem Stream'.Seq.getElem?_toList {α : Type u} (s : Seq α) (h : s.Terminates) (n : ℕ) : (s.toList h)[n]? = s.get? n

@[simp]

theorem Stream'.Seq.ofList_toList {α : Type u} (s : Seq α) (h : s.Terminates) : ↑(s.toList h) = s

@[simp]

theorem Stream'.Seq.toList_ofList {α : Type u} (l : List α) : (↑l).toList ⋯ = l

@[simp]

theorem Stream'.Seq.toList_nil {α : Type u} : nil.toList ⋯ = []

theorem Stream'.Seq.getLast?_toList {α : Type u} (s : Seq α) (h : s.Terminates) : (s.toList h).getLast? = s.get? (s.length h - 1)

@[simp]

theorem Stream'.Seq.cons_append {α : Type u} (a : α) (s t : Seq α) : (cons a s).append t = cons a (s.append t)

@[simp]

theorem Stream'.Seq.nil_append {α : Type u} (s : Seq α) : nil.append s = s

@[simp]

theorem Stream'.Seq.append_nil {α : Type u} (s : Seq α) : s.append nil = s

@[simp]

theorem Stream'.Seq.append_assoc {α : Type u} (s t u : Seq α) : (s.append t).append u = s.append (t.append u)

theorem Stream'.Seq.of_mem_append {α : Type u} {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁.append s₂) : a ∈ s₁ ∨ a ∈ s₂

theorem Stream'.Seq.mem_append_left {α : Type u} {s₁ s₂ : Seq α} {a : α} (h : a ∈ s₁) : a ∈ s₁.append s₂

@[simp]

theorem Stream'.Seq.ofList_append {α : Type u} (l l' : List α) : ↑(l ++ l') = (↑l).append ↑l'

@[simp]

theorem Stream'.Seq.ofStream_append {α : Type u} (l : List α) (s : Stream' α) : ↑(l ++ₛ s) = (↑l).append ↑s

@[simp]

theorem Stream'.Seq.map_get? {α : Type u} {β : Type v} (f : α → β) (s : Seq α) (n : ℕ) : (map f s).get? n = Option.map f (s.get? n)

@[simp]

theorem Stream'.Seq.map_nil {α : Type u} {β : Type v} (f : α → β) : map f nil = nil

@[simp]

theorem Stream'.Seq.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Seq α) : map f (cons a s) = cons (f a) (map f s)

@[simp]

theorem Stream'.Seq.map_id {α : Type u} (s : Seq α) : map id s = s

@[simp]

theorem Stream'.Seq.map_tail {α : Type u} {β : Type v} (f : α → β) (s : Seq α) : map f s.tail = (map f s).tail

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

@[simp]

theorem Stream'.Seq.terminatedAt_map_iff {α : Type u} {β : Type v} {f : α → β} {s : Seq α} {n : ℕ} : (map f s).TerminatedAt n ↔ s.TerminatedAt n

@[simp]

theorem Stream'.Seq.terminates_map_iff {α : Type u} {β : Type v} {f : α → β} {s : Seq α} : (map f s).Terminates ↔ s.Terminates

@[simp]

theorem Stream'.Seq.length_map {α : Type u} {β : Type v} {s : Seq α} {f : α → β} (h : (map f s).Terminates) : (map f s).length h = s.length ⋯

@[simp]

theorem Stream'.Seq.length'_map {α : Type u} {β : Type v} {s : Seq α} {f : α → β} : (map f s).length' = s.length'

theorem Stream'.Seq.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Seq α} : a ∈ s → f a ∈ map f s

theorem Stream'.Seq.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Seq α} : b ∈ map f s → ∃ a ∈ s, f a = b

@[simp]

theorem Stream'.Seq.map_append {α : Type u} {β : Type v} (f : α → β) (s t : Seq α) : map f (s.append t) = (map f s).append (map f t)

@[simp]

theorem Stream'.Seq.join_nil {α : Type u} : nil.join = nil

theorem Stream'.Seq.join_cons_nil {α : Type u} (a : α) (S : Seq (Seq1 α)) : (cons (a, nil) S).join = cons a S.join

theorem Stream'.Seq.join_cons_cons {α : Type u} (a b : α) (s : Seq α) (S : Seq (Seq1 α)) : (cons (a, cons b s) S).join = cons a (cons (b, s) S).join

@[simp]

theorem Stream'.Seq.join_cons {α : Type u} (a : α) (s : Seq α) (S : Seq (Seq1 α)) : (cons (a, s) S).join = cons a (s.append S.join)

@[simp]

theorem Stream'.Seq.join_append {α : Type u} (S T : Seq (Seq1 α)) : (S.append T).join = S.join.append T.join

@[simp]

theorem Stream'.Seq.drop_get? {α : Type u} {n m : ℕ} {s : Seq α} : (s.drop n).get? m = s.get? (n + m)

theorem Stream'.Seq.dropn_add {α : Type u} (s : Seq α) (m n : ℕ) : s.drop (m + n) = (s.drop m).drop n

theorem Stream'.Seq.dropn_tail {α : Type u} (s : Seq α) (n : ℕ) : s.tail.drop n = s.drop (n + 1)

@[simp]

theorem Stream'.Seq.head_dropn {α : Type u} (s : Seq α) (n : ℕ) : (s.drop n).head = s.get? n

@[simp]

theorem Stream'.Seq.drop_zero {α : Type u} {s : Seq α} : s.drop 0 = s

@[simp]

theorem Stream'.Seq.drop_succ_cons {α : Type u} {x : α} {s : Seq α} {n : ℕ} : (cons x s).drop (n + 1) = s.drop n

@[simp]

theorem Stream'.Seq.drop_nil {α : Type u} {n : ℕ} : nil.drop n = nil

@[simp, irreducible]

theorem Stream'.Seq.drop_length' {α : Type u} {n : ℕ} {s : Seq α} : (s.drop n).length' = s.length' - ↑n

theorem Stream'.Seq.take_drop {α : Type u} {s : Seq α} {n m : ℕ} : List.drop m (take n s) = take (n - m) (s.drop m)

@[simp]

theorem Stream'.Seq.get?_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s : Seq α) (s' : Seq β) (n : ℕ) : (zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n)

@[simp]

theorem Stream'.Seq.get?_zip {α : Type u} {β : Type v} (s : Seq α) (t : Seq β) (n : ℕ) : (s.zip t).get? n = Option.map₂ Prod.mk (s.get? n) (t.get? n)

@[simp]

theorem Stream'.Seq.nats_get? (n : ℕ) : nats.get? n = some n

@[simp]

theorem Stream'.Seq.get?_enum {α : Type u} (s : Seq α) (n : ℕ) : s.enum.get? n = Option.map (Prod.mk n) (s.get? n)

@[simp]

theorem Stream'.Seq.zipWith_nil_left {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Seq β} : zipWith f nil s = nil

@[simp]

theorem Stream'.Seq.zipWith_nil_right {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {s : Seq α} : zipWith f s nil = nil

@[simp]

theorem Stream'.Seq.zipWith_cons_cons {α : Type u} {β : Type v} {γ : Type w} {f : α → β → γ} {x : α} {s : Seq α} {x' : β} {s' : Seq β} : zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s')

@[simp]

theorem Stream'.Seq.zip_nil_left {α : Type u} {s : Seq α} : nil.zip s = nil

@[simp]

theorem Stream'.Seq.zip_nil_right {α : Type u} {s : Seq α} : s.zip nil = nil

@[simp]

theorem Stream'.Seq.zip_cons_cons {α : Type u} {s s' : Seq α} {x x' : α} : (cons x s).zip (cons x' s') = cons (x, x') (s.zip s')

@[simp]

theorem Stream'.Seq.enum_nil {α : Type u} : nil.enum = nil

@[simp]

theorem Stream'.Seq.enum_cons {α : Type u} (s : Seq α) (x : α) : (cons x s).enum = cons (0, x) (map (Prod.map Nat.succ id) s.enum)

theorem Stream'.Seq.zipWith_map {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f₁ : α → α') (f₂ : β → β') (g : α' → β' → γ) : zipWith g (map f₁ s₁) (map f₂ s₂) = zipWith (fun (a : α) (b : β) => g (f₁ a) (f₂ b)) s₁ s₂

theorem Stream'.Seq.zipWith_map_left {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} (s₁ : Seq α) (s₂ : Seq β) (f : α → α') (g : α' → β → γ) : zipWith g (map f s₁) s₂ = zipWith (fun (a : α) (b : β) => g (f a) b) s₁ s₂

theorem Stream'.Seq.zipWith_map_right {α : Type u} {β : Type v} {γ : Type w} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f : β → β') (g : α → β' → γ) : zipWith g s₁ (map f s₂) = zipWith (fun (a : α) (b : β) => g a (f b)) s₁ s₂

theorem Stream'.Seq.zip_map {α : Type u} {β : Type v} {α' : Type u'} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f₁ : α → α') (f₂ : β → β') : (map f₁ s₁).zip (map f₂ s₂) = map (Prod.map f₁ f₂) (s₁.zip s₂)

theorem Stream'.Seq.zip_map_left {α : Type u} {β : Type v} {α' : Type u'} (s₁ : Seq α) (s₂ : Seq β) (f : α → α') : (map f s₁).zip s₂ = map (Prod.map f id) (s₁.zip s₂)

theorem Stream'.Seq.zip_map_right {α : Type u} {β : Type v} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f : β → β') : s₁.zip (map f s₂) = map (Prod.map id f) (s₁.zip s₂)

@[simp]

theorem Stream'.Seq.fold_nil {α : Type u} {β : Type v} (init : β) (f : β → α → β) : nil.fold init f = cons init nil

@[simp]

theorem Stream'.Seq.fold_cons {α : Type u} {β : Type v} (init : β) (f : β → α → β) (x : α) (s : Seq α) : (cons x s).fold init f = cons init (s.fold (f init x) f)

@[simp]

theorem Stream'.Seq.fold_head {α : Type u} {β : Type v} (init : β) (f : β → α → β) (s : Seq α) : (s.fold init f).head = some init

theorem Stream'.Seq.get?_update {α : Type u} (f : α → α) (s : Seq α) (n m : ℕ) : (s.update n f).get? m = if m = n then Option.map f (s.get? m) else s.get? m

@[simp]

theorem Stream'.Seq.update_nil {α : Type u} (f : α → α) (n : ℕ) : nil.update n f = nil

@[simp]

theorem Stream'.Seq.set_nil {α : Type u} (n : ℕ) (x : α) : nil.set n x = nil

@[simp]

theorem Stream'.Seq.update_cons_zero {α : Type u} (hd : α) (tl : Seq α) (f : α → α) : (cons hd tl).update 0 f = cons (f hd) tl

@[simp]

theorem Stream'.Seq.set_cons_zero {α : Type u} (hd : α) (tl : Seq α) (hd' : α) : (cons hd tl).set 0 hd' = cons hd' tl

@[simp]

theorem Stream'.Seq.update_cons_succ {α : Type u} (hd : α) (tl : Seq α) (f : α → α) (n : ℕ) : (cons hd tl).update (n + 1) f = cons hd (tl.update n f)

@[simp]

theorem Stream'.Seq.set_cons_succ {α : Type u} (hd x : α) (tl : Seq α) (n : ℕ) : (cons hd tl).set (n + 1) x = cons hd (tl.set n x)

theorem Stream'.Seq.get?_set_of_not_terminatedAt {α : Type u} (x : α) {s : Seq α} {n : ℕ} (h_not_terminated : ¬s.TerminatedAt n) : (s.set n x).get? n = some x

theorem Stream'.Seq.get?_set_of_terminatedAt {α : Type u} (x : α) {s : Seq α} {n : ℕ} (h_terminated : s.TerminatedAt n) : (s.set n x).get? n = none

theorem Stream'.Seq.get?_set_of_ne {α : Type u} (x : α) (s : Seq α) {m n : ℕ} (h : n ≠ m) : (s.set m x).get? n = s.get? n

theorem Stream'.Seq.drop_set_of_lt {α : Type u} (x : α) (s : Seq α) {m n : ℕ} (h : m < n) : (s.set m x).drop n = s.drop n

theorem Stream'.Seq.all_cons {α : Type u} {p : α → Prop} {hd : α} {tl : Seq α} (h_hd : p hd) (h_tl : ∀ x ∈ tl, p x) (x : α) : x ∈ cons hd tl → p x

theorem Stream'.Seq.all_get {α : Type u} {p : α → Prop} {s : Seq α} (h : ∀ x ∈ s, p x) {n : ℕ} {x : α} (hx : s.get? n = some x) : p x

theorem Stream'.Seq.all_of_get {α : Type u} {p : α → Prop} {s : Seq α} (h : ∀ (n : ℕ) (x : α), s.get? n = some x → p x) (x : α) : x ∈ s → p x

theorem Stream'.Seq.all_coind {α : Type u} {s : Seq α} {p : α → Prop} (motive : Seq α → Prop) (base : motive s) (step : ∀ (hd : α) (tl : Seq α), motive (cons hd tl) → p hd ∧ motive tl) (x : α) : x ∈ s → p x

Coinductive principle for All.

theorem Stream'.Seq.map_all_iff {α β : Type u} {f : α → β} {p : β → Prop} {s : Seq α} : (∀ x ∈ map f s, p x) ↔ ∀ x ∈ s, (p ∘ f) x

theorem Stream'.Seq.take_all {α : Type u} {s : Seq α} {p : α → Prop} (h_all : ∀ x ∈ s, p x) {n : ℕ} {x : α} (hx : x ∈ take n s) : p x

theorem Stream'.Seq.set_all {α : Type u} {p : α → Prop} {s : Seq α} (h_all : ∀ x ∈ s, p x) {n : ℕ} {x : α} (hx : p x) (y : α) : y ∈ s.set n x → p y

@[simp]

theorem Stream'.Seq.Pairwise.nil {α : Type u} {R : α → α → Prop} : Pairwise R Seq.nil

theorem Stream'.Seq.Pairwise.cons {α : Type u} {R : α → α → Prop} {hd : α} {tl : Seq α} (h_hd : ∀ x ∈ tl, R hd x) (h_tl : Pairwise R tl) : Pairwise R (Seq.cons hd tl)

theorem Stream'.Seq.Pairwise.cons_elim {α : Type u} {R : α → α → Prop} {hd : α} {tl : Seq α} (h : Pairwise R (Seq.cons hd tl)) : (∀ x ∈ tl, R hd x) ∧ Pairwise R tl

@[simp]

theorem Stream'.Seq.Pairwise_cons_nil {α : Type u} {R : α → α → Prop} {hd : α} : Pairwise R (cons hd nil)

theorem Stream'.Seq.Pairwise_cons_cons_head {α : Type u} {R : α → α → Prop} {hd tl_hd : α} {tl_tl : Seq α} (h : Pairwise R (cons hd (cons tl_hd tl_tl))) : R hd tl_hd

theorem Stream'.Seq.Pairwise.cons_cons_of_trans {α : Type u} {R : α → α → Prop} [IsTrans α R] {hd tl_hd : α} {tl_tl : Seq α} (h_hd : R hd tl_hd) (h_tl : Pairwise R (Seq.cons tl_hd tl_tl)) : Pairwise R (Seq.cons hd (Seq.cons tl_hd tl_tl))

theorem Stream'.Seq.Pairwise.coind {α : Type u} {R : α → α → Prop} {s : Seq α} (motive : Seq α → Prop) (base : motive s) (step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl, R hd x) ∧ motive tl) : Pairwise R s

Coinductive principle for Pairwise.

theorem Stream'.Seq.Pairwise.coind_trans {α : Type u} {R : α → α → Prop} [IsTrans α R] {s : Seq α} (motive : Seq α → Prop) (base : motive s) (step : ∀ (hd : α) (tl : Seq α), motive (Seq.cons hd tl) → (∀ x ∈ tl.head, R hd x) ∧ motive tl) : Pairwise R s

Coinductive principle for Pairwise that assumes that R is transitive. Compared to Pairwise.coind, this allows you to prove R hd tl.head instead of tl.All (R hd ·) in step.

theorem Stream'.Seq.Pairwise_tail {α : Type u} {R : α → α → Prop} {s : Seq α} (h : Pairwise R s) : Pairwise R s.tail

theorem Stream'.Seq.Pairwise_drop {α : Type u} {R : α → α → Prop} {s : Seq α} (h : Pairwise R s) {n : ℕ} : Pairwise R (s.drop n)

theorem Stream'.Seq.at_least_as_long_as_coind {α : Type u} {β : Type v} {a : Seq α} {b : Seq β} (motive : Seq α → Seq β → Prop) (base : motive a b) (step : ∀ (a : Seq α) (b : Seq β), motive a b → ∀ (b_hd : β) (b_tl : Seq β), b = cons b_hd b_tl → ∃ (a_hd : α) (a_tl : Seq α), a = cons a_hd a_tl ∧ motive a_tl b_tl) : b.length' ≤ a.length'

Coinductive principle for proving b.length' ≤ a.length' for two sequences a and b.

instance Stream'.Seq.instFunctor : Functor Seq

Equations

• Stream'.Seq.instFunctor = { map := @Stream'.Seq.map }

instance Stream'.Seq.instLawfulFunctor : LawfulFunctor Seq

def Stream'.Seq1.toSeq {α : Type u} : Seq1 α → Seq α

Convert a Seq1 to a sequence.

Equations

• Stream'.Seq1.toSeq (a, s) = Stream'.Seq.cons a s

instance Stream'.Seq1.coeSeq {α : Type u} : Coe (Seq1 α) (Seq α)

Equations

• Stream'.Seq1.coeSeq = { coe := Stream'.Seq1.toSeq }

def Stream'.Seq1.map {α : Type u} {β : Type v} (f : α → β) : Seq1 α → Seq1 β

Map a function on a Seq1

Equations

• Stream'.Seq1.map f (a, s) = (f a, Stream'.Seq.map f s)

theorem Stream'.Seq1.map_pair {α : Type u} {β : Type v} {f : α → β} {a : α} {s : Seq α} : map f (a, s) = (f a, Seq.map f s)

theorem Stream'.Seq1.map_id {α : Type u} (s : Seq1 α) : map id s = s

def Stream'.Seq1.join {α : Type u} : Seq1 (Seq1 α) → Seq1 α

Flatten a nonempty sequence of nonempty sequences

Equations

• Stream'.Seq1.join ((a, s), S) = match s.destruct with | none => (a, S.join) | some s' => (a, (Stream'.Seq.cons s' S).join)

@[simp]

theorem Stream'.Seq1.join_nil {α : Type u} (a : α) (S : Seq (Seq1 α)) : join ((a, Seq.nil), S) = (a, S.join)

@[simp]

theorem Stream'.Seq1.join_cons {α : Type u} (a b : α) (s : Seq α) (S : Seq (Seq1 α)) : join ((a, Seq.cons b s), S) = (a, (Seq.cons (b, s) S).join)

def Stream'.Seq1.ret {α : Type u} (a : α) : Seq1 α

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

Equations

• Stream'.Seq1.ret a = (a, Stream'.Seq.nil)

instance Stream'.Seq1.instInhabited {α : Type u} [Inhabited α] : Inhabited (Seq1 α)

Equations

• Stream'.Seq1.instInhabited = { default := Stream'.Seq1.ret default }

def Stream'.Seq1.bind {α : Type u} {β : Type v} (s : Seq1 α) (f : α → 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

• s.bind f = (Stream'.Seq1.map f s).join

@[simp]

theorem Stream'.Seq1.join_map_ret {α : Type u} (s : Seq α) : (Seq.map ret s).join = s

@[simp]

theorem Stream'.Seq1.bind_ret {α : Type u} {β : Type v} (f : α → β) (s : Seq1 α) : s.bind (ret ∘ f) = map f s

@[simp]

theorem Stream'.Seq1.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → Seq1 β) : (ret a).bind f = f a

@[simp]

theorem Stream'.Seq1.map_join' {α : Type u} {β : Type v} (f : α → β) (S : Seq (Seq1 α)) : Seq.map f S.join = (Seq.map (map f) S).join

@[simp]

theorem Stream'.Seq1.map_join {α : Type u} {β : Type v} (f : α → β) (S : Seq1 (Seq1 α)) : map f S.join = (map (map f) S).join

@[simp]

theorem Stream'.Seq1.join_join {α : Type u} (SS : Seq (Seq1 (Seq1 α))) : SS.join.join = (Seq.map join SS).join

@[simp]

theorem Stream'.Seq1.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Seq1 α) (f : α → Seq1 β) (g : β → Seq1 γ) : (s.bind f).bind g = s.bind fun (x : α) => (f x).bind g

instance Stream'.Seq1.monad : Monad Seq1

Equations

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

instance Stream'.Seq1.lawfulMonad : LawfulMonad Seq1