mathlib documentation

data.seq.wseq

def wseq  :
Type u_1Type 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 wseq.of_seq {α : Type u} :
seq αwseq α

Turn a sequence into a weak sequence

Equations
def wseq.of_list {α : Type u} :
list αwseq α

Turn a list into a weak sequence

Equations
def wseq.of_stream {α : Type u} :
stream αwseq α

Turn a stream into a weak sequence

Equations
@[instance]
def wseq.coe_seq {α : Type u} :
has_coe (seq α) (wseq α)

Equations
@[instance]
def wseq.coe_list {α : Type u} :
has_coe (list α) (wseq α)

Equations
@[instance]
def wseq.coe_stream {α : Type u} :
has_coe (stream α) (wseq α)

Equations
def wseq.nil {α : Type u} :
wseq α

The empty weak sequence

Equations
@[instance]
def wseq.inhabited {α : Type u} :

Equations
def wseq.cons {α : Type u} :
α → wseq αwseq α

Prepend an element to a weak sequence

Equations
def wseq.think {α : Type u} :
wseq αwseq α

Compute for one tick, without producing any elements

Equations
def 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
def wseq.cases_on {α : Type u} {C : wseq αSort v} (s : wseq α) :
C wseq.nil(Π (x : α) (s : wseq α), C (wseq.cons x s))(Π (s : wseq α), C s.think)C s

Equations
def wseq.mem {α : Type u} :
α → wseq α → Prop

Equations
@[instance]
def wseq.has_mem {α : Type u} :
has_mem α (wseq α)

Equations
theorem wseq.not_mem_nil {α : Type u} (a : α) :

def wseq.head {α : Type u} :
wseq αcomputation (option α)

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

Equations
def wseq.flatten {α : Type u} :
computation (wseq α)wseq α

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

Equations
def wseq.tail {α : Type u} :
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
@[simp]
def wseq.drop {α : Type u} :
wseq αwseq α

drop the first n elements from s.

Equations
def wseq.nth {α : Type u} :
wseq αcomputation (option α)

Get the nth element of s.

Equations
def wseq.to_list {α : Type u} :
wseq αcomputation (list α)

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

Equations
def wseq.length {α : Type u} :

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

Equations
@[class]
def wseq.is_finite {α : Type u} :
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.

Equations
@[instance]
def wseq.to_list_terminates {α : Type u} (s : wseq α) [h : s.is_finite] :

def wseq.get {α : Type u} (s : wseq α) [s.is_finite] :
list α

Get the list corresponding to a finite weak sequence.

Equations
@[class]
def wseq.productive {α : Type u} :
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.

Equations
Instances
@[instance]
def wseq.nth_terminates {α : Type u} (s : wseq α) [h : s.productive] (n : ) :

@[instance]
def wseq.head_terminates {α : Type u} (s : wseq α) [h : s.productive] :

def wseq.update_nth {α : Type u} :
wseq αα → wseq α

Replace the nth element of s with a.

Equations
def wseq.remove_nth {α : Type u} :
wseq αwseq α

Remove the nth element of s.

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

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

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

Select the elements of s that satisfy p.

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

Get the first element of s satisfying p.

Equations
def wseq.zip_with {α : Type u} {β : Type v} {γ : Type w} :
(α → β → γ)wseq αwseq βwseq γ

Zip a function over two weak sequences

Equations
def wseq.zip {α : Type u} {β : Type v} :
wseq αwseq βwseq × β)

Zip two weak sequences into a single sequence of pairs

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

Get the list of indexes of elements of s satisfying p

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

Get the index of the first element of s satisfying p

Equations
def wseq.index_of {α : Type u} [decidable_eq α] :
α → wseq αcomputation

Get the index of the first occurrence of a in s

Equations
def wseq.indexes_of {α : Type u} [decidable_eq α] :
α → wseq αwseq

Get the indexes of occurrences of a in s

Equations
def wseq.union {α : Type u} :
wseq αwseq αwseq α

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

Equations
def wseq.is_empty {α : Type u} :

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

Equations
def wseq.compute {α : Type u} :
wseq αwseq α

Calculate one step of computation

Equations
def wseq.take {α : Type u} :
wseq αwseq α

Get the first n elements of a weak sequence

Equations
def wseq.split_at {α : Type u} :
wseq αcomputation (list α × wseq α)

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

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

Returns tt if any element of s satisfies p

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

Returns tt if every element of s satisfies p

Equations
def wseq.scanl {α : Type u} {β : Type v} :
(α → β → α)α → wseq β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
def wseq.inits {α : Type u} :
wseq αwseq (list α)

Get the weak sequence of initial segments of the input sequence

Equations
def wseq.collect {α : Type u} :
wseq αlist α

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

Equations
def 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 wseq.map {α : Type u} {β : Type v} :
(α → β)wseq αwseq β

Map a function over a weak sequence

Equations
def wseq.join {α : Type u} :
wseq (wseq α)wseq α

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

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

Monadic bind operator for weak sequences

Equations
@[simp]
def wseq.lift_rel_o {α : Type u} {β : Type v} :
(α → β → Prop)(wseq αwseq β → Prop)option × wseq α)option × wseq β) → Prop

Equations
theorem wseq.lift_rel_o.imp {α : Type u} {β : Type v} {R S : α → β → Prop} {C D : wseq αwseq β → Prop} (H1 : ∀ (a : α) (b : β), R a bS a b) (H2 : ∀ (s : wseq α) (t : wseq β), C s tD s t) {o : option × wseq α)} {p : option × wseq β)} :
wseq.lift_rel_o R C o pwseq.lift_rel_o S D o p

theorem wseq.lift_rel_o.imp_right {α : Type u} {β : Type v} (R : α → β → Prop) {C D : wseq αwseq β → Prop} (H : ∀ (s : wseq α) (t : wseq β), C s tD s t) {o : option × wseq α)} {p : option × wseq β)} :
wseq.lift_rel_o R C o pwseq.lift_rel_o R D o p

@[simp]
def wseq.bisim_o {α : Type u} :
(wseq αwseq α → Prop)option × wseq α)option × wseq α) → Prop

Equations
theorem wseq.bisim_o.imp {α : Type u} {R S : wseq αwseq α → Prop} (H : ∀ (s t : wseq α), R s tS s t) {o p : option × wseq α)} :
wseq.bisim_o R o pwseq.bisim_o S o p

def wseq.lift_rel {α : Type u} {β : Type v} :
(α → β → Prop)wseq α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
def wseq.equiv {α : Type u} :
wseq α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
theorem wseq.lift_rel_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : wseq α} {t : wseq β} :

theorem wseq.lift_rel_destruct_iff {α : Type u} {β : Type v} {R : α → β → Prop} {s : wseq α} {t : wseq β} :

theorem wseq.destruct_congr {α : Type u} {s t : wseq α} :

theorem wseq.lift_rel.refl {α : Type u} (R : α → α → Prop) :

theorem wseq.lift_rel_o.swap {α : Type u} {β : Type v} (R : α → β → Prop) (C : wseq αwseq β → Prop) :

theorem wseq.lift_rel.swap_lem {α : Type u} {β : Type v} {R : α → β → Prop} {s1 : wseq α} {s2 : wseq β} :

theorem wseq.lift_rel.swap {α : Type u} {β : Type v} (R : α → β → Prop) :

theorem wseq.lift_rel.symm {α : Type u} (R : α → α → Prop) :

theorem wseq.lift_rel.trans {α : Type u} (R : α → α → Prop) :

theorem wseq.lift_rel.equiv {α : Type u} (R : α → α → Prop) :

theorem wseq.equiv.refl {α : Type u} (s : wseq α) :
s ~ s

theorem wseq.equiv.symm {α : Type u} {s t : wseq α} :
s ~ tt ~ s

theorem wseq.equiv.trans {α : Type u} {s t u : wseq α} :
s ~ tt ~ us ~ u

@[simp]
theorem wseq.destruct_cons {α : Type u} (a : α) (s : wseq α) :

@[simp]
theorem wseq.destruct_think {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.seq_destruct_nil {α : Type u} :

@[simp]
theorem wseq.seq_destruct_cons {α : Type u} (a : α) (s : wseq α) :

@[simp]
theorem wseq.seq_destruct_think {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.head_nil {α : Type u} :

@[simp]
theorem wseq.head_cons {α : Type u} (a : α) (s : wseq α) :

@[simp]
theorem wseq.head_think {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.flatten_ret {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.flatten_think {α : Type u} (c : computation (wseq α)) :

@[simp]
theorem wseq.destruct_flatten {α : Type u} (c : computation (wseq α)) :

theorem wseq.head_terminates_iff {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.tail_nil {α : Type u} :

@[simp]
theorem wseq.tail_cons {α : Type u} (a : α) (s : wseq α) :
(wseq.cons a s).tail = s

@[simp]
theorem wseq.tail_think {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.dropn_nil {α : Type u} (n : ) :

@[simp]
theorem wseq.dropn_cons {α : Type u} (a : α) (s : wseq α) (n : ) :
(wseq.cons a s).drop (n + 1) = s.drop n

@[simp]
theorem wseq.dropn_think {α : Type u} (s : wseq α) (n : ) :
s.think.drop n = (s.drop n).think

theorem wseq.dropn_add {α : Type u} (s : wseq α) (m n : ) :
s.drop (m + n) = (s.drop m).drop n

theorem wseq.dropn_tail {α : Type u} (s : wseq α) (n : ) :
s.tail.drop n = s.drop (n + 1)

theorem wseq.nth_add {α : Type u} (s : wseq α) (m n : ) :
s.nth (m + n) = (s.drop m).nth n

theorem wseq.nth_tail {α : Type u} (s : wseq α) (n : ) :
s.tail.nth n = s.nth (n + 1)

@[simp]
theorem wseq.join_nil {α : Type u} :

@[simp]
theorem wseq.join_think {α : Type u} (S : wseq (wseq α)) :

@[simp]
theorem wseq.join_cons {α : Type u} (s : wseq α) (S : wseq (wseq α)) :

@[simp]
theorem wseq.nil_append {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.cons_append {α : Type u} (a : α) (s t : wseq α) :

@[simp]
theorem wseq.think_append {α : Type u} (s t : wseq α) :

@[simp]
theorem wseq.append_nil {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.append_assoc {α : Type u} (s t u : wseq α) :
(s.append t).append u = s.append (t.append u)

@[simp]
def wseq.tail.aux {α : Type u} :
option × wseq α)computation (option × wseq α))

Equations
theorem wseq.destruct_tail {α : Type u} (s : wseq α) :

@[simp]
def wseq.drop.aux {α : Type u} :
option × wseq α)computation (option × wseq α))

Equations
theorem wseq.destruct_dropn {α : Type u} (s : wseq α) (n : ) :

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

theorem wseq.head_some_of_head_tail_some {α : Type u} {s : wseq α} {a : α} :
some a s.tail.head(∃ (a' : α), some a' s.head)

theorem wseq.head_some_of_nth_some {α : Type u} {s : wseq α} {a : α} {n : } :
some a s.nth n(∃ (a' : α), some a' s.head)

@[instance]
def wseq.productive_tail {α : Type u} (s : wseq α) [s.productive] :

@[instance]
def wseq.productive_dropn {α : Type u} (s : wseq α) [s.productive] (n : ) :

def wseq.to_seq {α : Type u} (s : wseq α) [s.productive] :
seq α

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

Equations
theorem wseq.nth_terminates_le {α : Type u} {s : wseq α} {m n : } :
m n(s.nth n).terminates(s.nth m).terminates

theorem wseq.head_terminates_of_nth_terminates {α : Type u} {s : wseq α} {n : } :

theorem wseq.destruct_terminates_of_nth_terminates {α : Type u} {s : wseq α} {n : } :

theorem wseq.mem_rec_on {α : Type u} {C : wseq α → Prop} {a : α} {s : wseq α} :
a s(∀ (b : α) (s' : wseq α), a = b C s'C (wseq.cons b s'))(∀ (s : wseq α), C sC s.think)C s

@[simp]
theorem wseq.mem_think {α : Type u} (s : wseq α) (a : α) :
a s.think a s

theorem 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 wseq.mem_cons_iff {α : Type u} (s : wseq α) (b : α) {a : α} :
a wseq.cons b s a = b a s

theorem wseq.mem_cons_of_mem {α : Type u} {s : wseq α} (b : α) {a : α} :
a sa wseq.cons b s

theorem wseq.mem_cons {α : Type u} (s : wseq α) (a : α) :

theorem wseq.mem_of_mem_tail {α : Type u} {s : wseq α} {a : α} :
a s.taila s

theorem wseq.mem_of_mem_dropn {α : Type u} {s : wseq α} {a : α} {n : } :
a s.drop na s

theorem wseq.nth_mem {α : Type u} {s : wseq α} {a : α} {n : } :
some a s.nth na s

theorem wseq.exists_nth_of_mem {α : Type u} {s : wseq α} {a : α} :
a s(∃ (n : ), some a s.nth n)

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

theorem wseq.lift_rel_dropn_destruct {α : Type u} {β : Type v} {R : α → β → Prop} {s : wseq α} {t : wseq β} (H : wseq.lift_rel R s t) (n : ) :

theorem wseq.exists_of_lift_rel_left {α : Type u} {β : Type v} {R : α → β → Prop} {s : wseq α} {t : wseq β} (H : wseq.lift_rel R s t) {a : α} :
a s(∃ {b : β}, b t R a b)

theorem wseq.exists_of_lift_rel_right {α : Type u} {β : Type v} {R : α → β → Prop} {s : wseq α} {t : wseq β} (H : wseq.lift_rel R s t) {b : β} :
b t(∃ {a : α}, a s R a b)

theorem wseq.head_terminates_of_mem {α : Type u} {s : wseq α} {a : α} :
a s → s.head.terminates

theorem wseq.of_mem_append {α : Type u} {s₁ s₂ : wseq α} {a : α} :
a s₁.append s₂a s₁ a s₂

theorem wseq.mem_append_left {α : Type u} {s₁ s₂ : wseq α} {a : α} :
a s₁a s₁.append s₂

theorem wseq.exists_of_mem_map {α : Type u} {β : Type v} {f : α → β} {b : β} {s : wseq α} :
b wseq.map f s(∃ (a : α), a s f a = b)

@[simp]
theorem wseq.lift_rel_nil {α : Type u} {β : Type v} (R : α → β → Prop) :

@[simp]
theorem wseq.lift_rel_cons {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β) (s : wseq α) (t : wseq β) :

@[simp]
theorem wseq.lift_rel_think_left {α : Type u} {β : Type v} (R : α → β → Prop) (s : wseq α) (t : wseq β) :

@[simp]
theorem wseq.lift_rel_think_right {α : Type u} {β : Type v} (R : α → β → Prop) (s : wseq α) (t : wseq β) :

theorem wseq.cons_congr {α : Type u} {s t : wseq α} (a : α) :
s ~ twseq.cons a s ~ wseq.cons a t

theorem wseq.think_equiv {α : Type u} (s : wseq α) :
s.think ~ s

theorem wseq.think_congr {α : Type u} {s t : wseq α} :
α → s ~ ts.think ~ t.think

theorem wseq.head_congr {α : Type u} {s t : wseq α} :
s ~ ts.head ~ t.head

theorem wseq.flatten_equiv {α : Type u} {c : computation (wseq α)} {s : wseq α} :
s cwseq.flatten c ~ s

theorem wseq.lift_rel_flatten {α : Type u} {β : Type v} {R : α → β → Prop} {c1 : computation (wseq α)} {c2 : computation (wseq β)} :

theorem wseq.flatten_congr {α : Type u} {c1 c2 : computation (wseq α)} :

theorem wseq.tail_congr {α : Type u} {s t : wseq α} :
s ~ ts.tail ~ t.tail

theorem wseq.dropn_congr {α : Type u} {s t : wseq α} (h : s ~ t) (n : ) :
s.drop n ~ t.drop n

theorem wseq.nth_congr {α : Type u} {s t : wseq α} (h : s ~ t) (n : ) :
s.nth n ~ t.nth n

theorem wseq.mem_congr {α : Type u} {s t : wseq α} (h : s ~ t) (a : α) :
a s a t

theorem wseq.productive_congr {α : Type u} {s t : wseq α} :
s ~ t(s.productive t.productive)

theorem wseq.equiv.ext {α : Type u} {s t : wseq α} :
(∀ (n : ), s.nth n ~ t.nth n)s ~ t

theorem wseq.length_eq_map {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.of_list_nil {α : Type u} :

@[simp]
theorem wseq.of_list_cons {α : Type u} (a : α) (l : list α) :

@[simp]
theorem wseq.to_list'_nil {α : Type u} (l : list α) :
computation.corec wseq.to_list._match_2 (l, wseq.nil α) = computation.return l.reverse

@[simp]
theorem wseq.to_list'_cons {α : Type u} (l : list α) (s : wseq α) (a : α) :
computation.corec wseq.to_list._match_2 (l, wseq.cons a s) = (computation.corec wseq.to_list._match_2 (a :: l, s)).think

@[simp]
theorem wseq.to_list'_think {α : Type u} (l : list α) (s : wseq α) :
computation.corec wseq.to_list._match_2 (l, s.think) = (computation.corec wseq.to_list._match_2 (l, s)).think

theorem wseq.to_list'_map {α : Type u} (l : list α) (s : wseq α) :
computation.corec wseq.to_list._match_2 (l, s) = append l.reverse <$> s.to_list

@[simp]
theorem wseq.to_list_cons {α : Type u} (a : α) (s : wseq α) :

theorem wseq.to_list_of_list {α : Type u} (l : list α) :

@[simp]
theorem wseq.destruct_of_seq {α : Type u} (s : seq α) :

@[simp]
theorem wseq.head_of_seq {α : Type u} (s : seq α) :

@[simp]
theorem wseq.tail_of_seq {α : Type u} (s : seq α) :

@[simp]
theorem wseq.dropn_of_seq {α : Type u} (s : seq α) (n : ) :

theorem wseq.nth_of_seq {α : Type u} (s : seq α) (n : ) :

@[instance]
def wseq.productive_of_seq {α : Type u} (s : seq α) :

theorem wseq.to_seq_of_seq {α : Type u} (s : seq α) :

def wseq.ret {α : Type u} :
α → wseq α

The monadic return a is a singleton list containing a.

Equations
@[simp]
theorem wseq.map_nil {α : Type u} {β : Type v} (f : α → β) :

@[simp]
theorem wseq.map_cons {α : Type u} {β : Type v} (f : α → β) (a : α) (s : wseq α) :
wseq.map f (wseq.cons a s) = wseq.cons (f a) (wseq.map f s)

@[simp]
theorem wseq.map_think {α : Type u} {β : Type v} (f : α → β) (s : wseq α) :

@[simp]
theorem wseq.map_id {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.map_ret {α : Type u} {β : Type v} (f : α → β) (a : α) :

@[simp]
theorem wseq.map_append {α : Type u} {β : Type v} (f : α → β) (s t : wseq α) :
wseq.map f (s.append t) = (wseq.map f s).append (wseq.map f t)

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

theorem wseq.mem_map {α : Type u} {β : Type v} (f : α → β) {a : α} {s : wseq α} :
a sf a wseq.map f s

theorem wseq.exists_of_mem_join {α : Type u} {a : α} {S : wseq (wseq α)} :
a S.join(∃ (s : wseq α), s S a s)

theorem wseq.exists_of_mem_bind {α : Type u} {β : Type v} {s : wseq α} {f : α → wseq β} {b : β} :
b s.bind f(∃ (a : α) (H : a s), b f a)

theorem wseq.destruct_map {α : Type u} {β : Type v} (f : α → β) (s : wseq α) :

theorem wseq.lift_rel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : wseq α} {s2 : wseq β} {f1 : α → γ} {f2 : β → δ} :
wseq.lift_rel R s1 s2(∀ {a : α} {b : β}, R a bS (f1 a) (f2 b))wseq.lift_rel S (wseq.map f1 s1) (wseq.map f2 s2)

theorem wseq.map_congr {α : Type u} {β : Type v} (f : α → β) {s t : wseq α} :
s ~ twseq.map f s ~ wseq.map f t

@[simp]
def wseq.destruct_append.aux {α : Type u} :
wseq αoption × wseq α)computation (option × wseq α))

Equations
theorem wseq.destruct_append {α : Type u} (s t : wseq α) :

theorem wseq.lift_rel_append {α : Type u} {β : Type v} (R : α → β → Prop) {s1 s2 : wseq α} {t1 t2 : wseq β} :
wseq.lift_rel R s1 t1wseq.lift_rel R s2 t2wseq.lift_rel R (s1.append s2) (t1.append t2)

theorem wseq.lift_rel_join.lem {α : Type u} {β : Type v} (R : α → β → Prop) {S : wseq (wseq α)} {T : wseq (wseq β)} {U : wseq αwseq β → Prop} (ST : wseq.lift_rel (wseq.lift_rel R) S T) (HU : ∀ (s1 : wseq α) (s2 : wseq β), (∃ (s : wseq α) (t : wseq β) (S : wseq (wseq α)) (T : wseq (wseq β)), s1 = s.append S.join s2 = t.append T.join wseq.lift_rel R s t wseq.lift_rel (wseq.lift_rel R) S T)U s1 s2) {a : option × wseq α)} :
a S.join.destruct(∃ {b : option × wseq β)}, b T.join.destruct wseq.lift_rel_o R U a b)

theorem wseq.lift_rel_join {α : Type u} {β : Type v} (R : α → β → Prop) {S : wseq (wseq α)} {T : wseq (wseq β)} :

theorem wseq.join_congr {α : Type u} {S T : wseq (wseq α)} :

theorem wseq.lift_rel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : wseq α} {s2 : wseq β} {f1 : α → wseq γ} {f2 : β → wseq δ} :
wseq.lift_rel R s1 s2(∀ {a : α} {b : β}, R a bwseq.lift_rel S (f1 a) (f2 b))wseq.lift_rel S (s1.bind f1) (s2.bind f2)

theorem wseq.bind_congr {α : Type u} {β : Type v} {s1 s2 : wseq α} {f1 f2 : α → wseq β} :
s1 ~ s2(∀ (a : α), f1 a ~ f2 a)s1.bind f1 ~ s2.bind f2

@[simp]
theorem wseq.join_ret {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.join_map_ret {α : Type u} (s : wseq α) :

@[simp]
theorem wseq.join_append {α : Type u} (S T : wseq (wseq α)) :

@[simp]
theorem wseq.bind_ret {α : Type u} {β : Type v} (f : α → β) (s : wseq α) :

@[simp]
theorem wseq.ret_bind {α : Type u} {β : Type v} (a : α) (f : α → wseq β) :
(wseq.ret a).bind f ~ f a

@[simp]
theorem wseq.map_join {α : Type u} {β : Type v} (f : α → β) (S : wseq (wseq α)) :

@[simp]
theorem wseq.join_join {α : Type u} (SS : wseq (wseq (wseq α))) :

@[simp]
theorem wseq.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : wseq α) (f : α → wseq β) (g : β → wseq γ) :
(s.bind f).bind g ~ s.bind (λ (x : α), (f x).bind g)

@[instance]

Equations