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

• Stream'.WSeq α = Stream'.Seq (Option α)

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

Turn a sequence into a weak sequence

Equations

• Stream'.WSeq.ofSeq = (fun (x1 : α → Option α) (x2 : Stream'.Seq α) => x1 <$> x2) some

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

• Stream'.WSeq.coeSeq = { coe := Stream'.WSeq.ofSeq }

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

Equations

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

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

Equations

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

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

The empty weak sequence

Equations

• Stream'.WSeq.nil = Stream'.Seq.nil

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

Equations

• Stream'.WSeq.inhabited = { default := Stream'.WSeq.nil }

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

Prepend an element to a weak sequence

Equations

• Stream'.WSeq.cons a = Stream'.Seq.cons (some a)

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

Compute for one tick, without producing any elements

Equations

• Stream'.WSeq.think = Stream'.Seq.cons none

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

• s.recOn h1 h2 h3 = Stream'.Seq.recOn s h1 fun (o : Option α) => Option.recOn (motive := fun (x : Option α) => (s : Stream'.Seq (Option α)) → C (Stream'.Seq.cons x s)) o h3 h2

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

membership for weak sequences

Equations

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

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

Equations

• Stream'.WSeq.membership = { mem := Stream'.WSeq.Mem }

theorem Stream'.WSeq.not_mem_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.

Equations

• s.head = Computation.map (fun (x : Option (α × Stream'.WSeq α)) => Prod.fst <$> x) s.destruct

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

• s.tail = Stream'.WSeq.flatten ((fun (o : Option (α × Stream'.WSeq α)) => Option.recOn o Stream'.WSeq.nil Prod.snd) <$> s.destruct)

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

drop the first n elements from s.

Equations

• s.drop 0 = s
• s.drop n.succ = (s.drop n).tail

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

Get the nth element of s.

Equations

• s.get? n = (s.drop n).head

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

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

• Stream'.WSeq.append = Stream'.Seq.append

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

• S.join = ((fun (o : Option (Stream'.WSeq α)) => match o with | none => Stream'.Seq1.ret none | some s => (none, s)) <$> S).join

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

Map a function over a weak sequence

Equations

• Stream'.WSeq.map f = Stream'.Seq.map (Option.map f)

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

The monadic return a is a singleton list containing a.

Equations

• Stream'.WSeq.ret a = ↑[a]

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

Monadic bind operator for weak sequences

Equations

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

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.

Equations

• Stream'.WSeq.monad = Monad.mk

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

Equations

• Stream'.WSeq.tail.aux none = Computation.pure none
• Stream'.WSeq.tail.aux (some (fst, s)) = s.destruct

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

Equations

• Stream'.WSeq.drop.aux 0 = Computation.pure
• Stream'.WSeq.drop.aux n.succ = fun (a : Option (α × Stream'.WSeq α)) => Stream'.WSeq.tail.aux a >>= Stream'.WSeq.drop.aux n

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 : α), 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 : 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 α) : (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

Equations

• Stream'.WSeq.destruct_append.aux t none = t.destruct
• Stream'.WSeq.destruct_append.aux t (some (fst, s)) = Computation.pure (some (fst, s.append t))

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

Equations

• Stream'.WSeq.destruct_join.aux none = Computation.pure none
• Stream'.WSeq.destruct_join.aux (some (s, S)) = (s.append S.join).destruct.think

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