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.

Equations

• LazyList.listEquivLazyList α = { toFun := LazyList.ofList, invFun := LazyList.toList, left_inv := ⋯, right_inv := ⋯ }

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.decidableEq LazyList.nil (LazyList.cons hd tl) = isFalse ⋯
• LazyList.decidableEq (LazyList.cons hd tl) LazyList.nil = isFalse ⋯

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

instance LazyList.instTraversableLazyList : Traversable LazyList

Equations

• LazyList.instTraversableLazyList = Traversable.mk @LazyList.traverse

instance LazyList.instLawfulTraversableLazyListInstTraversableLazyList : LawfulTraversable LazyList

Equations

• LazyList.instLawfulTraversableLazyListInstTraversableLazyList = ⋯

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

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

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

• One or more equations did not get rendered due to their size.
• LazyList.interleave LazyList.nil x = x
• LazyList.interleave (LazyList.cons hd tl) LazyList.nil = LazyList.cons hd tl

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_1 : Unit) => 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.

Equations

• LazyList.reverse xs = LazyList.ofList (List.reverse (LazyList.toList xs))

instance LazyList.instMonadLazyList : Monad LazyList

Equations

• LazyList.instMonadLazyList = Monad.mk

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 : Unit) => ys }) { fn := fun (x : Unit) => zs } = LazyList.append xs { fn := fun (x : Unit) => LazyList.append ys { fn := fun (x : Unit) => 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 : Unit) => LazyList.bind (Thunk.get ys) f }

instance LazyList.instLawfulMonadLazyListInstMonadLazyList : LawfulMonad LazyList

Equations

• LazyList.instLawfulMonadLazyListInstMonadLazyList = ⋯

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 : Unit) => 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 α)

Equations

• LazyList.instMembershipLazyList = { mem := LazyList.Mem }

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 ⋯

@[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 ∈ LazyList.cons a l, p x) ↔ p a ∧ ∀ 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 ∈ 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

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

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

Equations

• LazyList.attach l = LazyList.pmap Subtype.mk l ⋯

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

Equations

• LazyList.instReprLazyList = { reprPrec := fun (xs : LazyList α) (x : ℕ) => repr (LazyList.toList xs) }