Definitions on lazy lists

This file contains various definitions and proofs on lazy lists.

TODO: move the LazyList.lean file from core to mathlib.

def LazyList.listEquivLazyList (α : Type u_1) : List α ≃ LazyList α

Isomorphism between strict and lazy lists.

instance LazyList.decidableEq {α : Type u} [DecidableEq α] : DecidableEq (LazyList α)

Equations

• One or more equations did not get rendered due to their size.
• LazyList.decidableEq LazyList.nil LazyList.nil = isTrue (_ : LazyList.nil = LazyList.nil)
• LazyList.decidableEq LazyList.nil (LazyList.cons hd tl) = isFalse (_ : ¬LazyList.nil = LazyList.cons hd tl)
• LazyList.decidableEq (LazyList.cons hd tl) LazyList.nil = isFalse (_ : ¬LazyList.cons hd tl = LazyList.nil)

def LazyList.traverse {m : Type u → Type u} [Applicative m] {α : Type u} {β : Type u} (f : α → m β) : LazyList α → m (LazyList β)

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 => Thunk.pure <$> LazyList.traverse f (Thunk.get xs)

instance LazyList.instTraversableLazyList : Traversable LazyList

instance LazyList.instLawfulTraversableLazyListInstTraversableLazyList : LawfulTraversable LazyList

def LazyList.init {α : Type u_1} : LazyList α → LazyList α

init xs, if xs non-empty, drops the last element of the list. Otherwise, return the empty list.

Equations

• LazyList.init LazyList.nil = LazyList.nil
• LazyList.init (LazyList.cons x_1 xs) = match Thunk.get xs with | LazyList.nil => LazyList.nil | LazyList.cons hd tl => LazyList.cons x_1 { fn := fun x => LazyList.init (Thunk.get xs) }

def LazyList.find {α : Type u_1} (p : α → Prop) [DecidablePred p] : LazyList α → Option α

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 (Thunk.get xs)

def LazyList.interleave {α : Type u_1} : LazyList α → LazyList α → LazyList α

interleave xs ys creates a list where elements of xs and ys alternate.

Equations

• LazyList.interleave LazyList.nil x = x
• LazyList.interleave (LazyList.cons hd tl) LazyList.nil = LazyList.cons hd tl
• LazyList.interleave (LazyList.cons x_2 xs) (LazyList.cons y ys) = LazyList.cons x_2 { fn := fun x => LazyList.cons y { fn := fun x => LazyList.interleave (Thunk.get xs) (Thunk.get ys) } }

def LazyList.interleaveAll {α : Type u_1} : List (LazyList α) → LazyList α

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) = LazyList.interleave x_1 (LazyList.interleaveAll xs)

def LazyList.bind {α : Type u_1} {β : Type u_2} : LazyList α → (α → LazyList β) → LazyList β

Monadic bind operation for LazyList.

Equations

• LazyList.bind LazyList.nil x = LazyList.nil
• LazyList.bind (LazyList.cons x_2 xs) x = LazyList.append (x x_2) { fn := fun x => LazyList.bind (Thunk.get xs) x }

def LazyList.reverse {α : Type u_1} (xs : LazyList α) : LazyList α

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.

instance LazyList.instMonadLazyList : Monad LazyList

theorem LazyList.append_nil {α : Type u_1} (xs : LazyList α) : LazyList.append xs (Thunk.pure LazyList.nil) = xs

theorem LazyList.append_assoc {α : Type u_1} (xs : LazyList α) (ys : LazyList α) (zs : LazyList α) : LazyList.append (LazyList.append xs { fn := fun x => ys }) { fn := fun x => zs } = LazyList.append xs { fn := fun x => LazyList.append ys { fn := fun x => zs } }

theorem LazyList.append_bind {α : Type u_1} {β : Type u_2} (xs : LazyList α) (ys : Thunk (LazyList α)) (f : α → LazyList β) : LazyList.bind (LazyList.append xs ys) f = LazyList.append (LazyList.bind xs f) { fn := fun x => LazyList.bind (Thunk.get ys) f }

instance LazyList.instLawfulMonadLazyListInstMonadLazyList : LawfulMonad LazyList

def LazyList.mfirst {m : Type u_1 → Type u_2} [Alternative m] {α : Type u_3} {β : Type u_1} (f : α → m β) : LazyList α → m β

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 => LazyList.mfirst f (Thunk.get xs)

def LazyList.Mem {α : Type u_1} (x : α) : LazyList α → Prop

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 (Thunk.get xs))

instance LazyList.instMembershipLazyList {α : Type u_1} : Membership α (LazyList α)

instance LazyList.Mem.decidable {α : Type u_1} [DecidableEq α] (x : α) (xs : LazyList α) : Decidable (x ∈ xs)

Equations

• One or more equations did not get rendered due to their size.
• LazyList.Mem.decidable x LazyList.nil = isFalse (_ : ¬LazyList.Mem x LazyList.nil)

@[simp]

theorem LazyList.mem_nil {α : Type u_1} (x : α) : x ∈ LazyList.nil ↔ False

@[simp]

theorem LazyList.mem_cons {α : Type u_1} (x : α) (y : α) (ys : Thunk (LazyList α)) : x ∈ LazyList.cons y ys ↔ x = y ∨ x ∈ Thunk.get ys

theorem LazyList.forall_mem_cons {α : Type u_1} {p : α → Prop} {a : α} {l : Thunk (LazyList α)} : ((x : α) → x ∈ LazyList.cons a l → p x) ↔ p a ∧ ((x : α) → x ∈ Thunk.get l → p x)

map for partial functions

def LazyList.pmap {α : Type u_1} {β : Type u_2} {p : α → Prop} (f : (a : α) → p a → β) (l : LazyList α) : ((a : α) → a ∈ l → p a) → LazyList β

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

• One or more equations did not get rendered due to their size.
• LazyList.pmap f LazyList.nil x_2 = LazyList.nil

def LazyList.attach {α : Type u_1} (l : LazyList α) : LazyList { x // x ∈ l }

"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}.

instance LazyList.instReprLazyList {α : Type u_1} [Repr α] : Repr (LazyList α)