Documentation

Mathlib.Data.WSeq.Basic

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.

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

Turn a sequence into a weak sequence

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

Turn a list into a weak sequence

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

Turn a stream into a weak sequence

Equations
  • l = l
instance Stream'.WSeq.coeSeq {α : Type u} :
Coe (Seq α) (WSeq α)
Equations
def Stream'.WSeq.nil {α : Type u} :
WSeq α

The empty weak sequence

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

Prepend an element to a weak sequence

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

Compute for one tick, without producing any elements

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

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

Equations
  • One or more equations did not get rendered due to their size.
def Stream'.WSeq.recOn {α : Type u} {C : WSeq αSort v} (s : WSeq α) (h1 : C nil) (h2 : (x : α) → (s : WSeq α) → C (cons x s)) (h3 : (s : WSeq α) → C s.think) :
C s

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

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

membership for weak sequences

Equations
theorem Stream'.WSeq.notMem_nil {α : Type u} (a : α) :
@[deprecated Stream'.WSeq.notMem_nil (since := "2025-05-23")]
theorem Stream'.WSeq.not_mem_nil {α : Type u} (a : α) :

Alias of Stream'.WSeq.notMem_nil.

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

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

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

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

Equations
  • One or more equations did not get rendered due to their size.
def Stream'.WSeq.tail {α : Type u} (s : WSeq α) :
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.

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

drop the first n elements from s.

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

Get the nth element of s.

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

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

Equations
  • One or more equations did not get rendered due to their size.
def Stream'.WSeq.append {α : Type u} :
WSeq αWSeq αWSeq α

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

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

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

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

Map a function over a weak sequence

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

The monadic return a is a singleton list containing a.

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

Monadic bind operator for weak sequences

Equations

Unfortunately, WSeq is not a lawful monad, because it does not satisfy the monad laws exactly, only up to sequence equivalence. Furthermore, even quotienting by the equivalence is not sufficient, because the join operation involves lists of quotient elements, with a lifted equivalence relation, and pure quotients cannot handle this type of construction.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Stream'.WSeq.destruct_cons {α : Type u} (a : α) (s : WSeq α) :
@[simp]
@[simp]
theorem Stream'.WSeq.seq_destruct_cons {α : Type u} (a : α) (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.head_cons {α : Type u} (a : α) (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.head_think {α : Type u} (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.flatten_pure {α : Type u} (s : WSeq α) :
@[simp]
@[simp]
@[simp]
theorem Stream'.WSeq.tail_cons {α : Type u} (a : α) (s : WSeq α) :
(cons a s).tail = s
@[simp]
theorem Stream'.WSeq.tail_think {α : Type u} (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.dropn_nil {α : Type u} (n : ) :
@[simp]
theorem Stream'.WSeq.dropn_cons {α : Type u} (a : α) (s : WSeq α) (n : ) :
(cons a s).drop (n + 1) = s.drop n
@[simp]
theorem Stream'.WSeq.dropn_think {α : Type u} (s : WSeq α) (n : ) :
s.think.drop n = (s.drop n).think
theorem Stream'.WSeq.dropn_add {α : Type u} (s : WSeq α) (m n : ) :
s.drop (m + n) = (s.drop m).drop n
theorem Stream'.WSeq.dropn_tail {α : Type u} (s : WSeq α) (n : ) :
s.tail.drop n = s.drop (n + 1)
theorem Stream'.WSeq.get?_add {α : Type u} (s : WSeq α) (m n : ) :
s.get? (m + n) = (s.drop m).get? n
theorem Stream'.WSeq.get?_tail {α : Type u} (s : WSeq α) (n : ) :
s.tail.get? n = s.get? (n + 1)
@[simp]
@[simp]
theorem Stream'.WSeq.join_think {α : Type u} (S : WSeq (WSeq α)) :
@[simp]
theorem Stream'.WSeq.join_cons {α : Type u} (s : WSeq α) (S : WSeq (WSeq α)) :
(cons s S).join = (s.append S.join).think
@[simp]
theorem Stream'.WSeq.nil_append {α : Type u} (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.cons_append {α : Type u} (a : α) (s t : WSeq α) :
(cons a s).append t = cons a (s.append t)
@[simp]
theorem Stream'.WSeq.think_append {α : Type u} (s t : WSeq α) :
@[simp]
theorem Stream'.WSeq.append_nil {α : Type u} (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.append_assoc {α : Type u} (s t u : WSeq α) :
(s.append t).append u = s.append (t.append u)
def Stream'.WSeq.tail.aux {α : Type u} :
Option (α × WSeq α)Computation (Option (α × WSeq α))

auxiliary definition of tail over weak sequences

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

auxiliary definition of drop over weak sequences

Equations
theorem Stream'.WSeq.destruct_dropn {α : Type u} (s : WSeq α) (n : ) :
theorem Stream'.WSeq.destruct_some_of_destruct_tail_some {α : Type u} {s : WSeq α} {a : α × WSeq α} (h : some a s.tail.destruct) :
(a' : α × WSeq α), some a' s.destruct
theorem Stream'.WSeq.head_some_of_head_tail_some {α : Type u} {s : WSeq α} {a : α} (h : some a s.tail.head) :
(a' : α), some a' s.head
theorem Stream'.WSeq.head_some_of_get?_some {α : Type u} {s : WSeq α} {a : α} {n : } (h : some a s.get? n) :
(a' : α), some a' s.head
theorem Stream'.WSeq.get?_terminates_le {α : Type u} {s : WSeq α} {m n : } (h : m n) :
(s.get? n).Terminates(s.get? m).Terminates
theorem Stream'.WSeq.mem_rec_on {α : Type u} {C : WSeq αProp} {a : α} {s : WSeq α} (M : a s) (h1 : ∀ (b : α) (s' : WSeq α), a = b C s'C (cons b s')) (h2 : ∀ (s : WSeq α), C sC s.think) :
C s
@[simp]
theorem Stream'.WSeq.mem_think {α : Type u} (s : WSeq α) (a : α) :
a s.think a s
theorem Stream'.WSeq.eq_or_mem_iff_mem {α : Type u} {s : WSeq α} {a a' : α} {s' : WSeq α} :
some (a', s') s.destruct → (a s a = a' a s')
@[simp]
theorem Stream'.WSeq.mem_cons_iff {α : Type u} (s : WSeq α) (b : α) {a : α} :
a cons b s a = b a s
theorem Stream'.WSeq.mem_cons_of_mem {α : Type u} {s : WSeq α} (b : α) {a : α} (h : a s) :
a cons b s
theorem Stream'.WSeq.mem_cons {α : Type u} (s : WSeq α) (a : α) :
a cons a s
theorem Stream'.WSeq.mem_of_mem_tail {α : Type u} {s : WSeq α} {a : α} :
a s.taila s
theorem Stream'.WSeq.mem_of_mem_dropn {α : Type u} {s : WSeq α} {a : α} {n : } :
a s.drop na s
theorem Stream'.WSeq.get?_mem {α : Type u} {s : WSeq α} {a : α} {n : } :
some a s.get? na s
theorem Stream'.WSeq.exists_get?_of_mem {α : Type u} {s : WSeq α} {a : α} (h : a s) :
theorem Stream'.WSeq.exists_dropn_of_mem {α : Type u} {s : WSeq α} {a : α} (h : a s) :
theorem Stream'.WSeq.head_terminates_of_mem {α : Type u} {s : WSeq α} {a : α} (h : a s) :
theorem Stream'.WSeq.of_mem_append {α : Type u} {s₁ s₂ : WSeq α} {a : α} :
a s₁.append s₂a s₁ a s₂
theorem Stream'.WSeq.mem_append_left {α : Type u} {s₁ s₂ : WSeq α} {a : α} :
a s₁a s₁.append s₂
theorem Stream'.WSeq.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : WSeq α} :
b map f s (a : α), a s f a = b
@[simp]
theorem Stream'.WSeq.ofList_nil {α : Type u} :
[] = nil
@[simp]
theorem Stream'.WSeq.ofList_cons {α : Type u} (a : α) (l : List α) :
↑(a :: l) = cons a l
@[simp]
theorem Stream'.WSeq.toList'_nil {α : Type u} (l : List α) :
Computation.corec (fun (x : List α × WSeq α) => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, nil) = Computation.pure l.reverse
@[simp]
theorem Stream'.WSeq.toList'_cons {α : Type u} (l : List α) (s : WSeq α) (a : α) :
Computation.corec (fun (x : List α × WSeq α) => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, cons a s) = (Computation.corec (fun (x : List α × WSeq α) => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (a :: l, s)).think
@[simp]
theorem Stream'.WSeq.toList'_think {α : Type u} (l : List α) (s : WSeq α) :
Computation.corec (fun (x : List α × WSeq α) => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s.think) = (Computation.corec (fun (x : List α × WSeq α) => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s)).think
theorem Stream'.WSeq.toList'_map {α : Type u} (l : List α) (s : WSeq α) :
Computation.corec (fun (x : List α × WSeq α) => match x with | (l, s) => match Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s) = (fun (x : List α) => l.reverse ++ x) <$> s.toList
@[simp]
theorem Stream'.WSeq.toList_cons {α : Type u} (a : α) (s : WSeq α) :
theorem Stream'.WSeq.toList_ofList {α : Type u} (l : List α) :
l (↑l).toList
@[simp]
theorem Stream'.WSeq.destruct_ofSeq {α : Type u} (s : Seq α) :
(↑s).destruct = Computation.pure (Option.map (fun (a : α) => (a, s.tail)) s.head)
@[simp]
theorem Stream'.WSeq.head_ofSeq {α : Type u} (s : Seq α) :
@[simp]
theorem Stream'.WSeq.tail_ofSeq {α : Type u} (s : Seq α) :
(↑s).tail = s.tail
@[simp]
theorem Stream'.WSeq.dropn_ofSeq {α : Type u} (s : Seq α) (n : ) :
(↑s).drop n = (s.drop n)
theorem Stream'.WSeq.get?_ofSeq {α : Type u} (s : Seq α) (n : ) :
(↑s).get? n = Computation.pure (s.get? n)
@[simp]
theorem Stream'.WSeq.map_nil {α : Type u} {β : Type v} (f : αβ) :
@[simp]
theorem Stream'.WSeq.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (s : WSeq α) :
map f (cons a s) = cons (f a) (map f s)
@[simp]
theorem Stream'.WSeq.map_think {α : Type u} {β : Type v} (f : αβ) (s : WSeq α) :
map f s.think = (map f s).think
@[simp]
theorem Stream'.WSeq.map_id {α : Type u} (s : WSeq α) :
map id s = s
@[simp]
theorem Stream'.WSeq.map_ret {α : Type u} {β : Type v} (f : αβ) (a : α) :
map f (ret a) = ret (f a)
@[simp]
theorem Stream'.WSeq.map_append {α : Type u} {β : Type v} (f : αβ) (s t : WSeq α) :
map f (s.append t) = (map f s).append (map f t)
theorem Stream'.WSeq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : WSeq α) :
map (g f) s = map g (map f s)
theorem Stream'.WSeq.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : WSeq α} :
a sf a map f s
theorem Stream'.WSeq.exists_of_mem_join {α : Type u} {a : α} {S : WSeq (WSeq α)} :
a S.join (s : WSeq α), s S a s
theorem Stream'.WSeq.exists_of_mem_bind {α : Type u} {β : Type v} {s : WSeq α} {f : αWSeq β} {b : β} (h : b s.bind f) :
(a : α), a s b f a
theorem Stream'.WSeq.destruct_map {α : Type u} {β : Type v} (f : αβ) (s : WSeq α) :
@[simp]
theorem Stream'.WSeq.map_join {α : Type u} {β : Type v} (f : αβ) (S : WSeq (WSeq α)) :
map f S.join = (map (map f) S).join