Lazy lists

The type LazyList α is a lazy list with elements of type α. In the VM, these are potentially infinite lists where all elements after the first are computed on-demand. (This is only useful for execution in the VM, logically we can prove that LazyList α is isomorphic to List α.)

inductive LazyList (α : Type u) : Type u

Lazy list. All elements (except the first) are computed lazily.

• nil: {α : Type u} → LazyList α

  The empty lazy list.

• cons: {α : Type u} → α → Thunk (LazyList α) → LazyList α

  Construct a lazy list from an element and a tail inside a thunk.

Instances For

• LazyList.instInhabited
• LazyList.instMembership
• LazyList.instMonad
• LazyList.instRepr

instance LazyList.instInhabited {α : Type u_1} : Inhabited (LazyList α)

Equations

• LazyList.instInhabited = { default := LazyList.nil }

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

The singleton lazy list.

Equations

• LazyList.singleton x = let a := x; LazyList.cons a (Thunk.pure LazyList.nil)

def LazyList.ofList {α : Type u_1} : List α → LazyList α

Constructs a lazy list from a list.

Equations

• LazyList.ofList [] = LazyList.nil
• LazyList.ofList (h :: t) = LazyList.cons h { fn := fun (x : Unit) => LazyList.ofList t }

@[irreducible]

def LazyList.toList {α : Type u_1} : LazyList α → List α

Converts a lazy list to a list. If the lazy list is infinite, then this function does not terminate.

Equations

• LazyList.nil.toList = []
• (LazyList.cons h t).toList = h :: t.get.toList

def LazyList.headI {α : Type u_1} [Inhabited α] : LazyList α → α

Returns the first element of the lazy list, or default if the lazy list is empty.

Equations

• x.headI = match x with | LazyList.nil => default | LazyList.cons h tl => h

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

Removes the first element of the lazy list.

Equations

• x.tail = match x with | LazyList.nil => LazyList.nil | LazyList.cons hd t => t.get

@[irreducible]

def LazyList.append {α : Type u_1} : LazyList α → Thunk (LazyList α) → LazyList α

Appends two lazy lists.

Equations

• LazyList.nil.append x = x.get
• (LazyList.cons h t).append x = LazyList.cons h { fn := fun (x_1 : Unit) => t.get.append x }

@[irreducible]

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

Maps a function over a lazy list.

Equations

• LazyList.map f LazyList.nil = LazyList.nil
• LazyList.map f (LazyList.cons h t) = LazyList.cons (f h) { fn := fun (x : Unit) => LazyList.map f t.get }

@[irreducible]

def LazyList.map₂ {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : α → β → δ) : LazyList α → LazyList β → LazyList δ

Maps a binary function over two lazy list. Like LazyList.zip, the result is only as long as the smaller input.

Equations

• LazyList.map₂ f LazyList.nil x = LazyList.nil
• LazyList.map₂ f x LazyList.nil = LazyList.nil
• LazyList.map₂ f (LazyList.cons h₁ t₁) (LazyList.cons h₂ t₂) = LazyList.cons (f h₁ h₂) { fn := fun (x : Unit) => LazyList.map₂ f t₁.get t₂.get }

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

Zips two lazy lists.

Equations

• LazyList.zip = LazyList.map₂ Prod.mk

@[irreducible]

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

The monadic join operation for lazy lists.

Equations

• LazyList.nil.join = LazyList.nil
• (LazyList.cons h t).join = h.append { fn := fun (x : Unit) => t.get.join }

def LazyList.take {α : Type u_1} : Nat → LazyList α → List α

The list containing the first n elements of a lazy list.

Equations

• LazyList.take 0 x = []
• LazyList.take x LazyList.nil = []
• LazyList.take a.succ (LazyList.cons h t) = h :: LazyList.take a t.get

@[irreducible]

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

The lazy list of all elements satisfying the predicate. If the lazy list is infinite and none of the elements satisfy the predicate, then this function will not terminate.

Equations

• LazyList.filter p LazyList.nil = LazyList.nil
• LazyList.filter p (LazyList.cons h t) = if p h then LazyList.cons h { fn := fun (x : Unit) => LazyList.filter p t.get } else LazyList.filter p t.get

def LazyList.get? {α : Type u_1} : LazyList α → Nat → Option α

The nth element of a lazy list as an option (like List.get?).

Equations

• LazyList.nil.get? x = none
• (LazyList.cons a tl).get? 0 = some a
• (LazyList.cons hd l).get? n.succ = l.get.get? n

partial def LazyList.iterates {α : Type u_1} (f : α → α) : α → LazyList α

The infinite lazy list [x, f x, f (f x), ...] of iterates of a function. This definition is partial because it creates an infinite list.

def LazyList.iota (i : Nat) : LazyList Nat

The infinite lazy list [i, i+1, i+2, ...]

Equations

• LazyList.iota i = LazyList.iterates Nat.succ i

@[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 h t) = Seq.seq (LazyList.cons <$> f h) fun (x : Unit) => Thunk.pure <$> LazyList.traverse f t.get

@[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 h t).init = match t.get with | LazyList.nil => LazyList.nil | LazyList.cons hd tl => LazyList.cons h { fn := fun (x : Unit) => t.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 h t) = if p h then some h else LazyList.find p t.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 : Monad LazyList

Equations

• LazyList.instMonad = 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 }

@[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 h t) = HOrElse.hOrElse (f h) fun (x : Unit) => LazyList.mfirst f t.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 h t) = (x = h ∨ LazyList.Mem x t.get)

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

Equations

• LazyList.instMembership = { 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 : α), x ∈ LazyList.cons a l → p x) ↔ p a ∧ ∀ (x : α), 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 : α), 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 {α : Type u_1} [Repr α] : Repr (LazyList α)

Equations

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