Partially defined possibly infinite lists

This file provides a WSeq α type representing partially defined possibly infinite lists (referred here as weak sequences).

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

Weak sequences.

While the Seq structure allows for lists which may not be finite, a weak sequence also allows the computation of each element to involve an indeterminate amount of computation, including possibly an infinite loop. This is represented as a regular Seq interspersed with none elements to indicate that computation is ongoing.

This model is appropriate for Haskell style lazy lists, and is closed under most interesting computation patterns on infinite lists, but conversely it is difficult to extract elements from it.

def Stream'.WSeq.ofSeq {α : Type u} : Stream'.Seq α → Stream'.WSeq α

Turn a sequence into a weak sequence

def Stream'.WSeq.ofList {α : Type u} (l : List α) : Stream'.WSeq α

Turn a list into a weak sequence

def Stream'.WSeq.ofStream {α : Type u} (l : Stream' α) : Stream'.WSeq α

Turn a stream into a weak sequence

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

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

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

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

The empty weak sequence

instance Stream'.WSeq.inhabited {α : Type u} : Inhabited (Stream'.WSeq α)

def Stream'.WSeq.cons {α : Type u} (a : α) : Stream'.WSeq α → Stream'.WSeq α

Prepend an element to a weak sequence

def Stream'.WSeq.think {α : Type u} : Stream'.WSeq α → Stream'.WSeq α

Compute for one tick, without producing any elements

def Stream'.WSeq.destruct {α : Type u} : Stream'.WSeq α → Computation (Option (α × Stream'.WSeq α))

Destruct a weak sequence, to (eventually possibly) produce either none for nil or some (a, s) if an element is produced.

def Stream'.WSeq.recOn {α : Type u} {C : Stream'.WSeq α → Sort v} (s : Stream'.WSeq α) (h1 : C Stream'.WSeq.nil) (h2 : (x : α) → (s : Stream'.WSeq α) → C (Stream'.WSeq.cons x s)) (h3 : (s : Stream'.WSeq α) → C (Stream'.WSeq.think s)) : C s

Recursion principle for weak sequences, compare with List.recOn.

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

membership for weak sequences

instance Stream'.WSeq.membership {α : Type u} : Membership α (Stream'.WSeq α)

theorem Stream'.WSeq.not_mem_nil {α : Type u} (a : α) : ¬a ∈ Stream'.WSeq.nil

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

Get the head of a weak sequence. This involves a possibly infinite computation.

def Stream'.WSeq.flatten {α : Type u} : Computation (Stream'.WSeq α) → Stream'.WSeq α

Encode a computation yielding a weak sequence into additional think constructors in a weak sequence

def Stream'.WSeq.tail {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq α

Get the tail of a weak sequence. This doesn't need a Computation wrapper, unlike head, because flatten allows us to hide this in the construction of the weak sequence itself.

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

drop the first n elements from s.

Equations

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

def Stream'.WSeq.get? {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Computation (Option α)

Get the nth element of s.

def Stream'.WSeq.toList {α : Type u} (s : Stream'.WSeq α) : Computation (List α)

Convert s to a list (if it is finite and completes in finite time).

def Stream'.WSeq.length {α : Type u} (s : Stream'.WSeq α) : Computation ℕ

Get the length of s (if it is finite and completes in finite time).

class Stream'.WSeq.IsFinite {α : Type u} (s : Stream'.WSeq α) : Prop

• out : Computation.Terminates (Stream'.WSeq.toList s✝)

A weak sequence is finite if toList s terminates. Equivalently, it is a finite number of think and cons applied to nil.

instance Stream'.WSeq.toList_terminates {α : Type u} (s : Stream'.WSeq α) [h : Stream'.WSeq.IsFinite s] : Computation.Terminates (Stream'.WSeq.toList s)

def Stream'.WSeq.get {α : Type u} (s : Stream'.WSeq α) [Stream'.WSeq.IsFinite s] : List α

Get the list corresponding to a finite weak sequence.

class Stream'.WSeq.Productive {α : Type u} (s : Stream'.WSeq α) : Prop

• get?_terminates : ∀ (n : ℕ), Computation.Terminates (Stream'.WSeq.get? s✝ n)

A weak sequence is productive if it never stalls forever - there are always a finite number of thinks between cons constructors. The sequence itself is allowed to be infinite though.

theorem Stream'.WSeq.productive_iff {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.Productive s ↔ ∀ (n : ℕ), Computation.Terminates (Stream'.WSeq.get? s n)

instance Stream'.WSeq.get?_terminates {α : Type u} (s : Stream'.WSeq α) [h : Stream'.WSeq.Productive s] (n : ℕ) : Computation.Terminates (Stream'.WSeq.get? s n)

instance Stream'.WSeq.head_terminates {α : Type u} (s : Stream'.WSeq α) [Stream'.WSeq.Productive s] : Computation.Terminates (Stream'.WSeq.head s)

def Stream'.WSeq.updateNth {α : Type u} (s : Stream'.WSeq α) (n : ℕ) (a : α) : Stream'.WSeq α

Replace the nth element of s with a.

def Stream'.WSeq.removeNth {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Stream'.WSeq α

Remove the nth element of s.

def Stream'.WSeq.filterMap {α : Type u} {β : Type v} (f : α → Option β) : Stream'.WSeq α → Stream'.WSeq β

Map the elements of s over f, removing any values that yield none.

def Stream'.WSeq.filter {α : Type u} (p : α → Prop) [DecidablePred p] : Stream'.WSeq α → Stream'.WSeq α

Select the elements of s that satisfy p.

def Stream'.WSeq.find {α : Type u} (p : α → Prop) [DecidablePred p] (s : Stream'.WSeq α) : Computation (Option α)

Get the first element of s satisfying p.

def Stream'.WSeq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq β) : Stream'.WSeq γ

Zip a function over two weak sequences

def Stream'.WSeq.zip {α : Type u} {β : Type v} : Stream'.WSeq α → Stream'.WSeq β → Stream'.WSeq (α × β)

Zip two weak sequences into a single sequence of pairs

def Stream'.WSeq.findIndexes {α : Type u} (p : α → Prop) [DecidablePred p] (s : Stream'.WSeq α) : Stream'.WSeq ℕ

Get the list of indexes of elements of s satisfying p

def Stream'.WSeq.findIndex {α : Type u} (p : α → Prop) [DecidablePred p] (s : Stream'.WSeq α) : Computation ℕ

Get the index of the first element of s satisfying p

def Stream'.WSeq.indexOf {α : Type u} [DecidableEq α] (a : α) : Stream'.WSeq α → Computation ℕ

Get the index of the first occurrence of a in s

def Stream'.WSeq.indexesOf {α : Type u} [DecidableEq α] (a : α) : Stream'.WSeq α → Stream'.WSeq ℕ

Get the indexes of occurrences of a in s

def Stream'.WSeq.union {α : Type u} (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq α) : Stream'.WSeq α

union s1 s2 is a weak sequence which interleaves s1 and s2 in some order (nondeterministically).

def Stream'.WSeq.isEmpty {α : Type u} (s : Stream'.WSeq α) : Computation Bool

Returns true if s is nil and false if s has an element

def Stream'.WSeq.compute {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq α

Calculate one step of computation

def Stream'.WSeq.take {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Stream'.WSeq α

Get the first n elements of a weak sequence

def Stream'.WSeq.splitAt {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Computation (List α × Stream'.WSeq α)

Split the sequence at position n into a finite initial segment and the weak sequence tail

def Stream'.WSeq.any {α : Type u} (s : Stream'.WSeq α) (p : α → Bool) : Computation Bool

Returns true if any element of s satisfies p

def Stream'.WSeq.all {α : Type u} (s : Stream'.WSeq α) (p : α → Bool) : Computation Bool

Returns true if every element of s satisfies p

def Stream'.WSeq.scanl {α : Type u} {β : Type v} (f : α → β → α) (a : α) (s : Stream'.WSeq β) : Stream'.WSeq α

Apply a function to the elements of the sequence to produce a sequence of partial results. (There is no scanr because this would require working from the end of the sequence, which may not exist.)

def Stream'.WSeq.inits {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq (List α)

Get the weak sequence of initial segments of the input sequence

def Stream'.WSeq.collect {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : List α

Like take, but does not wait for a result. Calculates n steps of computation and returns the sequence computed so far

def Stream'.WSeq.append {α : Type u} : Stream'.WSeq α → Stream'.WSeq α → Stream'.WSeq α

Append two weak sequences. As with Seq.append, this may not use the second sequence if the first one takes forever to compute

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

Map a function over a weak sequence

def Stream'.WSeq.join {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) : Stream'.WSeq α

Flatten a sequence of weak sequences. (Note that this allows empty sequences, unlike Seq.join.)

def Stream'.WSeq.bind {α : Type u} {β : Type v} (s : Stream'.WSeq α) (f : α → Stream'.WSeq β) : Stream'.WSeq β

Monadic bind operator for weak sequences

def Stream'.WSeq.LiftRelO {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop) : Option (α × Stream'.WSeq α) → Option (β × Stream'.WSeq β) → Prop

lift a relation to a relation over weak sequences

theorem Stream'.WSeq.LiftRelO.imp {α : Type u} {β : Type v} {R : α → β → Prop} {S : α → β → Prop} {C : Stream'.WSeq α → Stream'.WSeq β → Prop} {D : Stream'.WSeq α → Stream'.WSeq β → Prop} (H1 : (a : α) → (b : β) → R a b → S a b) (H2 : (s : Stream'.WSeq α) → (t : Stream'.WSeq β) → C s t → D s t) {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)} : Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO S D o p

theorem Stream'.WSeq.LiftRelO.imp_right {α : Type u} {β : Type v} (R : α → β → Prop) {C : Stream'.WSeq α → Stream'.WSeq β → Prop} {D : Stream'.WSeq α → Stream'.WSeq β → Prop} (H : (s : Stream'.WSeq α) → (t : Stream'.WSeq β) → C s t → D s t) {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)} : Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO R D o p

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

Definition of bisimilarity for weak sequences

theorem Stream'.WSeq.BisimO.imp {α : Type u} {R : Stream'.WSeq α → Stream'.WSeq α → Prop} {S : Stream'.WSeq α → Stream'.WSeq α → Prop} (H : (s t : Stream'.WSeq α) → R s t → S s t) {o : Option (α × Stream'.WSeq α)} {p : Option (α × Stream'.WSeq α)} : Stream'.WSeq.BisimO R o p → Stream'.WSeq.BisimO S o p

def Stream'.WSeq.LiftRel {α : Type u} {β : Type v} (R : α → β → Prop) (s : Stream'.WSeq α) (t : Stream'.WSeq β) : Prop

Two weak sequences are LiftRel R related if they are either both empty, or they are both nonempty and the heads are R related and the tails are LiftRel R related. (This is a coinductive definition.)

def Stream'.WSeq.Equiv {α : Type u} : Stream'.WSeq α → Stream'.WSeq α → Prop

If two sequences are equivalent, then they have the same values and the same computational behavior (i.e. if one loops forever then so does the other), although they may differ in the number of thinks needed to arrive at the answer.

theorem Stream'.WSeq.liftRel_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β} : Stream'.WSeq.LiftRel R s t → Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) (Stream'.WSeq.destruct s) (Stream'.WSeq.destruct t)

theorem Stream'.WSeq.liftRel_destruct_iff {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β} : Stream'.WSeq.LiftRel R s t ↔ Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) (Stream'.WSeq.destruct s) (Stream'.WSeq.destruct t)

def Stream'.WSeq.«term_~ʷ_» : Lean.TrailingParserDescr

theorem Stream'.WSeq.destruct_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} : s ~ʷ t → Computation.LiftRel (Stream'.WSeq.BisimO fun x x_1 => x ~ʷ x_1) (Stream'.WSeq.destruct s) (Stream'.WSeq.destruct t)

theorem Stream'.WSeq.destruct_congr_iff {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} : s ~ʷ t ↔ Computation.LiftRel (Stream'.WSeq.BisimO fun x x_1 => x ~ʷ x_1) (Stream'.WSeq.destruct s) (Stream'.WSeq.destruct t)

theorem Stream'.WSeq.LiftRel.refl {α : Type u} (R : α → α → Prop) (H : Reflexive R) : Reflexive (Stream'.WSeq.LiftRel R)

theorem Stream'.WSeq.LiftRelO.swap {α : Type u} {β : Type v} (R : α → β → Prop) (C : Stream'.WSeq α → Stream'.WSeq β → Prop) : Function.swap (Stream'.WSeq.LiftRelO R C) = Stream'.WSeq.LiftRelO (Function.swap R) (Function.swap C)

theorem Stream'.WSeq.LiftRel.swap_lem {α : Type u} {β : Type v} {R : α → β → Prop} {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} (h : Stream'.WSeq.LiftRel R s1 s2) : Stream'.WSeq.LiftRel (Function.swap R) s2 s1

theorem Stream'.WSeq.LiftRel.swap {α : Type u} {β : Type v} (R : α → β → Prop) : Function.swap (Stream'.WSeq.LiftRel R) = Stream'.WSeq.LiftRel (Function.swap R)

theorem Stream'.WSeq.LiftRel.symm {α : Type u} (R : α → α → Prop) (H : Symmetric R) : Symmetric (Stream'.WSeq.LiftRel R)

theorem Stream'.WSeq.LiftRel.trans {α : Type u} (R : α → α → Prop) (H : Transitive R) : Transitive (Stream'.WSeq.LiftRel R)

theorem Stream'.WSeq.LiftRel.equiv {α : Type u} (R : α → α → Prop) : Equivalence R → Equivalence (Stream'.WSeq.LiftRel R)

theorem Stream'.WSeq.Equiv.refl {α : Type u} (s : Stream'.WSeq α) : s ~ʷ s

theorem Stream'.WSeq.Equiv.symm {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} : s ~ʷ t → t ~ʷ s

theorem Stream'.WSeq.Equiv.trans {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} {u : Stream'.WSeq α} : s ~ʷ t → t ~ʷ u → s ~ʷ u

theorem Stream'.WSeq.Equiv.equivalence {α : Type u} : Equivalence Stream'.WSeq.Equiv

@[simp]

theorem Stream'.WSeq.destruct_nil {α : Type u} : Stream'.WSeq.destruct Stream'.WSeq.nil = Computation.pure none

@[simp]

theorem Stream'.WSeq.destruct_cons {α : Type u} (a : α) (s : Stream'.WSeq α) : Stream'.WSeq.destruct (Stream'.WSeq.cons a s) = Computation.pure (some (a, s))

@[simp]

theorem Stream'.WSeq.destruct_think {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.destruct (Stream'.WSeq.think s) = Computation.think (Stream'.WSeq.destruct s)

@[simp]

theorem Stream'.WSeq.seq_destruct_nil {α : Type u} : Stream'.Seq.destruct Stream'.WSeq.nil = none

@[simp]

theorem Stream'.WSeq.seq_destruct_cons {α : Type u} (a : α) (s : Stream'.WSeq α) : Stream'.Seq.destruct (Stream'.WSeq.cons a s) = some (some a, s)

@[simp]

theorem Stream'.WSeq.seq_destruct_think {α : Type u} (s : Stream'.WSeq α) : Stream'.Seq.destruct (Stream'.WSeq.think s) = some (none, s)

@[simp]

theorem Stream'.WSeq.head_nil {α : Type u} : Stream'.WSeq.head Stream'.WSeq.nil = Computation.pure none

@[simp]

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

@[simp]

theorem Stream'.WSeq.head_think {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.head (Stream'.WSeq.think s) = Computation.think (Stream'.WSeq.head s)

@[simp]

theorem Stream'.WSeq.flatten_pure {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.flatten (Computation.pure s) = s

@[simp]

theorem Stream'.WSeq.flatten_think {α : Type u} (c : Computation (Stream'.WSeq α)) : Stream'.WSeq.flatten (Computation.think c) = Stream'.WSeq.think (Stream'.WSeq.flatten c)

@[simp]

theorem Stream'.WSeq.destruct_flatten {α : Type u} (c : Computation (Stream'.WSeq α)) : Stream'.WSeq.destruct (Stream'.WSeq.flatten c) = c >>= Stream'.WSeq.destruct

theorem Stream'.WSeq.head_terminates_iff {α : Type u} (s : Stream'.WSeq α) : Computation.Terminates (Stream'.WSeq.head s) ↔ Computation.Terminates (Stream'.WSeq.destruct s)

@[simp]

theorem Stream'.WSeq.tail_nil {α : Type u} : Stream'.WSeq.tail Stream'.WSeq.nil = Stream'.WSeq.nil

@[simp]

theorem Stream'.WSeq.tail_cons {α : Type u} (a : α) (s : Stream'.WSeq α) : Stream'.WSeq.tail (Stream'.WSeq.cons a s) = s

@[simp]

theorem Stream'.WSeq.tail_think {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.tail (Stream'.WSeq.think s) = Stream'.WSeq.think (Stream'.WSeq.tail s)

@[simp]

theorem Stream'.WSeq.dropn_nil {α : Type u} (n : ℕ) : Stream'.WSeq.drop Stream'.WSeq.nil n = Stream'.WSeq.nil

@[simp]

theorem Stream'.WSeq.dropn_cons {α : Type u} (a : α) (s : Stream'.WSeq α) (n : ℕ) : Stream'.WSeq.drop (Stream'.WSeq.cons a s) (n + 1) = Stream'.WSeq.drop s n

@[simp]

theorem Stream'.WSeq.dropn_think {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Stream'.WSeq.drop (Stream'.WSeq.think s) n = Stream'.WSeq.think (Stream'.WSeq.drop s n)

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

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

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

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

@[simp]

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

@[simp]

theorem Stream'.WSeq.join_think {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) : Stream'.WSeq.join (Stream'.WSeq.think S) = Stream'.WSeq.think (Stream'.WSeq.join S)

@[simp]

theorem Stream'.WSeq.join_cons {α : Type u} (s : Stream'.WSeq α) (S : Stream'.WSeq (Stream'.WSeq α)) : Stream'.WSeq.join (Stream'.WSeq.cons s S) = Stream'.WSeq.think (Stream'.WSeq.append s (Stream'.WSeq.join S))

@[simp]

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

@[simp]

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

@[simp]

theorem Stream'.WSeq.think_append {α : Type u} (s : Stream'.WSeq α) (t : Stream'.WSeq α) : Stream'.WSeq.append (Stream'.WSeq.think s) t = Stream'.WSeq.think (Stream'.WSeq.append s t)

@[simp]

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

@[simp]

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

def Stream'.WSeq.tail.aux {α : Type u} : Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))

auxiliary definition of tail over weak sequences

theorem Stream'.WSeq.destruct_tail {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.destruct (Stream'.WSeq.tail s) = Stream'.WSeq.destruct s >>= Stream'.WSeq.tail.aux

def Stream'.WSeq.drop.aux {α : Type u} : ℕ → Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))

auxiliary definition of drop over weak sequences

Equations

• Stream'.WSeq.drop.aux 0 = Computation.pure
• Stream'.WSeq.drop.aux (Nat.succ n) = fun a => Stream'.WSeq.tail.aux a >>= Stream'.WSeq.drop.aux n

theorem Stream'.WSeq.drop.aux_none {α : Type u} (n : ℕ) : Stream'.WSeq.drop.aux n none = Computation.pure none

theorem Stream'.WSeq.destruct_dropn {α : Type u} (s : Stream'.WSeq α) (n : ℕ) : Stream'.WSeq.destruct (Stream'.WSeq.drop s n) = Stream'.WSeq.destruct s >>= Stream'.WSeq.drop.aux n

theorem Stream'.WSeq.head_terminates_of_head_tail_terminates {α : Type u} (s : Stream'.WSeq α) [T : Computation.Terminates (Stream'.WSeq.head (Stream'.WSeq.tail s))] : Computation.Terminates (Stream'.WSeq.head s)

theorem Stream'.WSeq.destruct_some_of_destruct_tail_some {α : Type u} {s : Stream'.WSeq α} {a : α × Stream'.WSeq α} (h : some a ∈ Stream'.WSeq.destruct (Stream'.WSeq.tail s)) : ∃ a', some a' ∈ Stream'.WSeq.destruct s

theorem Stream'.WSeq.head_some_of_head_tail_some {α : Type u} {s : Stream'.WSeq α} {a : α} (h : some a ∈ Stream'.WSeq.head (Stream'.WSeq.tail s)) : ∃ a', some a' ∈ Stream'.WSeq.head s

theorem Stream'.WSeq.head_some_of_get?_some {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ} (h : some a ∈ Stream'.WSeq.get? s n) : ∃ a', some a' ∈ Stream'.WSeq.head s

instance Stream'.WSeq.productive_tail {α : Type u} (s : Stream'.WSeq α) [Stream'.WSeq.Productive s] : Stream'.WSeq.Productive (Stream'.WSeq.tail s)

instance Stream'.WSeq.productive_dropn {α : Type u} (s : Stream'.WSeq α) [Stream'.WSeq.Productive s] (n : ℕ) : Stream'.WSeq.Productive (Stream'.WSeq.drop s n)

def Stream'.WSeq.toSeq {α : Type u} (s : Stream'.WSeq α) [Stream'.WSeq.Productive s] : Stream'.Seq α

Given a productive weak sequence, we can collapse all the thinks to produce a sequence.

theorem Stream'.WSeq.get?_terminates_le {α : Type u} {s : Stream'.WSeq α} {m : ℕ} {n : ℕ} (h : m ≤ n) : Computation.Terminates (Stream'.WSeq.get? s n) → Computation.Terminates (Stream'.WSeq.get? s m)

theorem Stream'.WSeq.head_terminates_of_get?_terminates {α : Type u} {s : Stream'.WSeq α} {n : ℕ} : Computation.Terminates (Stream'.WSeq.get? s n) → Computation.Terminates (Stream'.WSeq.head s)

theorem Stream'.WSeq.destruct_terminates_of_get?_terminates {α : Type u} {s : Stream'.WSeq α} {n : ℕ} (T : Computation.Terminates (Stream'.WSeq.get? s n)) : Computation.Terminates (Stream'.WSeq.destruct s)

theorem Stream'.WSeq.mem_rec_on {α : Type u} {C : Stream'.WSeq α → Prop} {a : α} {s : Stream'.WSeq α} (M : a ∈ s) (h1 : (b : α) → (s' : Stream'.WSeq α) → a = b ∨ C s' → C (Stream'.WSeq.cons b s')) (h2 : (s : Stream'.WSeq α) → C s → C (Stream'.WSeq.think s)) : C s

@[simp]

theorem Stream'.WSeq.mem_think {α : Type u} (s : Stream'.WSeq α) (a : α) : a ∈ Stream'.WSeq.think s ↔ a ∈ s

theorem Stream'.WSeq.eq_or_mem_iff_mem {α : Type u} {s : Stream'.WSeq α} {a : α} {a' : α} {s' : Stream'.WSeq α} : some (a', s') ∈ Stream'.WSeq.destruct s → (a ∈ s ↔ a = a' ∨ a ∈ s')

@[simp]

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

theorem Stream'.WSeq.mem_cons_of_mem {α : Type u} {s : Stream'.WSeq α} (b : α) {a : α} (h : a ∈ s) : a ∈ Stream'.WSeq.cons b s

theorem Stream'.WSeq.mem_cons {α : Type u} (s : Stream'.WSeq α) (a : α) : a ∈ Stream'.WSeq.cons a s

theorem Stream'.WSeq.mem_of_mem_tail {α : Type u} {s : Stream'.WSeq α} {a : α} : a ∈ Stream'.WSeq.tail s → a ∈ s

theorem Stream'.WSeq.mem_of_mem_dropn {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ} : a ∈ Stream'.WSeq.drop s n → a ∈ s

theorem Stream'.WSeq.get?_mem {α : Type u} {s : Stream'.WSeq α} {a : α} {n : ℕ} : some a ∈ Stream'.WSeq.get? s n → a ∈ s

theorem Stream'.WSeq.exists_get?_of_mem {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a ∈ s) : ∃ n, some a ∈ Stream'.WSeq.get? s n

theorem Stream'.WSeq.exists_dropn_of_mem {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a ∈ s) : ∃ n s', some (a, s') ∈ Stream'.WSeq.destruct (Stream'.WSeq.drop s n)

theorem Stream'.WSeq.liftRel_dropn_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β} (H : Stream'.WSeq.LiftRel R s t) (n : ℕ) : Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) (Stream'.WSeq.destruct (Stream'.WSeq.drop s n)) (Stream'.WSeq.destruct (Stream'.WSeq.drop t n))

theorem Stream'.WSeq.exists_of_liftRel_left {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β} (H : Stream'.WSeq.LiftRel R s t) {a : α} (h : a ∈ s) : ∃ b, b ∈ t ∧ R a b

theorem Stream'.WSeq.exists_of_liftRel_right {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β} (H : Stream'.WSeq.LiftRel R s t) {b : β} (h : b ∈ t) : ∃ a, a ∈ s ∧ R a b

theorem Stream'.WSeq.head_terminates_of_mem {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a ∈ s) : Computation.Terminates (Stream'.WSeq.head s)

theorem Stream'.WSeq.of_mem_append {α : Type u} {s₁ : Stream'.WSeq α} {s₂ : Stream'.WSeq α} {a : α} : a ∈ Stream'.WSeq.append s₁ s₂ → a ∈ s₁ ∨ a ∈ s₂

theorem Stream'.WSeq.mem_append_left {α : Type u} {s₁ : Stream'.WSeq α} {s₂ : Stream'.WSeq α} {a : α} : a ∈ s₁ → a ∈ Stream'.WSeq.append s₁ s₂

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

@[simp]

theorem Stream'.WSeq.liftRel_nil {α : Type u} {β : Type v} (R : α → β → Prop) : Stream'.WSeq.LiftRel R Stream'.WSeq.nil Stream'.WSeq.nil

@[simp]

theorem Stream'.WSeq.liftRel_cons {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β) (s : Stream'.WSeq α) (t : Stream'.WSeq β) : Stream'.WSeq.LiftRel R (Stream'.WSeq.cons a s) (Stream'.WSeq.cons b t) ↔ R a b ∧ Stream'.WSeq.LiftRel R s t

@[simp]

theorem Stream'.WSeq.liftRel_think_left {α : Type u} {β : Type v} (R : α → β → Prop) (s : Stream'.WSeq α) (t : Stream'.WSeq β) : Stream'.WSeq.LiftRel R (Stream'.WSeq.think s) t ↔ Stream'.WSeq.LiftRel R s t

@[simp]

theorem Stream'.WSeq.liftRel_think_right {α : Type u} {β : Type v} (R : α → β → Prop) (s : Stream'.WSeq α) (t : Stream'.WSeq β) : Stream'.WSeq.LiftRel R s (Stream'.WSeq.think t) ↔ Stream'.WSeq.LiftRel R s t

theorem Stream'.WSeq.cons_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (a : α) (h : s ~ʷ t) : Stream'.WSeq.cons a s ~ʷ Stream'.WSeq.cons a t

theorem Stream'.WSeq.think_equiv {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.think s ~ʷ s

theorem Stream'.WSeq.think_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) : Stream'.WSeq.think s ~ʷ Stream'.WSeq.think t

theorem Stream'.WSeq.head_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} : s ~ʷ t → Computation.Equiv (Stream'.WSeq.head s) (Stream'.WSeq.head t)

theorem Stream'.WSeq.flatten_equiv {α : Type u} {c : Computation (Stream'.WSeq α)} {s : Stream'.WSeq α} (h : s ∈ c) : Stream'.WSeq.flatten c ~ʷ s

theorem Stream'.WSeq.liftRel_flatten {α : Type u} {β : Type v} {R : α → β → Prop} {c1 : Computation (Stream'.WSeq α)} {c2 : Computation (Stream'.WSeq β)} (h : Computation.LiftRel (Stream'.WSeq.LiftRel R) c1 c2) : Stream'.WSeq.LiftRel R (Stream'.WSeq.flatten c1) (Stream'.WSeq.flatten c2)

theorem Stream'.WSeq.flatten_congr {α : Type u} {c1 : Computation (Stream'.WSeq α)} {c2 : Computation (Stream'.WSeq α)} : Computation.LiftRel Stream'.WSeq.Equiv c1 c2 → Stream'.WSeq.flatten c1 ~ʷ Stream'.WSeq.flatten c2

theorem Stream'.WSeq.tail_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) : Stream'.WSeq.tail s ~ʷ Stream'.WSeq.tail t

theorem Stream'.WSeq.dropn_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) (n : ℕ) : Stream'.WSeq.drop s n ~ʷ Stream'.WSeq.drop t n

theorem Stream'.WSeq.get?_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) (n : ℕ) : Computation.Equiv (Stream'.WSeq.get? s n) (Stream'.WSeq.get? t n)

theorem Stream'.WSeq.mem_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) (a : α) : a ∈ s ↔ a ∈ t

theorem Stream'.WSeq.productive_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) : Stream'.WSeq.Productive s ↔ Stream'.WSeq.Productive t

theorem Stream'.WSeq.Equiv.ext {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : ∀ (n : ℕ), Computation.Equiv (Stream'.WSeq.get? s n) (Stream'.WSeq.get? t n)) : s ~ʷ t

theorem Stream'.WSeq.length_eq_map {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.length s = Computation.map List.length (Stream'.WSeq.toList s)

@[simp]

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

@[simp]

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

@[simp]

theorem Stream'.WSeq.toList'_nil {α : Type u} (l : List α) : Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl (List.reverse l) | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.nil) = Computation.pure (List.reverse l)

@[simp]

theorem Stream'.WSeq.toList'_cons {α : Type u} (l : List α) (s : Stream'.WSeq α) (a : α) : Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl (List.reverse l) | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.cons a s) = Computation.think (Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl (List.reverse l) | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (a :: l, s))

@[simp]

theorem Stream'.WSeq.toList'_think {α : Type u} (l : List α) (s : Stream'.WSeq α) : Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl (List.reverse l) | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.think s) = Computation.think (Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl (List.reverse l) | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s))

theorem Stream'.WSeq.toList'_map {α : Type u} (l : List α) (s : Stream'.WSeq α) : Computation.corec (fun x => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl (List.reverse l) | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s) = (fun x x_1 => x ++ x_1) (List.reverse l) <$> Stream'.WSeq.toList s

@[simp]

theorem Stream'.WSeq.toList_cons {α : Type u} (a : α) (s : Stream'.WSeq α) : Stream'.WSeq.toList (Stream'.WSeq.cons a s) = Computation.think (List.cons a <$> Stream'.WSeq.toList s)

@[simp]

theorem Stream'.WSeq.toList_nil {α : Type u} : Stream'.WSeq.toList Stream'.WSeq.nil = Computation.pure []

theorem Stream'.WSeq.toList_ofList {α : Type u} (l : List α) : l ∈ Stream'.WSeq.toList ↑l

@[simp]

theorem Stream'.WSeq.destruct_ofSeq {α : Type u} (s : Stream'.Seq α) : Stream'.WSeq.destruct ↑s = Computation.pure (Option.map (fun a => (a, ↑(Stream'.Seq.tail s))) (Stream'.Seq.head s))

@[simp]

theorem Stream'.WSeq.head_ofSeq {α : Type u} (s : Stream'.Seq α) : Stream'.WSeq.head ↑s = Computation.pure (Stream'.Seq.head s)

@[simp]

theorem Stream'.WSeq.tail_ofSeq {α : Type u} (s : Stream'.Seq α) : Stream'.WSeq.tail ↑s = ↑(Stream'.Seq.tail s)

@[simp]

theorem Stream'.WSeq.dropn_ofSeq {α : Type u} (s : Stream'.Seq α) (n : ℕ) : Stream'.WSeq.drop (↑s) n = ↑(Stream'.Seq.drop s n)

theorem Stream'.WSeq.get?_ofSeq {α : Type u} (s : Stream'.Seq α) (n : ℕ) : Stream'.WSeq.get? (↑s) n = Computation.pure (Stream'.Seq.get? s n)

instance Stream'.WSeq.productive_ofSeq {α : Type u} (s : Stream'.Seq α) : Stream'.WSeq.Productive ↑s

theorem Stream'.WSeq.toSeq_ofSeq {α : Type u} (s : Stream'.Seq α) : Stream'.WSeq.toSeq ↑s = s

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

The monadic return a is a singleton list containing a.

@[simp]

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

@[simp]

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

@[simp]

theorem Stream'.WSeq.map_think {α : Type u} {β : Type v} (f : α → β) (s : Stream'.WSeq α) : Stream'.WSeq.map f (Stream'.WSeq.think s) = Stream'.WSeq.think (Stream'.WSeq.map f s)

@[simp]

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

@[simp]

theorem Stream'.WSeq.map_ret {α : Type u} {β : Type v} (f : α → β) (a : α) : Stream'.WSeq.map f (Stream'.WSeq.ret a) = Stream'.WSeq.ret (f a)

@[simp]

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

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

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

theorem Stream'.WSeq.exists_of_mem_join {α : Type u} {a : α} {S : Stream'.WSeq (Stream'.WSeq α)} : a ∈ Stream'.WSeq.join S → ∃ s, s ∈ S ∧ a ∈ s

theorem Stream'.WSeq.exists_of_mem_bind {α : Type u} {β : Type v} {s : Stream'.WSeq α} {f : α → Stream'.WSeq β} {b : β} (h : b ∈ Stream'.WSeq.bind s f) : ∃ a, a ∈ s ∧ b ∈ f a

theorem Stream'.WSeq.destruct_map {α : Type u} {β : Type v} (f : α → β) (s : Stream'.WSeq α) : Stream'.WSeq.destruct (Stream'.WSeq.map f s) = Computation.map (Option.map (Prod.map f (Stream'.WSeq.map f))) (Stream'.WSeq.destruct s)

theorem Stream'.WSeq.liftRel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} {f1 : α → γ} {f2 : β → δ} (h1 : Stream'.WSeq.LiftRel R s1 s2) (h2 : {a : α} → {b : β} → R a b → S (f1 a) (f2 b)) : Stream'.WSeq.LiftRel S (Stream'.WSeq.map f1 s1) (Stream'.WSeq.map f2 s2)

theorem Stream'.WSeq.map_congr {α : Type u} {β : Type v} (f : α → β) {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s ~ʷ t) : Stream'.WSeq.map f s ~ʷ Stream'.WSeq.map f t

def Stream'.WSeq.destruct_append.aux {α : Type u} (t : Stream'.WSeq α) : Option (α × Stream'.WSeq α) → Computation (Option (α × Stream'.WSeq α))

auxiliary definition of destruct_append over weak sequences

theorem Stream'.WSeq.destruct_append {α : Type u} (s : Stream'.WSeq α) (t : Stream'.WSeq α) : Stream'.WSeq.destruct (Stream'.WSeq.append s t) = Computation.bind (Stream'.WSeq.destruct s) (Stream'.WSeq.destruct_append.aux t)

def Stream'.WSeq.destruct_join.aux {α : Type u} : Option (Stream'.WSeq α × Stream'.WSeq (Stream'.WSeq α)) → Computation (Option (α × Stream'.WSeq α))

auxiliary definition of destruct_join over weak sequences

theorem Stream'.WSeq.destruct_join {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) : Stream'.WSeq.destruct (Stream'.WSeq.join S) = Computation.bind (Stream'.WSeq.destruct S) Stream'.WSeq.destruct_join.aux

theorem Stream'.WSeq.liftRel_append {α : Type u} {β : Type v} (R : α → β → Prop) {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq α} {t1 : Stream'.WSeq β} {t2 : Stream'.WSeq β} (h1 : Stream'.WSeq.LiftRel R s1 t1) (h2 : Stream'.WSeq.LiftRel R s2 t2) : Stream'.WSeq.LiftRel R (Stream'.WSeq.append s1 s2) (Stream'.WSeq.append t1 t2)

theorem Stream'.WSeq.liftRel_join.lem {α : Type u} {β : Type v} (R : α → β → Prop) {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq β)} {U : Stream'.WSeq α → Stream'.WSeq β → Prop} (ST : Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) (HU : (s1 : Stream'.WSeq α) → (s2 : Stream'.WSeq β) → (∃ s t S T, s1 = Stream'.WSeq.append s (Stream'.WSeq.join S) ∧ s2 = Stream'.WSeq.append t (Stream'.WSeq.join T) ∧ Stream'.WSeq.LiftRel R s t ∧ Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) → U s1 s2) {a : Option (α × Stream'.WSeq α)} (ma : a ∈ Stream'.WSeq.destruct (Stream'.WSeq.join S)) : ∃ b, b ∈ Stream'.WSeq.destruct (Stream'.WSeq.join T) ∧ Stream'.WSeq.LiftRelO R U a b

theorem Stream'.WSeq.liftRel_join {α : Type u} {β : Type v} (R : α → β → Prop) {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq β)} (h : Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) : Stream'.WSeq.LiftRel R (Stream'.WSeq.join S) (Stream'.WSeq.join T)

theorem Stream'.WSeq.join_congr {α : Type u} {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq α)} (h : Stream'.WSeq.LiftRel Stream'.WSeq.Equiv S T) : Stream'.WSeq.join S ~ʷ Stream'.WSeq.join T

theorem Stream'.WSeq.liftRel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} {f1 : α → Stream'.WSeq γ} {f2 : β → Stream'.WSeq δ} (h1 : Stream'.WSeq.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → Stream'.WSeq.LiftRel S (f1 a) (f2 b)) : Stream'.WSeq.LiftRel S (Stream'.WSeq.bind s1 f1) (Stream'.WSeq.bind s2 f2)

theorem Stream'.WSeq.bind_congr {α : Type u} {β : Type v} {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq α} {f1 : α → Stream'.WSeq β} {f2 : α → Stream'.WSeq β} (h1 : s1 ~ʷ s2) (h2 : ∀ (a : α), f1 a ~ʷ f2 a) : Stream'.WSeq.bind s1 f1 ~ʷ Stream'.WSeq.bind s2 f2

@[simp]

theorem Stream'.WSeq.join_ret {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.join (Stream'.WSeq.ret s) ~ʷ s

@[simp]

theorem Stream'.WSeq.join_map_ret {α : Type u} (s : Stream'.WSeq α) : Stream'.WSeq.join (Stream'.WSeq.map Stream'.WSeq.ret s) ~ʷ s

@[simp]

theorem Stream'.WSeq.join_append {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) (T : Stream'.WSeq (Stream'.WSeq α)) : Stream'.WSeq.join (Stream'.WSeq.append S T) ~ʷ Stream'.WSeq.append (Stream'.WSeq.join S) (Stream'.WSeq.join T)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem Stream'.WSeq.join_join {α : Type u} (SS : Stream'.WSeq (Stream'.WSeq (Stream'.WSeq α))) : Stream'.WSeq.join (Stream'.WSeq.join SS) ~ʷ Stream'.WSeq.join (Stream'.WSeq.map Stream'.WSeq.join SS)

@[simp]

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

instance Stream'.WSeq.monad : Monad Stream'.WSeq