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 := ⋯ }

@[irreducible]

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

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 ⋯

@[irreducible]

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 xs.get

instance LazyList.instTraversable : Traversable LazyList

Equations

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

instance LazyList.instLawfulTraversable : LawfulTraversable LazyList

Equations

• LazyList.instLawfulTraversable = ⋯

@[irreducible]

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

@[irreducible]

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 xs.get

@[irreducible]

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

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

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

@[irreducible]

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

Monadic bind operation for LazyList.

Equations

• LazyList.nil.bind x = LazyList.nil
• (LazyList.cons x_2 xs).bind x = (x x_2).append { fn := fun (x_1 : Unit) => xs.get.bind 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

• xs.reverse = LazyList.ofList xs.toList.reverse

instance LazyList.instMonad_mathlib : Monad LazyList

Equations

• LazyList.instMonad_mathlib = Monad.mk

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

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

@[irreducible]

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

instance LazyList.instLawfulMonad_mathlib : LawfulMonad LazyList

Equations

• LazyList.instLawfulMonad_mathlib = ⋯

@[irreducible]

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 xs.get

@[irreducible]

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

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

Equations

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

@[irreducible]

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 ∈ ys.get

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

map for partial functions

@[irreducible]

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 xs.get ⋯ }

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

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

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

Equations

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