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} : Seq α → WSeq α

Turn a sequence into a weak sequence

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

Turn a list into a weak sequence

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

Turn a stream into a weak sequence

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

The empty weak sequence

@[implicit_reducible]

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

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

Prepend an element to a weak sequence

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

Compute for one tick, without producing any elements

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.

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

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

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

membership for weak sequences

@[implicit_reducible]

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

theorem Stream'.WSeq.notMem_nil {α : Type u} (a : α) : a ∉ nil

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

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

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

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

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.

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

drop the first n elements from s.

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

Get the nth element of s.

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

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

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

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

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

Map a function over a weak sequence

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

The monadic return a is a singleton list containing a.

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

Monadic bind operator for weak sequences

@[implicit_reducible]

instance Stream'.WSeq.monad : Monad WSeq

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[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 α) : s.think.tail = s.tail.think

@[simp]

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

@[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]

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

@[simp]

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

@[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 α) : nil.append s = s

@[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 α) : s.think.append t = (s.append t).think

@[simp]

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

@[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

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

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

auxiliary definition of drop over weak sequences

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

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

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

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.head_terminates_of_get?_terminates {α : Type u} {s : WSeq α} {n : ℕ} : (s.get? n).Terminates → s.head.Terminates

theorem Stream'.WSeq.destruct_terminates_of_get?_terminates {α : Type u} {s : WSeq α} {n : ℕ} (T : (s.get? n).Terminates) : s.destruct.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 s → C 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.tail → a ∈ s

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

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

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

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

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

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 ∈ 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 α) : (cons a s).toList = (List.cons a <$> s.toList).think

@[simp]

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

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 α) : (↑s).head = Computation.pure s.head

@[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 : α → β) : map f nil = nil

@[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 ∈ s → f a ∈ map f s

theorem Stream'.WSeq.exists_of_mem_join {α : Type u} {a : α} {S : WSeq (WSeq α)} : a ∈ S.join → ∃ 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 ∈ s, b ∈ f a

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

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

auxiliary definition of destruct_append over weak sequences

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

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

auxiliary definition of destruct_join over weak sequences

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

@[simp]

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