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' (Option α)) : Prop

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

Equations

• Stream'.IsSeq s = ∀ {n : ℕ}, s n = none → s (n + 1) = none

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 : Stream' (Option α) // Stream'.IsSeq f }

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

Seq1 α is the type of nonempty sequences.

Equations

• Stream'.Seq1 α = (α × Stream'.Seq α)

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

The empty sequence

Equations

• Stream'.Seq.nil = { val := Stream'.const none, property := (_ : ∀ {x : ℕ}, Stream'.const none x = none → Stream'.const none (x + 1) = Stream'.const none (x + 1)) }

instance Stream'.Seq.instInhabitedSeq {α : Type u} : Inhabited (Stream'.Seq α)

Equations

• Stream'.Seq.instInhabitedSeq = { default := Stream'.Seq.nil }

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

Prepend an element to a sequence

Equations

• Stream'.Seq.cons a s = { val := Stream'.cons (some a) ↑s, property := (_ : ∀ {n : ℕ}, Stream'.cons (some a) (↑s) n = none → Stream'.cons (some a) (↑s) (n + 1) = none) }

@[simp]

theorem Stream'.Seq.val_cons {α : Type u} (s : Stream'.Seq α) (x : α) : ↑(Stream'.Seq.cons x s) = Stream'.cons (some x) ↑s

def Stream'.Seq.get? {α : Type u} : Stream'.Seq α → ℕ → Option α

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

Equations

• Stream'.Seq.get? = Subtype.val

@[simp]

theorem Stream'.Seq.get?_mk {α : Type u} (f : Stream' (Option α)) (hf : Stream'.IsSeq f) : 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 : Stream'.Seq α) : Stream'.Seq.get? (Stream'.Seq.cons a s) 0 = some a

@[simp]

theorem Stream'.Seq.get?_cons_succ {α : Type u} (a : α) (s : Stream'.Seq α) (n : ℕ) : Stream'.Seq.get? (Stream'.Seq.cons a s) (n + 1) = Stream'.Seq.get? s n

theorem Stream'.Seq.ext {α : Type u} {s : Stream'.Seq α} {t : Stream'.Seq α} (h : ∀ (n : ℕ), Stream'.Seq.get? s n = Stream'.Seq.get? t n) : s = t

theorem Stream'.Seq.cons_injective2 {α : Type u} : Function.Injective2 Stream'.Seq.cons

theorem Stream'.Seq.cons_left_injective {α : Type u} (s : Stream'.Seq α) : Function.Injective fun (x : α) => Stream'.Seq.cons x s

theorem Stream'.Seq.cons_right_injective {α : Type u} (x : α) : Function.Injective (Stream'.Seq.cons x)

def Stream'.Seq.TerminatedAt {α : Type u} (s : Stream'.Seq α) (n : ℕ) : Prop

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

Equations

• Stream'.Seq.TerminatedAt s n = (Stream'.Seq.get? s n = none)

instance Stream'.Seq.terminatedAtDecidable {α : Type u} (s : Stream'.Seq α) (n : ℕ) : Decidable (Stream'.Seq.TerminatedAt s n)

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

Equations

• Stream'.Seq.terminatedAtDecidable s n = decidable_of_iff' (Option.isNone (Stream'.Seq.get? s n) = true) (_ : Stream'.Seq.TerminatedAt s n ↔ Option.isNone (Stream'.Seq.get? s n) = true)

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

• Stream'.Seq.Terminates s = ∃ (n : ℕ), Stream'.Seq.TerminatedAt s n

theorem Stream'.Seq.not_terminates_iff {α : Type u} {s : Stream'.Seq α} : ¬Stream'.Seq.Terminates s ↔ ∀ (n : ℕ), Option.isSome (Stream'.Seq.get? s n) = true

def Stream'.Seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : β → γ) : Option (α × β) → Option (α × γ)

Functorial action of the functor Option (α × _)

Equations

• Stream'.Seq.omap f x = match x with | none => none | some (a, b) => some (a, f b)

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

Get the first element of a sequence

Equations

• Stream'.Seq.head s = Stream'.Seq.get? s 0

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

• Stream'.Seq.tail s = { val := Stream'.tail ↑s, property := (_ : ∀ {n : ℕ}, Stream'.tail (↑s) n = none → Stream'.tail (↑s) (n + 1) = none) }

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

member definition for Seq

Equations

• Stream'.Seq.Mem a s = (some a ∈ ↑s)

instance Stream'.Seq.instMembershipSeq {α : Type u} : Membership α (Stream'.Seq α)

Equations

• Stream'.Seq.instMembershipSeq = { mem := Stream'.Seq.Mem }

theorem Stream'.Seq.le_stable {α : Type u} (s : Stream'.Seq α) {m : ℕ} {n : ℕ} (h : m ≤ n) : Stream'.Seq.get? s m = none → Stream'.Seq.get? s n = none

theorem Stream'.Seq.terminated_stable {α : Type u} (s : Stream'.Seq α) {m : ℕ} {n : ℕ} : m ≤ n → Stream'.Seq.TerminatedAt s m → Stream'.Seq.TerminatedAt s 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 : Stream'.Seq.get? s n = some aₙ) : ∃ (aₘ : α), Stream'.Seq.get? s m = 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 : Stream'.Seq α) : a ∈ Stream'.Seq.cons a s

theorem Stream'.Seq.mem_cons_of_mem {α : Type u} (y : α) {a : α} {s : Stream'.Seq α} : a ∈ s → a ∈ Stream'.Seq.cons y s

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

@[simp]

theorem Stream'.Seq.mem_cons_iff {α : Type u} {a : α} {b : α} {s : Stream'.Seq α} : a ∈ Stream'.Seq.cons b s ↔ a = b ∨ a ∈ s

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

• Stream'.Seq.destruct s = (fun (a' : α) => (a', Stream'.Seq.tail s)) <$> Stream'.Seq.get? s 0

theorem Stream'.Seq.destruct_eq_nil {α : Type u} {s : Stream'.Seq α} : Stream'.Seq.destruct s = none → s = Stream'.Seq.nil

theorem Stream'.Seq.destruct_eq_cons {α : Type u} {s : Stream'.Seq α} {a : α} {s' : Stream'.Seq α} : Stream'.Seq.destruct s = some (a, s') → s = Stream'.Seq.cons a 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 : Stream'.Seq α) : Stream'.Seq.destruct (Stream'.Seq.cons a s) = some (a, s)

theorem Stream'.Seq.head_eq_destruct {α : Type u} (s : Stream'.Seq α) : Stream'.Seq.head s = Prod.fst <$> Stream'.Seq.destruct s

@[simp]

theorem Stream'.Seq.head_nil {α : Type u} : Stream'.Seq.head Stream'.Seq.nil = none

@[simp]

theorem Stream'.Seq.head_cons {α : Type u} (a : α) (s : Stream'.Seq α) : Stream'.Seq.head (Stream'.Seq.cons a s) = some a

@[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 : Stream'.Seq α) : Stream'.Seq.tail (Stream'.Seq.cons a s) = s

@[simp]

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

def Stream'.Seq.recOn {α : 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.recOn.

Equations

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

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

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 x = match x with | none => (none, none) | some b => match f b with | none => (none, none) | some (a, b') => (some a, some b')

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

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

@[simp]

theorem Stream'.Seq.corec_eq {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β) : Stream'.Seq.destruct (Stream'.Seq.corec f b) = Stream'.Seq.omap (Stream'.Seq.corec f) (f b)

def Stream'.Seq.BisimO {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop) : Option (Stream'.Seq1 α) → Option (Stream'.Seq1 α) → Prop

Bisimilarity relation over Option of Seq1 α

Equations

• Stream'.Seq.BisimO R x✝ x = match x✝, x with | none, none => True | some (a, s), some (a', s') => a = a' ∧ R s s' | x, x_1 => False

def Stream'.Seq.IsBisimulation {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop) : Prop

a relation is bisimilar if it meets the BisimO test

Equations

• Stream'.Seq.IsBisimulation R = ∀ ⦃s₁ s₂ : Stream'.Seq α⦄, R s₁ s₂ → Stream'.Seq.BisimO R (Stream'.Seq.destruct s₁) (Stream'.Seq.destruct s₂)

theorem Stream'.Seq.eq_of_bisim {α : Type u} (R : Stream'.Seq α → Stream'.Seq α → Prop) (bisim : Stream'.Seq.IsBisimulation R) {s₁ : Stream'.Seq α} {s₂ : Stream'.Seq α} (r : R s₁ s₂) : s₁ = s₂

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

theorem Stream'.Seq.coinduction2 {α : Type u} {β : Type v} (s : Stream'.Seq α) (f : Stream'.Seq α → Stream'.Seq β) (g : Stream'.Seq α → Stream'.Seq β) (H : ∀ (s : Stream'.Seq α), Stream'.Seq.BisimO (fun (s1 s2 : Stream'.Seq β) => ∃ (s : Stream'.Seq α), 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 α) : Stream'.Seq α

Embed a list as a sequence

Equations

• ↑l = { val := List.get? l, property := (_ : ∀ {n : ℕ}, List.get? l n = none → List.get? l (n + 1) = none) }

instance Stream'.Seq.coeList {α : Type u} : Coe (List α) (Stream'.Seq α)

Equations

• Stream'.Seq.coeList = { coe := Stream'.Seq.ofList }

@[simp]

theorem Stream'.Seq.ofList_nil {α : Type u} : ↑[] = Stream'.Seq.nil

@[simp]

theorem Stream'.Seq.ofList_get {α : Type u} (l : List α) (n : ℕ) : Stream'.Seq.get? (↑l) n = List.get? l n

@[simp]

theorem Stream'.Seq.ofList_cons {α : Type u} (a : α) (l : List α) : ↑(a :: l) = Stream'.Seq.cons a ↑l

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

Embed an infinite stream as a sequence

Equations

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

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

Equations

• Stream'.Seq.coeStream = { coe := Stream'.Seq.ofStream }

def Stream'.Seq.ofLazyList {α : Type u} : LazyList α → Stream'.Seq α

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.

Equations

• Stream'.Seq.ofLazyList = Stream'.Seq.corec fun (l : LazyList α) => match l with | LazyList.nil => none | LazyList.cons a l' => some (a, Thunk.get l')

instance Stream'.Seq.coeLazyList {α : Type u} : Coe (LazyList α) (Stream'.Seq α)

Equations

• Stream'.Seq.coeLazyList = { coe := Stream'.Seq.ofLazyList }

unsafe def Stream'.Seq.toLazyList {α : Type u} : Stream'.Seq α → LazyList α

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

Equations

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

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

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

Equations

• Stream'.Seq.forceToList s = LazyList.toList (Stream'.Seq.toLazyList s)

def Stream'.Seq.nats : Stream'.Seq ℕ

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

Equations

• Stream'.Seq.nats = ↑Stream'.nats

@[simp]

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

def Stream'.Seq.append {α : Type u} (s₁ : Stream'.Seq α) (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

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

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

Map a function over a sequence.

Equations

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

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

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

def Stream'.Seq.drop {α : Type u} (s : Stream'.Seq α) : ℕ → Stream'.Seq α

Remove the first n elements from the sequence.

Equations

• Stream'.Seq.drop s 0 = s
• Stream'.Seq.drop s (Nat.succ n) = Stream'.Seq.tail (Stream'.Seq.drop s n)

def Stream'.Seq.take {α : Type u} : ℕ → Stream'.Seq α → List α

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

Equations

• Stream'.Seq.take 0 x = []
• Stream'.Seq.take (Nat.succ n) x = match Stream'.Seq.destruct x with | none => [] | some (x, r) => x :: Stream'.Seq.take n r

def Stream'.Seq.splitAt {α : Type u} : ℕ → Stream'.Seq α → List α × Stream'.Seq α

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.
• Stream'.Seq.splitAt 0 x = ([], x)

def Stream'.Seq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) : Stream'.Seq γ

Combine two sequences with a function

Equations

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

@[simp]

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

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.zipWith Prod.mk

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

def Stream'.Seq.unzip {α : Type u} {β : Type v} (s : Stream'.Seq (α × β)) : Stream'.Seq α × Stream'.Seq β

Separate a sequence of pairs into two sequences

Equations

• Stream'.Seq.unzip s = (Stream'.Seq.map Prod.fst s, Stream'.Seq.map Prod.snd s)

def Stream'.Seq.enum {α : Type u} (s : Stream'.Seq α) : Stream'.Seq (ℕ × α)

Enumerate a sequence by tagging each element with its index.

Equations

• Stream'.Seq.enum s = Stream'.Seq.zip Stream'.Seq.nats s

@[simp]

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

@[simp]

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

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

Convert a sequence which is known to terminate into a list

Equations

• Stream'.Seq.toList s h = Stream'.Seq.take (Nat.find h) s

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

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

Equations

• Stream'.Seq.toStream s h n = Option.get (Stream'.Seq.get? s n) (_ : Option.isSome (Stream'.Seq.get? s n) = true)

def Stream'.Seq.toListOrStream {α : Type u} (s : Stream'.Seq α) [Decidable (Stream'.Seq.Terminates s)] : 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

• Stream'.Seq.toListOrStream s = if h : Stream'.Seq.Terminates s then Sum.inl (Stream'.Seq.toList s h) else Sum.inr (Stream'.Seq.toStream s h)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Stream'.Seq.append_assoc {α : Type u} (s : Stream'.Seq α) (t : Stream'.Seq α) (u : Stream'.Seq α) : Stream'.Seq.append (Stream'.Seq.append s t) u = Stream'.Seq.append s (Stream'.Seq.append 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 : Stream'.Seq α) : Stream'.Seq.map f (Stream'.Seq.cons a s) = Stream'.Seq.cons (f a) (Stream'.Seq.map f s)

@[simp]

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

@[simp]

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

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)

@[simp]

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

@[simp]

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

instance Stream'.Seq.instFunctorSeq : Functor Stream'.Seq

Equations

• Stream'.Seq.instFunctorSeq = { map := @Stream'.Seq.map, mapConst := fun {α β : Type u_1} => Stream'.Seq.map ∘ Function.const β }

instance Stream'.Seq.instLawfulFunctorSeqInstFunctorSeq : LawfulFunctor Stream'.Seq

Equations

• Stream'.Seq.instLawfulFunctorSeqInstFunctorSeq = (_ : LawfulFunctor Stream'.Seq)

@[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 (Stream'.Seq1 α)) : Stream'.Seq.join (Stream'.Seq.cons (a, Stream'.Seq.nil) S) = Stream'.Seq.cons a (Stream'.Seq.join S)

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

@[simp]

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

@[simp]

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

@[simp]

theorem Stream'.Seq.ofStream_cons {α : Type u} (a : α) (s : Stream' α) : ↑(Stream'.cons a s) = Stream'.Seq.cons 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 : Stream' α) : ↑(l ++ₛ s) = Stream'.Seq.append ↑l ↑s

def Stream'.Seq.toList' {α : 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

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

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

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

@[simp]

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

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

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

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

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

@[simp]

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

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

Convert a Seq1 to a sequence.

Equations

• Stream'.Seq1.toSeq x = match x with | (a, s) => Stream'.Seq.cons a s

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

Equations

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

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

Map a function on a Seq1

Equations

• Stream'.Seq1.map f x = match x with | (a, s) => (f a, Stream'.Seq.map f s)

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

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

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

Flatten a nonempty sequence of nonempty sequences

Equations

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

@[simp]

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

@[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.join (Stream'.Seq.cons (b, s) S))

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)

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

Equations

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

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

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

@[simp]

theorem Stream'.Seq1.join_map_ret {α : Type u} (s : Stream'.Seq α) : 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 α) : Stream'.Seq1.bind s (Stream'.Seq1.ret ∘ f) = Stream'.Seq1.map f s

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance Stream'.Seq1.monad : Monad Stream'.Seq1

Equations

• Stream'.Seq1.monad = Monad.mk

instance Stream'.Seq1.lawfulMonad : LawfulMonad Stream'.Seq1

Equations

• Stream'.Seq1.lawfulMonad = (_ : LawfulMonad Stream'.Seq1)