mathlib documentation

data.seq.wseq

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

Turn a sequence into a weak sequence

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

Turn a list into a weak sequence

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

Turn a stream into a weak sequence

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

The empty weak sequence

Equations
@[protected, instance]
def wseq.inhabited {α : Type u} :
Equations
def wseq.cons {α : Type u} (a : α) :
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 α) (h1 : C wseq.nil) (h2 : Π (x : α) (s : wseq α), C (wseq.cons x s)) (h3 : Π (s : wseq α), C s.think) :
C s
Equations
@[protected]
def wseq.mem {α : Type u} (a : α) (s : wseq α) :
Prop
Equations
@[protected, instance]
def wseq.has_mem {α : Type u} :
has_mem α (wseq α)
Equations
theorem wseq.not_mem_nil {α : Type u} (a : α) :
def wseq.head {α : Type u} (s : wseq α) :

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

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

drop the first n elements from s.

Equations
Instances for wseq.drop
def wseq.nth {α : Type u} (s : wseq α) (n : ) :

Get the nth element of s.

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

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

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

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

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

@[protected, 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]
structure wseq.productive {α : Type u} (s : 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
theorem wseq.productive_iff {α : Type u} (s : wseq α) :
s.productive ∀ (n : ), (s.nth n).terminates
@[protected, instance]
def wseq.nth_terminates {α : Type u} (s : wseq α) [h : s.productive] (n : ) :
@[protected, instance]
def wseq.head_terminates {α : Type u} (s : wseq α) [s.productive] :
def wseq.update_nth {α : Type u} (s : wseq α) (n : ) (a : α) :
wseq α

Replace the nth element of s with a.

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

Remove the nth element of s.

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

Get the first element of s satisfying p.

Equations
def wseq.zip_with {α : Type u} {β : Type v} {γ : Type w} (f : α → β → γ) (s1 : wseq α) (s2 : 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] (s : wseq α) :

Get the list of indexes of elements of s satisfying p

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

Get the index of the first element of s satisfying p

Equations
def wseq.index_of {α : Type u} [decidable_eq α] (a : α) :

Get the index of the first occurrence of a in s

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

Get the indexes of occurrences of a in s

Equations
def wseq.union {α : Type u} (s1 s2 : 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} (s : wseq α) :

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

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

Calculate one step of computation

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

Get the first n elements of a weak sequence

Equations
def wseq.split_at {α : Type u} (s : wseq α) (n : ) :

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

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

Returns tt if any element of s satisfies p

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

Returns tt if every element of s satisfies p

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

Get the weak sequence of initial segments of the input sequence

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

Map a function over a weak sequence

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

Monadic bind operator for weak sequences

Equations
@[simp]
def wseq.lift_rel_o {α : Type u} {β : Type v} (R : α → β → Prop) (C : 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} (R : 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} (R : α → β → Prop) (s : wseq α) (t : 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) (H : reflexive R) :
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 β} (h : wseq.lift_rel R s1 s2) :
theorem wseq.lift_rel.swap {α : Type u} {β : Type v} (R : α → β → Prop) :
theorem wseq.lift_rel.symm {α : Type u} (R : α → α → Prop) (H : symmetric R) :
theorem wseq.lift_rel.trans {α : Type u} (R : α → α → Prop) (H : transitive R) :
theorem wseq.lift_rel.equiv {α : Type u} (R : α → α → Prop) :
@[refl]
theorem wseq.equiv.refl {α : Type u} (s : wseq α) :
s ~ s
@[symm]
theorem wseq.equiv.symm {α : Type u} {s t : wseq α} :
s ~ tt ~ s
@[trans]
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]
@[simp]
theorem wseq.seq_destruct_cons {α : Type u} (a : α) (s : wseq α) :
@[simp]
theorem wseq.seq_destruct_think {α : Type u} (s : wseq α) :
@[simp]
@[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)
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 α} (h : option.some a s.tail.destruct) :
∃ (a' : α × wseq α), option.some a' s.destruct
theorem wseq.head_some_of_head_tail_some {α : Type u} {s : wseq α} {a : α} (h : option.some a s.tail.head) :
∃ (a' : α), option.some a' s.head
theorem wseq.head_some_of_nth_some {α : Type u} {s : wseq α} {a : α} {n : } (h : option.some a s.nth n) :
∃ (a' : α), option.some a' s.head
@[protected, instance]
def wseq.productive_tail {α : Type u} (s : wseq α) [s.productive] :
@[protected, 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 : } (h : 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 : } (T : (s.nth n).terminates) :
theorem wseq.mem_rec_on {α : Type u} {C : wseq α → Prop} {a : α} {s : wseq α} (M : a s) (h1 : ∀ (b : α) (s' : wseq α), a = b C s'C (wseq.cons b s')) (h2 : ∀ (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 α} :
option.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 : α} (h : a 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 : } :
option.some a s.nth na s
theorem wseq.exists_nth_of_mem {α : Type u} {s : wseq α} {a : α} (h : a s) :
∃ (n : ), option.some a s.nth n
theorem wseq.exists_dropn_of_mem {α : Type u} {s : wseq α} {a : α} (h : a s) :
∃ (n : ) (s' : wseq α), option.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 : α} (h : 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 : β} (h : b t) :
∃ {a : α}, a s R a b
theorem wseq.head_terminates_of_mem {α : Type u} {s : wseq α} {a : α} (h : a s) :
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 : α) (h : s ~ t) :
theorem wseq.think_equiv {α : Type u} (s : wseq α) :
s.think ~ s
theorem wseq.think_congr {α : Type u} {s t : wseq α} (a : α) (h : s ~ t) :
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 α} (h : s c) :
theorem wseq.lift_rel_flatten {α : Type u} {β : Type v} {R : α → β → Prop} {c1 : computation (wseq α)} {c2 : computation (wseq β)} (h : computation.lift_rel (wseq.lift_rel R) c1 c2) :
theorem wseq.flatten_congr {α : Type u} {c1 c2 : computation (wseq α)} :
theorem wseq.tail_congr {α : Type u} {s t : wseq α} (h : s ~ t) :
s.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 α} (h : s ~ t) :
theorem wseq.equiv.ext {α : Type u} {s t : wseq α} (h : ∀ (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) = has_append.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 : ) :
@[protected, 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} (a : α) :
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 : β} (h : 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 : β → δ} (h1 : wseq.lift_rel R s1 s2) (h2 : ∀ {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 α} (h : s ~ t) :
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 β} (h1 : wseq.lift_rel R s1 t1) (h2 : wseq.lift_rel R s2 t2) :
wseq.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 α)} (ma : 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 β)} (h : wseq.lift_rel (wseq.lift_rel R) S T) :
theorem wseq.join_congr {α : Type u} {S T : wseq (wseq α)} (h : wseq.lift_rel wseq.equiv S T) :
S.join ~ T.join
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 δ} (h1 : wseq.lift_rel R s1 s2) (h2 : ∀ {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 β} (h1 : s1 ~ s2) (h2 : ∀ (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)
@[protected, instance]
Equations