Definitions on lazy lists #
This file contains various definitions and proofs on lazy lists.
TODO: move the LazyList.lean
file from core to mathlib.
Isomorphism between strict and lazy lists.
Equations
- LazyList.listEquivLazyList α = { toFun := LazyList.ofList, invFun := LazyList.toList, left_inv := ⋯, right_inv := ⋯ }
Instances For
Equations
- LazyList.nil.decidableEq LazyList.nil = isTrue ⋯
- (LazyList.cons x_2 xs).decidableEq (LazyList.cons y ys) = if h : x_2 = y then match xs.get.decidableEq ys.get with | isFalse h2 => isFalse ⋯ | isTrue h2 => isTrue ⋯ else isFalse ⋯
- LazyList.nil.decidableEq (LazyList.cons hd tl) = isFalse ⋯
- (LazyList.cons hd tl).decidableEq LazyList.nil = isFalse ⋯
Traversal of lazy lists using an applicative effect.
Equations
- LazyList.traverse f LazyList.nil = pure LazyList.nil
- LazyList.traverse f (LazyList.cons x_1 xs) = Seq.seq (LazyList.cons <$> f x_1) fun (x : Unit) => Thunk.pure <$> LazyList.traverse f xs.get
Instances For
Equations
init xs
, if xs
non-empty, drops the last element of the list.
Otherwise, return the empty list.
Equations
- LazyList.nil.init = LazyList.nil
- (LazyList.cons x_1 xs).init = match xs.get with | LazyList.nil => LazyList.nil | LazyList.cons hd tl => LazyList.cons x_1 { fn := fun (x : Unit) => xs.get.init }
Instances For
Return the first object contained in the list that satisfies
predicate p
Equations
- LazyList.find p LazyList.nil = none
- LazyList.find p (LazyList.cons x_1 xs) = if p x_1 then some x_1 else LazyList.find p xs.get
Instances For
interleave xs ys
creates a list where elements of xs
and ys
alternate.
Equations
- LazyList.nil.interleave x = x
- (LazyList.cons hd tl).interleave LazyList.nil = LazyList.cons hd tl
- (LazyList.cons x_2 xs).interleave (LazyList.cons y ys) = LazyList.cons x_2 { fn := fun (x : Unit) => LazyList.cons y { fn := fun (x : Unit) => xs.get.interleave ys.get } }
Instances For
interleaveAll (xs::ys::zs::xss)
creates a list where elements of xs
, ys
and zs
and the rest alternate. Every other element of the resulting list is taken from
xs
, every fourth is taken from ys
, every eighth is taken from zs
and so on.
Equations
- LazyList.interleaveAll [] = LazyList.nil
- LazyList.interleaveAll (x_1 :: xs) = x_1.interleave (LazyList.interleaveAll xs)
Instances For
Reverse the order of a LazyList
.
It is done by converting to a List
first because reversal involves evaluating all
the list and if the list is all evaluated, List
is a better representation for
it than a series of thunks.
Equations
- xs.reverse = LazyList.ofList xs.toList.reverse
Instances For
Equations
- LazyList.instMonad_mathlib = Monad.mk
Equations
Try applying function f
to every element of a LazyList
and
return the result of the first attempt that succeeds.
Equations
- LazyList.mfirst f LazyList.nil = failure
- LazyList.mfirst f (LazyList.cons x_1 xs) = HOrElse.hOrElse (f x_1) fun (x : Unit) => LazyList.mfirst f xs.get
Instances For
Membership in lazy lists
Equations
- LazyList.Mem x LazyList.nil = False
- LazyList.Mem x (LazyList.cons x_2 xs) = (x = x_2 ∨ LazyList.Mem x xs.get)
Instances For
Equations
- LazyList.instMembership_mathlib = { mem := LazyList.Mem }
Equations
- One or more equations did not get rendered due to their size.
- LazyList.Mem.decidable x LazyList.nil = isFalse ⋯
map for partial functions #
Partial map. If f : ∀ a, p a → β
is a partial function defined on
a : α
satisfying p
, then pmap f l h
is essentially the same as map f l
but is defined only when all members of l
satisfy p
, using the proof
to apply f
.
Equations
- LazyList.pmap f LazyList.nil x_2 = LazyList.nil
- LazyList.pmap f (LazyList.cons x_2 xs) H = LazyList.cons (f x_2 ⋯) { fn := fun (x : Unit) => LazyList.pmap f xs.get ⋯ }
Instances For
"Attach" the proof that the elements of l
are in l
to produce a new LazyList
with the same elements but in the type {x // x ∈ l}
.
Equations
- l.attach = LazyList.pmap Subtype.mk l ⋯