mathlib3 documentation

data.seq.wseq

source
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
Instances for stream.wseq
source
def stream.wseq.of_seq {α : Type u} :
stream.seq α → stream.wseq α

Turn a sequence into a weak sequence

Equations
Instances for stream.wseq.of_seq
source
def stream.wseq.of_list {α : Type u} (l : list α) :
stream.wseq α

Turn a list into a weak sequence

Equations
source
def stream.wseq.of_stream {α : Type u} (l : stream α) :
stream.wseq α

Turn a stream into a weak sequence

Equations
source
@[protected, instance]
def stream.wseq.coe_seq {α : Type u} :
has_coe (stream.seq α) (stream.wseq α)
Equations
source
@[protected, instance]
def stream.wseq.coe_list {α : Type u} :
has_coe (list α) (stream.wseq α)
Equations
source
@[protected, instance]
def stream.wseq.coe_stream {α : Type u} :
has_coe (stream α) (stream.wseq α)
Equations
source
def stream.wseq.nil {α : Type u} :
stream.wseq α

The empty weak sequence

Equations
source
@[protected, instance]
def stream.wseq.inhabited {α : Type u} :
inhabited (stream.wseq α)
Equations
source
def stream.wseq.cons {α : Type u} (a : α) :
stream.wseq α → stream.wseq α

Prepend an element to a weak sequence

Equations
source
def stream.wseq.think {α : Type u} :
stream.wseq α → stream.wseq α

Compute for one tick, without producing any elements

Equations
source
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.

Equations
source
def stream.wseq.rec_on {α : 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 s.think) :
C s

Recursion principle for weak sequences, compare with list.rec_on.

Equations
source
@[protected]
def stream.wseq.mem {α : Type u} (a : α) (s : stream.wseq α) :
Prop

membership for weak sequences

Equations
source
@[protected, instance]
def stream.wseq.has_mem {α : Type u} :
has_mem α (stream.wseq α)
Equations
source
theorem stream.wseq.not_mem_nil {α : Type u} (a : α) :
a ∉ stream.wseq.nil
source
def stream.wseq.head {α : Type u} (s : stream.wseq α) :
computation (option α)

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

Equations
Instances for stream.wseq.head
source
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

Equations
source
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.

Equations
Instances for stream.wseq.tail
source
@[simp]
def stream.wseq.drop {α : Type u} (s : stream.wseq α) :
ℕ → stream.wseq α

drop the first n elements from s.

Equations
Instances for stream.wseq.drop
source
def stream.wseq.nth {α : Type u} (s : stream.wseq α) (n : ℕ) :
computation (option α)

Get the nth element of s.

Equations
Instances for stream.wseq.nth
source
def stream.wseq.to_list {α : Type u} (s : stream.wseq α) :
computation (list α)

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

Equations
Instances for stream.wseq.to_list
source
def stream.wseq.length {α : Type u} (s : stream.wseq α) :
computation ℕ

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

Equations
source
@[class]
structure stream.wseq.is_finite {α : Type u} (s : stream.wseq α) :
Prop

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

source
@[protected, instance]
def stream.wseq.to_list_terminates {α : Type u} (s : stream.wseq α) [h : s.is_finite] :
s.to_list.terminates
source
def stream.wseq.get {α : Type u} (s : stream.wseq α) [s.is_finite] :
list α

Get the list corresponding to a finite weak sequence.

Equations
source
@[class]
structure stream.wseq.productive {α : Type u} (s : stream.wseq α) :
Prop

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.

Instances of this typeclass
source
theorem stream.wseq.productive_iff {α : Type u} (s : stream.wseq α) :
s.productive ↔ ∀ (n : ℕ), (s.nth n).terminates
source
@[protected, instance]
def stream.wseq.nth_terminates {α : Type u} (s : stream.wseq α) [h : s.productive] (n : ℕ) :
(s.nth n).terminates
source
@[protected, instance]
def stream.wseq.head_terminates {α : Type u} (s : stream.wseq α) [s.productive] :
s.head.terminates
source
def stream.wseq.update_nth {α : Type u} (s : stream.wseq α) (n : ℕ) (a : α) :
stream.wseq α

Replace the nth element of s with a.

Equations
source
def stream.wseq.remove_nth {α : Type u} (s : stream.wseq α) (n : ℕ) :
stream.wseq α

Remove the nth element of s.

Equations
source
def stream.wseq.filter_map {α : Type u} {β : Type v} (f : α → option β) :
stream.wseq α → stream.wseq β

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

Equations
source
def stream.wseq.filter {α : Type u} (p : α → Prop) [decidable_pred p] :
stream.wseq α → stream.wseq α

Select the elements of s that satisfy p.

Equations
source
def stream.wseq.find {α : Type u} (p : α → Prop) [decidable_pred p] (s : stream.wseq α) :
computation (option α)

Get the first element of s satisfying p.

Equations
source
def stream.wseq.zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s1 : stream.wseq α) (s2 : stream.wseq β) :
stream.wseq γ

Zip a function over two weak sequences

Equations
source
def stream.wseq.zip {α : Type u} {β : Type v} :
stream.wseq α → stream.wseq β → stream.wseq (α × β)

Zip two weak sequences into a single sequence of pairs

Equations
source
def stream.wseq.find_indexes {α : Type u} (p : α → Prop) [decidable_pred p] (s : stream.wseq α) :
stream.wseq ℕ

Get the list of indexes of elements of s satisfying p

Equations
source
def stream.wseq.find_index {α : Type u} (p : α → Prop) [decidable_pred p] (s : stream.wseq α) :
computation ℕ

Get the index of the first element of s satisfying p

Equations
source
def stream.wseq.index_of {α : Type u} [decidable_eq α] (a : α) :
stream.wseq α → computation ℕ

Get the index of the first occurrence of a in s

Equations
source
def stream.wseq.indexes_of {α : Type u} [decidable_eq α] (a : α) :
stream.wseq α → stream.wseq ℕ

Get the indexes of occurrences of a in s

Equations
source
def stream.wseq.union {α : Type u} (s1 s2 : stream.wseq α) :
stream.wseq α

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

Equations
source
def stream.wseq.is_empty {α : Type u} (s : stream.wseq α) :
computation bool

Returns tt if s is nil and ff if s has an element

Equations
source
def stream.wseq.compute {α : Type u} (s : stream.wseq α) :
stream.wseq α

Calculate one step of computation

Equations
source
def stream.wseq.take {α : Type u} (s : stream.wseq α) (n : ℕ) :
stream.wseq α

Get the first n elements of a weak sequence

Equations
source
def stream.wseq.split_at {α : 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

Equations
source
def stream.wseq.any {α : Type u} (s : stream.wseq α) (p : α → bool) :
computation bool

Returns tt if any element of s satisfies p

Equations
source
def stream.wseq.all {α : Type u} (s : stream.wseq α) (p : α → bool) :
computation bool

Returns tt if every element of s satisfies p

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

Equations
source
def stream.wseq.inits {α : Type u} (s : stream.wseq α) :
stream.wseq (list α)

Get the weak sequence of initial segments of the input sequence

Equations
source
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

Equations
source
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

Equations
source
def stream.wseq.map {α : Type u} {β : Type v} (f : α → β) :
stream.wseq α → stream.wseq β

Map a function over a weak sequence

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

Equations
source
def stream.wseq.bind {α : Type u} {β : Type v} (s : stream.wseq α) (f : α → stream.wseq β) :
stream.wseq β

Monadic bind operator for weak sequences

Equations
source
@[simp]
def stream.wseq.lift_rel_o {α : 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

Equations
source
theorem stream.wseq.lift_rel_o.imp {α : Type u} {β : Type v} {R S : α → β → Prop} {C 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.lift_rel_o R C o p → stream.wseq.lift_rel_o S D o p
source
theorem stream.wseq.lift_rel_o.imp_right {α : Type u} {β : Type v} (R : α → β → Prop) {C 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.lift_rel_o R C o p → stream.wseq.lift_rel_o R D o p
source
@[simp]
def stream.wseq.bisim_o {α : Type u} (R : stream.wseq α → stream.wseq α → Prop) :
option (α × stream.wseq α) → option (α × stream.wseq α) → Prop

Definitino of bisimilarity for weak sequences

Equations
source
theorem stream.wseq.bisim_o.imp {α : Type u} {R S : stream.wseq α → stream.wseq α → Prop} (H : ∀ (s t : stream.wseq α), R s t → S s t) {o p : option (α × stream.wseq α)} :
stream.wseq.bisim_o R o p → stream.wseq.bisim_o S o p
source
def stream.wseq.lift_rel {α : Type u} {β : Type v} (R : α → β → Prop) (s : stream.wseq α) (t : stream.wseq β) :
Prop

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

Equations
source
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.

Equations
source
theorem stream.wseq.lift_rel_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : stream.wseq α} {t : stream.wseq β} :
stream.wseq.lift_rel R s t → computation.lift_rel (stream.wseq.lift_rel_o R (stream.wseq.lift_rel R)) s.destruct t.destruct
source
theorem stream.wseq.lift_rel_destruct_iff {α : Type u} {β : Type v} {R : α → β → Prop} {s : stream.wseq α} {t : stream.wseq β} :
stream.wseq.lift_rel R s t ↔ computation.lift_rel (stream.wseq.lift_rel_o R (stream.wseq.lift_rel R)) s.destruct t.destruct
source
theorem stream.wseq.destruct_congr {α : Type u} {s t : stream.wseq α} :
s ~ t → computation.lift_rel (stream.wseq.bisim_o stream.wseq.equiv) s.destruct t.destruct
source
theorem stream.wseq.destruct_congr_iff {α : Type u} {s t : stream.wseq α} :
s ~ t ↔ computation.lift_rel (stream.wseq.bisim_o stream.wseq.equiv) s.destruct t.destruct
source
theorem stream.wseq.lift_rel.refl {α : Type u} (R : α → α → Prop) (H : reflexive R) :
reflexive (stream.wseq.lift_rel R)
source
theorem stream.wseq.lift_rel_o.swap {α : Type u} {β : Type v} (R : α → β → Prop) (C : stream.wseq α → stream.wseq β → Prop) :
function.swap (stream.wseq.lift_rel_o R C) = stream.wseq.lift_rel_o (function.swap R) (function.swap C)
source
theorem stream.wseq.lift_rel.swap_lem {α : Type u} {β : Type v} {R : α → β → Prop} {s1 : stream.wseq α} {s2 : stream.wseq β} (h : stream.wseq.lift_rel R s1 s2) :
stream.wseq.lift_rel (function.swap R) s2 s1
source
theorem stream.wseq.lift_rel.swap {α : Type u} {β : Type v} (R : α → β → Prop) :
function.swap (stream.wseq.lift_rel R) = stream.wseq.lift_rel (function.swap R)
source
theorem stream.wseq.lift_rel.symm {α : Type u} (R : α → α → Prop) (H : symmetric R) :
symmetric (stream.wseq.lift_rel R)
source
theorem stream.wseq.lift_rel.trans {α : Type u} (R : α → α → Prop) (H : transitive R) :
transitive (stream.wseq.lift_rel R)
source
theorem stream.wseq.lift_rel.equiv {α : Type u} (R : α → α → Prop) :
equivalence R → equivalence (stream.wseq.lift_rel R)
source
@[refl]
theorem stream.wseq.equiv.refl {α : Type u} (s : stream.wseq α) :
s ~ s
source
@[symm]
theorem stream.wseq.equiv.symm {α : Type u} {s t : stream.wseq α} :
s ~ t → t ~ s
source
@[trans]
theorem stream.wseq.equiv.trans {α : Type u} {s t u : stream.wseq α} :
s ~ t → t ~ u → s ~ u
source
theorem stream.wseq.equiv.equivalence {α : Type u} :
equivalence stream.wseq.equiv
source
@[simp]
theorem stream.wseq.destruct_nil {α : Type u} :
stream.wseq.nil.destruct = computation.return option.none
source
@[simp]
theorem stream.wseq.destruct_cons {α : Type u} (a : α) (s : stream.wseq α) :
(stream.wseq.cons a s).destruct = computation.return (option.some (a, s))
source
@[simp]
theorem stream.wseq.destruct_think {α : Type u} (s : stream.wseq α) :
s.think.destruct = s.destruct.think
source
@[simp]
theorem stream.wseq.seq_destruct_nil {α : Type u} :
stream.seq.destruct stream.wseq.nil = option.none
source
@[simp]
theorem stream.wseq.seq_destruct_cons {α : Type u} (a : α) (s : stream.wseq α) :
stream.seq.destruct (stream.wseq.cons a s) = option.some (option.some a, s)
source
@[simp]
theorem stream.wseq.seq_destruct_think {α : Type u} (s : stream.wseq α) :
stream.seq.destruct s.think = option.some (option.none α, s)
source
@[simp]
theorem stream.wseq.head_nil {α : Type u} :
stream.wseq.nil.head = computation.return option.none
source
@[simp]
theorem stream.wseq.head_cons {α : Type u} (a : α) (s : stream.wseq α) :
(stream.wseq.cons a s).head = computation.return (option.some a)
source
@[simp]
theorem stream.wseq.head_think {α : Type u} (s : stream.wseq α) :
s.think.head = s.head.think
source
@[simp]
theorem stream.wseq.flatten_ret {α : Type u} (s : stream.wseq α) :
stream.wseq.flatten (computation.return s) = s
source
@[simp]
theorem stream.wseq.flatten_think {α : Type u} (c : computation (stream.wseq α)) :
stream.wseq.flatten c.think = (stream.wseq.flatten c).think
source
@[simp]
theorem stream.wseq.destruct_flatten {α : Type u} (c : computation (stream.wseq α)) :
(stream.wseq.flatten c).destruct = c >>= stream.wseq.destruct
source
theorem stream.wseq.head_terminates_iff {α : Type u} (s : stream.wseq α) :
s.head.terminates ↔ s.destruct.terminates
source
@[simp]
theorem stream.wseq.tail_nil {α : Type u} :
stream.wseq.nil.tail = stream.wseq.nil
source
@[simp]
theorem stream.wseq.tail_cons {α : Type u} (a : α) (s : stream.wseq α) :
(stream.wseq.cons a s).tail = s
source
@[simp]
theorem stream.wseq.tail_think {α : Type u} (s : stream.wseq α) :
s.think.tail = s.tail.think
source
@[simp]
theorem stream.wseq.dropn_nil {α : Type u} (n : ℕ) :
stream.wseq.nil.drop n = stream.wseq.nil
source
@[simp]
theorem stream.wseq.dropn_cons {α : Type u} (a : α) (s : stream.wseq α) (n : ℕ) :
(stream.wseq.cons a s).drop (n + 1) = s.drop n
source
@[simp]
theorem stream.wseq.dropn_think {α : Type u} (s : stream.wseq α) (n : ℕ) :
s.think.drop n = (s.drop n).think
source
theorem stream.wseq.dropn_add {α : Type u} (s : stream.wseq α) (m n : ℕ) :
s.drop (m + n) = (s.drop m).drop n
source
theorem stream.wseq.dropn_tail {α : Type u} (s : stream.wseq α) (n : ℕ) :
s.tail.drop n = s.drop (n + 1)
source
theorem stream.wseq.nth_add {α : Type u} (s : stream.wseq α) (m n : ℕ) :
s.nth (m + n) = (s.drop m).nth n
source
theorem stream.wseq.nth_tail {α : Type u} (s : stream.wseq α) (n : ℕ) :
s.tail.nth n = s.nth (n + 1)
source
@[simp]
theorem stream.wseq.join_nil {α : Type u} :
stream.wseq.nil.join = stream.wseq.nil
source
@[simp]
theorem stream.wseq.join_think {α : Type u} (S : stream.wseq (stream.wseq α)) :
S.think.join = S.join.think
source
@[simp]
theorem stream.wseq.join_cons {α : Type u} (s : stream.wseq α) (S : stream.wseq (stream.wseq α)) :
(stream.wseq.cons s S).join = (s.append S.join).think
source
@[simp]
theorem stream.wseq.nil_append {α : Type u} (s : stream.wseq α) :
stream.wseq.nil.append s = s
source
@[simp]
theorem stream.wseq.cons_append {α : Type u} (a : α) (s t : stream.wseq α) :
(stream.wseq.cons a s).append t = stream.wseq.cons a (s.append t)
source
@[simp]
theorem stream.wseq.think_append {α : Type u} (s t : stream.wseq α) :
s.think.append t = (s.append t).think
source
@[simp]
theorem stream.wseq.append_nil {α : Type u} (s : stream.wseq α) :
s.append stream.wseq.nil = s
source
@[simp]
theorem stream.wseq.append_assoc {α : Type u} (s t u : stream.wseq α) :
(s.append t).append u = s.append (t.append u)
source
@[simp]
def stream.wseq.tail.aux {α : Type u} :
option (α × stream.wseq α) → computation (option (α × stream.wseq α))

auxilary defintion of tail over weak sequences

Equations
source
theorem stream.wseq.destruct_tail {α : Type u} (s : stream.wseq α) :
s.tail.destruct = s.destruct >>= stream.wseq.tail.aux
source
@[simp]
def stream.wseq.drop.aux {α : Type u} :
ℕ → option (α × stream.wseq α) → computation (option (α × stream.wseq α))

auxilary defintion of drop over weak sequences

Equations
source
theorem stream.wseq.drop.aux_none {α : Type u} (n : ℕ) :
stream.wseq.drop.aux n option.none = computation.return option.none
source
theorem stream.wseq.destruct_dropn {α : Type u} (s : stream.wseq α) (n : ℕ) :
(s.drop n).destruct = s.destruct >>= stream.wseq.drop.aux n
source
theorem stream.wseq.head_terminates_of_head_tail_terminates {α : Type u} (s : stream.wseq α) [T : s.tail.head.terminates] :
s.head.terminates
source
theorem stream.wseq.destruct_some_of_destruct_tail_some {α : Type u} {s : stream.wseq α} {a : α × stream.wseq α} (h : option.some a ∈ s.tail.destruct) :
∃ (a' : α × stream.wseq α), option.some a' ∈ s.destruct
source
theorem stream.wseq.head_some_of_head_tail_some {α : Type u} {s : stream.wseq α} {a : α} (h : option.some a ∈ s.tail.head) :
∃ (a' : α), option.some a' ∈ s.head
source
theorem stream.wseq.head_some_of_nth_some {α : Type u} {s : stream.wseq α} {a : α} {n : ℕ} (h : option.some a ∈ s.nth n) :
∃ (a' : α), option.some a' ∈ s.head
source
@[protected, instance]
def stream.wseq.productive_tail {α : Type u} (s : stream.wseq α) [s.productive] :
s.tail.productive
source
@[protected, instance]
def stream.wseq.productive_dropn {α : Type u} (s : stream.wseq α) [s.productive] (n : ℕ) :
(s.drop n).productive
source
def stream.wseq.to_seq {α : Type u} (s : stream.wseq α) [s.productive] :
stream.seq α

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

Equations
source
theorem stream.wseq.nth_terminates_le {α : Type u} {s : stream.wseq α} {m n : ℕ} (h : m ≤ n) :
(s.nth n).terminates → (s.nth m).terminates
source
theorem stream.wseq.head_terminates_of_nth_terminates {α : Type u} {s : stream.wseq α} {n : ℕ} :
(s.nth n).terminates → s.head.terminates
source
theorem stream.wseq.destruct_terminates_of_nth_terminates {α : Type u} {s : stream.wseq α} {n : ℕ} (T : (s.nth n).terminates) :
s.destruct.terminates
source
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 s.think) :
C s
source
@[simp]
theorem stream.wseq.mem_think {α : Type u} (s : stream.wseq α) (a : α) :
a ∈ s.think ↔ a ∈ s
source
theorem stream.wseq.eq_or_mem_iff_mem {α : Type u} {s : stream.wseq α} {a a' : α} {s' : stream.wseq α} :
option.some (a', s') ∈ s.destruct → (a ∈ s ↔ a = a' ∨ a ∈ s')
source
@[simp]
theorem stream.wseq.mem_cons_iff {α : Type u} (s : stream.wseq α) (b : α) {a : α} :
a ∈ stream.wseq.cons b s ↔ a = b ∨ a ∈ s
source
theorem stream.wseq.mem_cons_of_mem {α : Type u} {s : stream.wseq α} (b : α) {a : α} (h : a ∈ s) :
a ∈ stream.wseq.cons b s
source
theorem stream.wseq.mem_cons {α : Type u} (s : stream.wseq α) (a : α) :
a ∈ stream.wseq.cons a s
source
theorem stream.wseq.mem_of_mem_tail {α : Type u} {s : stream.wseq α} {a : α} :
a ∈ s.tail → a ∈ s
source
theorem stream.wseq.mem_of_mem_dropn {α : Type u} {s : stream.wseq α} {a : α} {n : ℕ} :
a ∈ s.drop n → a ∈ s
source
theorem stream.wseq.nth_mem {α : Type u} {s : stream.wseq α} {a : α} {n : ℕ} :
option.some a ∈ s.nth n → a ∈ s
source
theorem stream.wseq.exists_nth_of_mem {α : Type u} {s : stream.wseq α} {a : α} (h : a ∈ s) :
∃ (n : ℕ), option.some a ∈ s.nth n
source
theorem stream.wseq.exists_dropn_of_mem {α : Type u} {s : stream.wseq α} {a : α} (h : a ∈ s) :
∃ (n : ℕ) (s' : stream.wseq α), option.some (a, s') ∈ (s.drop n).destruct
source
theorem stream.wseq.lift_rel_dropn_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : stream.wseq α} {t : stream.wseq β} (H : stream.wseq.lift_rel R s t) (n : ℕ) :
computation.lift_rel (stream.wseq.lift_rel_o R (stream.wseq.lift_rel R)) (s.drop n).destruct (t.drop n).destruct
source
theorem stream.wseq.exists_of_lift_rel_left {α : Type u} {β : Type v} {R : α → β → Prop} {s : stream.wseq α} {t : stream.wseq β} (H : stream.wseq.lift_rel R s t) {a : α} (h : a ∈ s) :
∃ {b : β}, b ∈ t ∧ R a b
source
theorem stream.wseq.exists_of_lift_rel_right {α : Type u} {β : Type v} {R : α → β → Prop} {s : stream.wseq α} {t : stream.wseq β} (H : stream.wseq.lift_rel R s t) {b : β} (h : b ∈ t) :
∃ {a : α}, a ∈ s ∧ R a b
source
theorem stream.wseq.head_terminates_of_mem {α : Type u} {s : stream.wseq α} {a : α} (h : a ∈ s) :
s.head.terminates
source
theorem stream.wseq.of_mem_append {α : Type u} {s₁ s₂ : stream.wseq α} {a : α} :
a ∈ s₁.append s₂ → a ∈ s₁ ∨ a ∈ s₂
source
theorem stream.wseq.mem_append_left {α : Type u} {s₁ s₂ : stream.wseq α} {a : α} :
a ∈ s₁ → a ∈ s₁.append s₂
source
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)
source
@[simp]
theorem stream.wseq.lift_rel_nil {α : Type u} {β : Type v} (R : α → β → Prop) :
stream.wseq.lift_rel R stream.wseq.nil stream.wseq.nil
source
@[simp]
theorem stream.wseq.lift_rel_cons {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β) (s : stream.wseq α) (t : stream.wseq β) :
stream.wseq.lift_rel R (stream.wseq.cons a s) (stream.wseq.cons b t) ↔ R a b ∧ stream.wseq.lift_rel R s t
source
@[simp]
theorem stream.wseq.lift_rel_think_left {α : Type u} {β : Type v} (R : α → β → Prop) (s : stream.wseq α) (t : stream.wseq β) :
stream.wseq.lift_rel R s.think t ↔ stream.wseq.lift_rel R s t
source
@[simp]
theorem stream.wseq.lift_rel_think_right {α : Type u} {β : Type v} (R : α → β → Prop) (s : stream.wseq α) (t : stream.wseq β) :
stream.wseq.lift_rel R s t.think ↔ stream.wseq.lift_rel R s t
source
theorem stream.wseq.cons_congr {α : Type u} {s t : stream.wseq α} (a : α) (h : s ~ t) :
stream.wseq.cons a s ~ stream.wseq.cons a t
source
theorem stream.wseq.think_equiv {α : Type u} (s : stream.wseq α) :
s.think ~ s
source
theorem stream.wseq.think_congr {α : Type u} {s t : stream.wseq α} (h : s ~ t) :
s.think ~ t.think
source
theorem stream.wseq.head_congr {α : Type u} {s t : stream.wseq α} :
s ~ t → s.head ~ t.head
source
theorem stream.wseq.flatten_equiv {α : Type u} {c : computation (stream.wseq α)} {s : stream.wseq α} (h : s ∈ c) :
stream.wseq.flatten c ~ s
source
theorem stream.wseq.lift_rel_flatten {α : Type u} {β : Type v} {R : α → β → Prop} {c1 : computation (stream.wseq α)} {c2 : computation (stream.wseq β)} (h : computation.lift_rel (stream.wseq.lift_rel R) c1 c2) :
stream.wseq.lift_rel R (stream.wseq.flatten c1) (stream.wseq.flatten c2)
source
theorem stream.wseq.flatten_congr {α : Type u} {c1 c2 : computation (stream.wseq α)} :
computation.lift_rel stream.wseq.equiv c1 c2 → stream.wseq.flatten c1 ~ stream.wseq.flatten c2
source
theorem stream.wseq.tail_congr {α : Type u} {s t : stream.wseq α} (h : s ~ t) :
s.tail ~ t.tail
source
theorem stream.wseq.dropn_congr {α : Type u} {s t : stream.wseq α} (h : s ~ t) (n : ℕ) :
s.drop n ~ t.drop n
source
theorem stream.wseq.nth_congr {α : Type u} {s t : stream.wseq α} (h : s ~ t) (n : ℕ) :
s.nth n ~ t.nth n
source
theorem stream.wseq.mem_congr {α : Type u} {s t : stream.wseq α} (h : s ~ t) (a : α) :
a ∈ s ↔ a ∈ t
source
theorem stream.wseq.productive_congr {α : Type u} {s t : stream.wseq α} (h : s ~ t) :
s.productive ↔ t.productive
source
theorem stream.wseq.equiv.ext {α : Type u} {s t : stream.wseq α} (h : ∀ (n : ℕ), s.nth n ~ t.nth n) :
s ~ t
source
theorem stream.wseq.length_eq_map {α : Type u} (s : stream.wseq α) :
s.length = computation.map list.length s.to_list
source
@[simp]
theorem stream.wseq.of_list_nil {α : Type u} :
stream.wseq.of_list list.nil = stream.wseq.nil
source
@[simp]
theorem stream.wseq.of_list_cons {α : Type u} (a : α) (l : list α) :
stream.wseq.of_list (a :: l) = stream.wseq.cons a (stream.wseq.of_list l)
source
@[simp]
theorem stream.wseq.to_list'_nil {α : Type u} (l : list α) :
computation.corec stream.wseq.to_list._match_2 (l, stream.wseq.nil α) = computation.return l.reverse
source
@[simp]
theorem stream.wseq.to_list'_cons {α : Type u} (l : list α) (s : stream.wseq α) (a : α) :
computation.corec stream.wseq.to_list._match_2 (l, stream.wseq.cons a s) = (computation.corec stream.wseq.to_list._match_2 (a :: l, s)).think
source
@[simp]
theorem stream.wseq.to_list'_think {α : Type u} (l : list α) (s : stream.wseq α) :
computation.corec stream.wseq.to_list._match_2 (l, s.think) = (computation.corec stream.wseq.to_list._match_2 (l, s)).think
source
theorem stream.wseq.to_list'_map {α : Type u} (l : list α) (s : stream.wseq α) :
computation.corec stream.wseq.to_list._match_2 (l, s) = has_append.append l.reverse <$> s.to_list
source
@[simp]
theorem stream.wseq.to_list_cons {α : Type u} (a : α) (s : stream.wseq α) :
(stream.wseq.cons a s).to_list = (list.cons a <$> s.to_list).think
source
@[simp]
theorem stream.wseq.to_list_nil {α : Type u} :
stream.wseq.nil.to_list = computation.return list.nil
source
theorem stream.wseq.to_list_of_list {α : Type u} (l : list α) :
l ∈ (stream.wseq.of_list l).to_list
source
@[simp]
theorem stream.wseq.destruct_of_seq {α : Type u} (s : stream.seq α) :
(stream.wseq.of_seq s).destruct = computation.return (option.map (λ (a : α), (a, stream.wseq.of_seq s.tail)) s.head)
source
@[simp]
theorem stream.wseq.head_of_seq {α : Type u} (s : stream.seq α) :
(stream.wseq.of_seq s).head = computation.return s.head
source
@[simp]
theorem stream.wseq.tail_of_seq {α : Type u} (s : stream.seq α) :
(stream.wseq.of_seq s).tail = stream.wseq.of_seq s.tail
source
@[simp]
theorem stream.wseq.dropn_of_seq {α : Type u} (s : stream.seq α) (n : ℕ) :
(stream.wseq.of_seq s).drop n = stream.wseq.of_seq (s.drop n)
source
theorem stream.wseq.nth_of_seq {α : Type u} (s : stream.seq α) (n : ℕ) :
(stream.wseq.of_seq s).nth n = computation.return (s.nth n)
source
@[protected, instance]
def stream.wseq.productive_of_seq {α : Type u} (s : stream.seq α) :
(stream.wseq.of_seq s).productive
source
theorem stream.wseq.to_seq_of_seq {α : Type u} (s : stream.seq α) :
(stream.wseq.of_seq s).to_seq = s
source
def stream.wseq.ret {α : Type u} (a : α) :
stream.wseq α

The monadic return a is a singleton list containing a.

Equations
source
@[simp]
theorem stream.wseq.map_nil {α : Type u} {β : Type v} (f : α → β) :
stream.wseq.map f stream.wseq.nil = stream.wseq.nil
source
@[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)
source
@[simp]
theorem stream.wseq.map_think {α : Type u} {β : Type v} (f : α → β) (s : stream.wseq α) :
stream.wseq.map f s.think = (stream.wseq.map f s).think
source
@[simp]
theorem stream.wseq.map_id {α : Type u} (s : stream.wseq α) :
stream.wseq.map id s = s
source
@[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)
source
@[simp]
theorem stream.wseq.map_append {α : Type u} {β : Type v} (f : α → β) (s t : stream.wseq α) :
stream.wseq.map f (s.append t) = (stream.wseq.map f s).append (stream.wseq.map f t)
source
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)
source
theorem stream.wseq.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : stream.wseq α} :
a ∈ s → f a ∈ stream.wseq.map f s
source
theorem stream.wseq.exists_of_mem_join {α : Type u} {a : α} {S : stream.wseq (stream.wseq α)} :
a ∈ S.join → (∃ (s : stream.wseq α), s ∈ S ∧ a ∈ s)
source
theorem stream.wseq.exists_of_mem_bind {α : Type u} {β : Type v} {s : stream.wseq α} {f : α → stream.wseq β} {b : β} (h : b ∈ s.bind f) :
∃ (a : α) (H : a ∈ s), b ∈ f a
source
theorem stream.wseq.destruct_map {α : Type u} {β : Type v} (f : α → β) (s : stream.wseq α) :
(stream.wseq.map f s).destruct = computation.map (option.map (prod.map f (stream.wseq.map f))) s.destruct
source
theorem stream.wseq.lift_rel_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.lift_rel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → S (f1 a) (f2 b)) :
stream.wseq.lift_rel S (stream.wseq.map f1 s1) (stream.wseq.map f2 s2)
source
theorem stream.wseq.map_congr {α : Type u} {β : Type v} (f : α → β) {s t : stream.wseq α} (h : s ~ t) :
stream.wseq.map f s ~ stream.wseq.map f t
source
@[simp]
def stream.wseq.destruct_append.aux {α : Type u} (t : stream.wseq α) :
option (α × stream.wseq α) → computation (option (α × stream.wseq α))

auxilary defintion of destruct_append over weak sequences

Equations
source
theorem stream.wseq.destruct_append {α : Type u} (s t : stream.wseq α) :
(s.append t).destruct = s.destruct.bind (stream.wseq.destruct_append.aux t)
source
@[simp]
def stream.wseq.destruct_join.aux {α : Type u} :
option (stream.wseq α × stream.wseq (stream.wseq α)) → computation (option (α × stream.wseq α))

auxilary defintion of destruct_join over weak sequences

Equations
source
theorem stream.wseq.destruct_join {α : Type u} (S : stream.wseq (stream.wseq α)) :
S.join.destruct = S.destruct.bind stream.wseq.destruct_join.aux
source
theorem stream.wseq.lift_rel_append {α : Type u} {β : Type v} (R : α → β → Prop) {s1 s2 : stream.wseq α} {t1 t2 : stream.wseq β} (h1 : stream.wseq.lift_rel R s1 t1) (h2 : stream.wseq.lift_rel R s2 t2) :
stream.wseq.lift_rel R (s1.append s2) (t1.append t2)
source
theorem stream.wseq.lift_rel_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.lift_rel (stream.wseq.lift_rel R) S T) (HU : ∀ (s1 : stream.wseq α) (s2 : stream.wseq β), (∃ (s : stream.wseq α) (t : stream.wseq β) (S : stream.wseq (stream.wseq α)) (T : stream.wseq (stream.wseq β)), s1 = s.append S.join ∧ s2 = t.append T.join ∧ stream.wseq.lift_rel R s t ∧ stream.wseq.lift_rel (stream.wseq.lift_rel R) S T) → U s1 s2) {a : option (α × stream.wseq α)} (ma : a ∈ S.join.destruct) :
∃ {b : option (β × stream.wseq β)}, b ∈ T.join.destruct ∧ stream.wseq.lift_rel_o R U a b
source
theorem stream.wseq.lift_rel_join {α : Type u} {β : Type v} (R : α → β → Prop) {S : stream.wseq (stream.wseq α)} {T : stream.wseq (stream.wseq β)} (h : stream.wseq.lift_rel (stream.wseq.lift_rel R) S T) :
stream.wseq.lift_rel R S.join T.join
source
theorem stream.wseq.join_congr {α : Type u} {S T : stream.wseq (stream.wseq α)} (h : stream.wseq.lift_rel stream.wseq.equiv S T) :
S.join ~ T.join
source
theorem stream.wseq.lift_rel_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.lift_rel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a b → stream.wseq.lift_rel S (f1 a) (f2 b)) :
stream.wseq.lift_rel S (s1.bind f1) (s2.bind f2)
source
theorem stream.wseq.bind_congr {α : Type u} {β : Type v} {s1 s2 : stream.wseq α} {f1 f2 : α → stream.wseq β} (h1 : s1 ~ s2) (h2 : ∀ (a : α), f1 a ~ f2 a) :
s1.bind f1 ~ s2.bind f2
source
@[simp]
theorem stream.wseq.join_ret {α : Type u} (s : stream.wseq α) :
(stream.wseq.ret s).join ~ s
source
@[simp]
theorem stream.wseq.join_map_ret {α : Type u} (s : stream.wseq α) :
(stream.wseq.map stream.wseq.ret s).join ~ s
source
@[simp]
theorem stream.wseq.join_append {α : Type u} (S T : stream.wseq (stream.wseq α)) :
(S.append T).join ~ S.join.append T.join
source
@[simp]
theorem stream.wseq.bind_ret {α : Type u} {β : Type v} (f : α → β) (s : stream.wseq α) :
s.bind (stream.wseq.ret ∘ f) ~ stream.wseq.map f s
source
@[simp]
theorem stream.wseq.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → stream.wseq β) :
(stream.wseq.ret a).bind f ~ f a
source
@[simp]
theorem stream.wseq.map_join {α : Type u} {β : Type v} (f : α → β) (S : stream.wseq (stream.wseq α)) :
stream.wseq.map f S.join = (stream.wseq.map (stream.wseq.map f) S).join
source
@[simp]
theorem stream.wseq.join_join {α : Type u} (SS : stream.wseq (stream.wseq (stream.wseq α))) :
SS.join.join ~ (stream.wseq.map stream.wseq.join SS).join
source
@[simp]
theorem stream.wseq.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : stream.wseq α) (f : α → stream.wseq β) (g : β → stream.wseq γ) :
(s.bind f).bind g ~ s.bind (λ (x : α), (f x).bind g)
source
@[protected, instance]
def stream.wseq.monad  :
monad stream.wseq
Equations