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.
Turn a sequence into a weak sequence
Equations
Turn a list into a weak sequence
Equations
Turn a stream into a weak sequence
Equations
@[instance]
Equations
- wseq.coe_seq = {coe := wseq.of_seq α}
@[instance]
Equations
- wseq.coe_list = {coe := wseq.of_list α}
@[instance]
Equations
- wseq.coe_stream = {coe := wseq.of_stream α}
@[instance]
Equations
- wseq.inhabited = {default := wseq.nil α}
Prepend an element to a weak sequence
Equations
- wseq.cons a = seq.cons (option.some a)
Compute for one tick, without producing any elements
Equations
Destruct a weak sequence, to (eventually possibly) produce either
none for nil or some (a, s) if an element is produced.
Equations
- wseq.destruct = computation.corec (λ (s : wseq α), wseq.destruct._match_1 (seq.destruct s))
- wseq.destruct._match_1 (option.some (option.some a, s')) = sum.inl (option.some (a, s'))
- wseq.destruct._match_1 (option.some (option.none α, s')) = sum.inr s'
- wseq.destruct._match_1 option.none = sum.inl option.none
@[instance]
Equations
- wseq.has_mem = {mem := wseq.mem α}
Get the head of a weak sequence. This involves a possibly infinite computation.
Equations
Encode a computation yielding a weak sequence into additional
think constructors in a weak sequence
Equations
- wseq.flatten = seq.corec (λ (c : computation (wseq α)), wseq.flatten._match_1 c.destruct)
- wseq.flatten._match_1 (sum.inr c') = option.some (option.none α, c')
- wseq.flatten._match_1 (sum.inl s) = seq.omap return (seq.destruct s)
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.
Convert s to a list (if it is finite and completes in finite time).
Equations
- s.to_list = computation.corec (λ (_x : list α × wseq α), wseq.to_list._match_2 _x) (list.nil α, s)
- wseq.to_list._match_2 (l, s) = wseq.to_list._match_1 l (seq.destruct s)
- wseq.to_list._match_1 l (option.some (option.some a, s')) = sum.inr (a :: l, s')
- wseq.to_list._match_1 l (option.some (option.none α, s')) = sum.inr (l, s')
- wseq.to_list._match_1 l option.none = sum.inl l.reverse
Get the length of s (if it is finite and completes in finite time).
Equations
- s.length = computation.corec (λ (_x : ℕ × wseq α), wseq.length._match_2 _x) (0, s)
- wseq.length._match_2 (n, s) = wseq.length._match_1 n (seq.destruct s)
- wseq.length._match_1 n (option.some (option.some a, s')) = sum.inr (n + 1, s')
- wseq.length._match_1 n (option.some (option.none α, s')) = sum.inr (n, s')
- wseq.length._match_1 n option.none = sum.inl n
@[class]
A weak sequence is finite if to_list s terminates. Equivalently,
it is a finite number of think and cons applied to nil.
Equations
- s.is_finite = s.to_list.terminates
@[instance]
Equations
- _ = h
@[class]
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
- s.productive = ∀ (n : ℕ), (s.nth n).terminates
@[instance]
def
wseq.nth_terminates
{α : Type u}
(s : wseq α)
[h : s.productive]
(n : ℕ) :
(s.nth n).terminates
Equations
- _ = h
@[instance]
Equations
- _ = _
Replace the nth element of s with a.
Equations
- s.update_nth n a = seq.corec (λ (_x : ℕ × wseq α), wseq.update_nth._match_2 a _x) (n + 1, s)
- wseq.update_nth._match_2 a (n, s) = wseq.update_nth._match_1 a (seq.destruct s) n
- wseq.update_nth._match_1 a (option.some (option.some a', s')) (n + 2) = option.some (option.some a', n + 1, s')
- wseq.update_nth._match_1 a (option.some (option.some a', s')) 1 = option.some (option.some a, 0, s')
- wseq.update_nth._match_1 a (option.some (option.some a', s')) 0 = option.some (option.some a', 0, s')
- wseq.update_nth._match_1 a (option.some (option.none α, s')) n = option.some (option.none α, n, s')
- wseq.update_nth._match_1 a option.none n = option.none
Remove the nth element of s.
Equations
- s.remove_nth n = seq.corec (λ (_x : ℕ × wseq α), wseq.remove_nth._match_2 _x) (n + 1, s)
- wseq.remove_nth._match_2 (n, s) = wseq.remove_nth._match_1 (seq.destruct s) n
- wseq.remove_nth._match_1 (option.some (option.some a', s')) (n + 2) = option.some (option.some a', n + 1, s')
- wseq.remove_nth._match_1 (option.some (option.some a', s')) 1 = option.some (option.none α, 0, s')
- wseq.remove_nth._match_1 (option.some (option.some a', s')) 0 = option.some (option.some a', 0, s')
- wseq.remove_nth._match_1 (option.some (option.none α, s')) n = option.some (option.none α, n, s')
- wseq.remove_nth._match_1 option.none n = option.none
Map the elements of s over f, removing any values that yield none.
Equations
- wseq.filter_map f = seq.corec (λ (s : wseq α), wseq.filter_map._match_1 f (seq.destruct s))
- wseq.filter_map._match_1 f (option.some (option.some a, s')) = option.some (f a, s')
- wseq.filter_map._match_1 f (option.some (option.none α, s')) = option.some (option.none β, s')
- wseq.filter_map._match_1 f option.none = option.none
Select the elements of s that satisfy p.
Equations
- wseq.filter p = wseq.filter_map (λ (a : α), ite (p a) (option.some a) option.none)
Get the first element of s satisfying p.
Equations
- wseq.find p s = (wseq.filter p s).head
Zip a function over two weak sequences
Equations
- wseq.zip_with f s1 s2 = seq.corec (λ (_x : wseq α × wseq β), wseq.zip_with._match_2 f _x) (s1, s2)
- wseq.zip_with._match_2 f (s1, s2) = wseq.zip_with._match_1 f s1 s2 (seq.destruct s1) (seq.destruct s2)
- wseq.zip_with._match_1 f s1 s2 (option.some (option.some a1, s1')) (option.some (option.some a2, s2')) = option.some (option.some (f a1 a2), s1', s2')
- wseq.zip_with._match_1 f s1 s2 (option.some (option.some a1, s1')) (option.some (option.none β, s2')) = option.some (option.none γ, s1, s2')
- wseq.zip_with._match_1 f s1 s2 (option.some (option.some val, snd)) option.none = option.none
- wseq.zip_with._match_1 f s1 s2 (option.some (option.none α, s1')) (option.some (option.some a2, s2')) = option.some (option.none γ, s1', s2)
- wseq.zip_with._match_1 f s1 s2 (option.some (option.none α, s1')) (option.some (option.none β, s2')) = option.some (option.none γ, s1', s2')
- wseq.zip_with._match_1 f s1 s2 (option.some (option.none α, snd)) option.none = option.none
- wseq.zip_with._match_1 f s1 s2 option.none _x = option.none
Get the list of indexes of elements of s satisfying p
Equations
- wseq.find_indexes p s = wseq.filter_map (λ (_x : α × ℕ), wseq.find_indexes._match_1 p _x) (s.zip ↑stream.nats)
- wseq.find_indexes._match_1 p (a, n) = ite (p a) (option.some n) option.none
Get the index of the first element of s satisfying p
Equations
- wseq.find_index p s = (λ (o : option ℕ), o.get_or_else 0) <$> (wseq.find_indexes p s).head
Get the index of the first occurrence of a in s
Equations
- wseq.index_of a = wseq.find_index (eq a)
Get the indexes of occurrences of a in s
Equations
- wseq.indexes_of a = wseq.find_indexes (eq a)
union s1 s2 is a weak sequence which interleaves s1 and s2 in
some order (nondeterministically).
Equations
- s1.union s2 = seq.corec (λ (_x : wseq α × wseq α), wseq.union._match_2 _x) (s1, s2)
- wseq.union._match_2 (s1, s2) = wseq.union._match_1 (seq.destruct s1) (seq.destruct s2)
- wseq.union._match_1 (option.some (option.some a1, s1')) (option.some (option.some a2, s2')) = option.some (option.some a1, wseq.cons a2 s1', s2')
- wseq.union._match_1 (option.some (option.some a1, s1')) (option.some (option.none α, s2')) = option.some (option.some a1, s1', s2')
- wseq.union._match_1 (option.some (option.some val, s1')) option.none = option.some (option.some val, s1', wseq.nil α)
- wseq.union._match_1 (option.some (option.none α, s1')) (option.some (option.some a2, s2')) = option.some (option.some a2, s1', s2')
- wseq.union._match_1 (option.some (option.none α, s1')) (option.some (option.none α, s2')) = option.some (option.none α, s1', s2')
- wseq.union._match_1 (option.some (option.none α, s1')) option.none = option.some (option.none α, s1', wseq.nil α)
- wseq.union._match_1 option.none (option.some (a2, s2')) = option.some (a2, wseq.nil α, s2')
- wseq.union._match_1 option.none option.none = option.none
Returns tt if s is nil and ff if s has an element
Equations
Calculate one step of computation
Equations
- s.compute = wseq.compute._match_1 s (seq.destruct s)
- wseq.compute._match_1 s (option.some (option.some val, snd)) = s
- wseq.compute._match_1 s (option.some (option.none α, s')) = s'
- wseq.compute._match_1 s option.none = s
Get the first n elements of a weak sequence
Equations
- s.take n = seq.corec (λ (_x : ℕ × wseq α), wseq.take._match_2 _x) (n, s)
- wseq.take._match_2 (n, s) = wseq.take._match_1 n (seq.destruct s)
- wseq.take._match_1 (m + 1) (option.some (option.some a, s')) = option.some (option.some a, m, s')
- wseq.take._match_1 (m + 1) (option.some (option.none α, s')) = option.some (option.none α, m + 1, s')
- wseq.take._match_1 (m + 1) option.none = option.none
- wseq.take._match_1 0 _x = option.none
Split the sequence at position n into a finite initial segment
and the weak sequence tail
Equations
- s.split_at n = computation.corec (λ (_x : ℕ × list α × wseq α), wseq.split_at._match_2 _x) (n, list.nil α, s)
- wseq.split_at._match_2 (n, l, s) = wseq.split_at._match_1 n l s n (seq.destruct s)
- wseq.split_at._match_1 n l s (m + 1) (option.some (option.some a, s')) = sum.inr (m, a :: l, s')
- wseq.split_at._match_1 n l s (m + 1) (option.some (option.none α, s')) = sum.inr (n, l, s')
- wseq.split_at._match_1 n l s (m + 1) option.none = sum.inl (l.reverse, s)
- wseq.split_at._match_1 n l s 0 _x = sum.inl (l.reverse, s)
Returns tt if any element of s satisfies p
Equations
- s.any p = computation.corec (λ (s : wseq α), wseq.any._match_1 p (seq.destruct s)) s
- wseq.any._match_1 p (option.some (option.some a, s')) = ite ↥(p a) (sum.inl bool.tt) (sum.inr s')
- wseq.any._match_1 p (option.some (option.none α, s')) = sum.inr s'
- wseq.any._match_1 p option.none = sum.inl bool.ff
Returns tt if every element of s satisfies p
Equations
- s.all p = computation.corec (λ (s : wseq α), wseq.all._match_1 p (seq.destruct s)) s
- wseq.all._match_1 p (option.some (option.some a, s')) = ite ↥(p a) (sum.inr s') (sum.inl bool.ff)
- wseq.all._match_1 p (option.some (option.none α, s')) = sum.inr s'
- wseq.all._match_1 p option.none = sum.inl bool.tt
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
- wseq.scanl f a s = wseq.cons a (seq.corec (λ (_x : α × wseq β), wseq.scanl._match_2 f _x) (a, s))
- wseq.scanl._match_2 f (a, s) = wseq.scanl._match_1 f a (seq.destruct s)
- wseq.scanl._match_1 f a (option.some (option.some b, s')) = let a' : α := f a b in option.some (option.some a', a', s')
- wseq.scanl._match_1 f a (option.some (option.none β, s')) = option.some (option.none α, a, s')
- wseq.scanl._match_1 f a option.none = option.none
Get the weak sequence of initial segments of the input sequence
Equations
- s.inits = wseq.cons list.nil (seq.corec (λ (_x : dlist α × wseq α), wseq.inits._match_2 _x) (dlist.empty α, s))
- wseq.inits._match_2 (l, s) = wseq.inits._match_1 l (seq.destruct s)
- wseq.inits._match_1 l (option.some (option.some a, s')) = let l' : dlist α := dlist.concat a l in option.some (option.some l'.to_list, l', s')
- wseq.inits._match_1 l (option.some (option.none α, s')) = option.some (option.none (list α), l, s')
- wseq.inits._match_1 l option.none = option.none
Like take, but does not wait for a result. Calculates n steps of
computation and returns the sequence computed so far
Equations
- s.collect n = list.filter_map id (seq.take n s)
Append two weak sequences. As with seq.append, this may not use
the second sequence if the first one takes forever to compute
Equations
Flatten a sequence of weak sequences. (Note that this allows
empty sequences, unlike seq.join.)
Equations
- S.join = ((λ (o : option (wseq α)), wseq.join._match_1 o) <$> S).join
- wseq.join._match_1 (option.some s) = (option.none α, s)
- wseq.join._match_1 option.none = seq1.ret option.none
@[simp]
Equations
- wseq.lift_rel_o R C (option.some (a, s)) (option.some (b, t)) = (R a b ∧ C s t)
- wseq.lift_rel_o R C (option.some (fst, snd)) option.none = false
- wseq.lift_rel_o R C option.none (option.some val) = false
- wseq.lift_rel_o R C option.none option.none = true
theorem
wseq.lift_rel_o.imp
{α : Type u}
{β : Type v}
{R S : α → β → Prop}
{C D : wseq α → wseq β → Prop}
(H1 : ∀ (a : α) (b : β), R a b → S a b)
(H2 : ∀ (s : wseq α) (t : wseq β), C s t → D s t)
{o : option (α × wseq α)}
{p : option (β × wseq β)} :
wseq.lift_rel_o R C o p → wseq.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 t → D s t)
{o : option (α × wseq α)}
{p : option (β × wseq β)} :
wseq.lift_rel_o R C o p → wseq.lift_rel_o R D o p
theorem
wseq.bisim_o.imp
{α : Type u}
{R S : wseq α → wseq α → Prop}
(H : ∀ (s t : wseq α), R s t → S s t)
{o p : option (α × wseq α)} :
wseq.bisim_o R o p → wseq.bisim_o S o p
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
- wseq.lift_rel R s t = ∃ (C : wseq α → wseq β → Prop), C s t ∧ ∀ {s : wseq α} {t : wseq β}, C s t → computation.lift_rel (wseq.lift_rel_o R C) s.destruct t.destruct
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 β} :
wseq.lift_rel R s t → computation.lift_rel (wseq.lift_rel_o R (wseq.lift_rel R)) s.destruct t.destruct
theorem
wseq.lift_rel_destruct_iff
{α : Type u}
{β : Type v}
{R : α → β → Prop}
{s : wseq α}
{t : wseq β} :
wseq.lift_rel R s t ↔ computation.lift_rel (wseq.lift_rel_o R (wseq.lift_rel R)) s.destruct t.destruct
theorem
wseq.destruct_congr
{α : Type u}
{s t : wseq α} :
s ~ t → computation.lift_rel (wseq.bisim_o wseq.equiv) s.destruct t.destruct
theorem
wseq.destruct_congr_iff
{α : Type u}
{s t : wseq α} :
s ~ t ↔ computation.lift_rel (wseq.bisim_o wseq.equiv) s.destruct t.destruct
theorem
wseq.lift_rel.refl
{α : Type u}
(R : α → α → Prop) :
reflexive R → reflexive (wseq.lift_rel R)
theorem
wseq.lift_rel_o.swap
{α : Type u}
{β : Type v}
(R : α → β → Prop)
(C : wseq α → wseq β → Prop) :
function.swap (wseq.lift_rel_o R C) = wseq.lift_rel_o (function.swap R) (function.swap C)
theorem
wseq.lift_rel.swap_lem
{α : Type u}
{β : Type v}
{R : α → β → Prop}
{s1 : wseq α}
{s2 : wseq β} :
wseq.lift_rel R s1 s2 → wseq.lift_rel (function.swap R) s2 s1
theorem
wseq.lift_rel.symm
{α : Type u}
(R : α → α → Prop) :
symmetric R → symmetric (wseq.lift_rel R)
theorem
wseq.lift_rel.trans
{α : Type u}
(R : α → α → Prop) :
transitive R → transitive (wseq.lift_rel R)
theorem
wseq.lift_rel.equiv
{α : Type u}
(R : α → α → Prop) :
equivalence R → equivalence (wseq.lift_rel R)
@[simp]
@[simp]
theorem
wseq.destruct_cons
{α : Type u}
(a : α)
(s : wseq α) :
(wseq.cons a s).destruct = computation.return (option.some (a, s))
@[simp]
theorem
wseq.seq_destruct_cons
{α : Type u}
(a : α)
(s : wseq α) :
seq.destruct (wseq.cons a s) = option.some (option.some a, s)
@[simp]
theorem
wseq.seq_destruct_think
{α : Type u}
(s : wseq α) :
seq.destruct s.think = option.some (option.none α, s)
@[simp]
theorem
wseq.head_cons
{α : Type u}
(a : α)
(s : wseq α) :
(wseq.cons a s).head = computation.return (option.some a)
@[simp]
@[simp]
theorem
wseq.flatten_think
{α : Type u}
(c : computation (wseq α)) :
wseq.flatten c.think = (wseq.flatten c).think
@[simp]
theorem
wseq.destruct_flatten
{α : Type u}
(c : computation (wseq α)) :
(wseq.flatten c).destruct = c >>= wseq.destruct
@[simp]
Equations
@[simp]
Equations
- wseq.drop.aux (n + 1) = λ (a : option (α × wseq α)), wseq.tail.aux a >>= wseq.drop.aux n
- wseq.drop.aux 0 = computation.return
theorem
wseq.head_terminates_of_head_tail_terminates
{α : Type u}
(s : wseq α)
[T : s.tail.head.terminates] :
theorem
wseq.destruct_some_of_destruct_tail_some
{α : Type u}
{s : wseq α}
{a : α × wseq α} :
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 : α} :
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 : ℕ} :
option.some a ∈ s.nth n → (∃ (a' : α), option.some a' ∈ s.head)
@[instance]
Equations
- _ = _
@[instance]
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 : ℕ} :
(s.nth n).terminates → s.head.terminates
theorem
wseq.destruct_terminates_of_nth_terminates
{α : Type u}
{s : wseq α}
{n : ℕ} :
(s.nth n).terminates → s.destruct.terminates
theorem
wseq.exists_nth_of_mem
{α : Type u}
{s : wseq α}
{a : α} :
a ∈ s → (∃ (n : ℕ), option.some a ∈ s.nth n)
theorem
wseq.lift_rel_dropn_destruct
{α : Type u}
{β : Type v}
{R : α → β → Prop}
{s : wseq α}
{t : wseq β}
(H : wseq.lift_rel R s t)
(n : ℕ) :
computation.lift_rel (wseq.lift_rel_o R (wseq.lift_rel R)) (s.drop n).destruct (t.drop n).destruct
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 : α} :
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 : β} :
@[simp]
@[simp]
theorem
wseq.lift_rel_cons
{α : Type u}
{β : Type v}
(R : α → β → Prop)
(a : α)
(b : β)
(s : wseq α)
(t : wseq β) :
wseq.lift_rel R (wseq.cons a s) (wseq.cons b t) ↔ R a b ∧ wseq.lift_rel R s t
@[simp]
theorem
wseq.lift_rel_think_left
{α : Type u}
{β : Type v}
(R : α → β → Prop)
(s : wseq α)
(t : wseq β) :
wseq.lift_rel R s.think t ↔ wseq.lift_rel R s t
@[simp]
theorem
wseq.lift_rel_think_right
{α : Type u}
{β : Type v}
(R : α → β → Prop)
(s : wseq α)
(t : wseq β) :
wseq.lift_rel R s t.think ↔ wseq.lift_rel R s t
theorem
wseq.flatten_equiv
{α : Type u}
{c : computation (wseq α)}
{s : wseq α} :
s ∈ c → wseq.flatten c ~ s
theorem
wseq.lift_rel_flatten
{α : Type u}
{β : Type v}
{R : α → β → Prop}
{c1 : computation (wseq α)}
{c2 : computation (wseq β)} :
computation.lift_rel (wseq.lift_rel R) c1 c2 → wseq.lift_rel R (wseq.flatten c1) (wseq.flatten c2)
theorem
wseq.flatten_congr
{α : Type u}
{c1 c2 : computation (wseq α)} :
computation.lift_rel wseq.equiv c1 c2 → wseq.flatten c1 ~ wseq.flatten c2
@[simp]
theorem
wseq.of_list_cons
{α : Type u}
(a : α)
(l : list α) :
wseq.of_list (a :: l) = wseq.cons a (wseq.of_list l)
@[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]
@[simp]
theorem
wseq.destruct_of_seq
{α : Type u}
(s : seq α) :
(wseq.of_seq s).destruct = computation.return (option.map (λ (a : α), (a, wseq.of_seq s.tail)) s.head)
@[simp]
theorem
wseq.head_of_seq
{α : Type u}
(s : seq α) :
(wseq.of_seq s).head = computation.return s.head
@[simp]
@[simp]
theorem
wseq.dropn_of_seq
{α : Type u}
(s : seq α)
(n : ℕ) :
(wseq.of_seq s).drop n = wseq.of_seq (s.drop n)
theorem
wseq.nth_of_seq
{α : Type u}
(s : seq α)
(n : ℕ) :
(wseq.of_seq s).nth n = computation.return (s.nth n)
@[instance]
Equations
- _ = _
theorem
wseq.destruct_map
{α : Type u}
{β : Type v}
(f : α → β)
(s : wseq α) :
(wseq.map f s).destruct = computation.map (option.map (prod.map f (wseq.map f))) s.destruct
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 b → S (f1 a) (f2 b)) → wseq.lift_rel S (wseq.map f1 s1) (wseq.map f2 s2)
@[simp]
Equations
- wseq.destruct_append.aux t (option.some (a, s)) = computation.return (option.some (a, s.append t))
- wseq.destruct_append.aux t option.none = t.destruct
theorem
wseq.lift_rel_append
{α : Type u}
{β : Type v}
(R : α → β → Prop)
{s1 s2 : wseq α}
{t1 t2 : wseq β} :
wseq.lift_rel R s1 t1 → 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 α)} :
theorem
wseq.lift_rel_join
{α : Type u}
{β : Type v}
(R : α → β → Prop)
{S : wseq (wseq α)}
{T : wseq (wseq β)} :
wseq.lift_rel (wseq.lift_rel R) S T → wseq.lift_rel R S.join T.join
theorem
wseq.join_congr
{α : Type u}
{S T : wseq (wseq α)} :
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 δ} :
wseq.lift_rel R s1 s2 → (∀ {a : α} {b : β}, R a b → wseq.lift_rel S (f1 a) (f2 b)) → wseq.lift_rel S (s1.bind f1) (s2.bind f2)