mathlib3 documentation

data.lazy_list.basic

Definitions on lazy lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file contains various definitions and proofs on lazy lists.

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

def thunk.mk {α : Type u_1} (x : α) :

Creates a thunk with a (non-lazy) constant value.

Equations
@[protected, instance]
Equations

Isomorphism between strict and lazy lists.

Equations
@[protected, instance]
Equations
@[protected]
def lazy_list.traverse {m : Type u Type u} [applicative m] {α β : Type u} (f : α m β) :

Traversal of lazy lists using an applicative effect.

Equations
@[protected, instance]
Equations
def lazy_list.init {α : Type u_1} :

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

Equations
def lazy_list.find {α : Type u_1} (p : α Prop) [decidable_pred p] :

Return the first object contained in the list that satisfies predicate p

Equations

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

Equations

interleave_all (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
@[protected]
def lazy_list.bind {α : Type u_1} {β : Type u_2} :

Monadic bind operation for lazy_list.

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

Reverse the order of a lazy_list. 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
@[protected, instance]
Equations
theorem lazy_list.append_nil {α : Type u_1} (xs : lazy_list α) :
xs.append (λ («_» : unit), lazy_list.nil) = xs
theorem lazy_list.append_assoc {α : Type u_1} (xs ys zs : lazy_list α) :
(xs.append (λ («_» : unit), ys)).append (λ («_» : unit), zs) = xs.append (λ («_» : unit), ys.append (λ («_» : unit), zs))
theorem lazy_list.append_bind {α : Type u_1} {β : Type u_2} (xs : lazy_list α) (ys : thunk (lazy_list α)) (f : α lazy_list β) :
(xs.append ys).bind f = (xs.bind f).append (λ («_» : unit), (ys unit.star()).bind f)
def lazy_list.mfirst {m : Type u_1 Type u_2} [alternative m] {α : Type u_3} {β : Type u_1} (f : α m β) :
lazy_list α m β

Try applying function f to every element of a lazy_list and return the result of the first attempt that succeeds.

Equations
@[protected]
def lazy_list.mem {α : Type u_1} (x : α) :
lazy_list α Prop

Membership in lazy lists

Equations
@[protected, instance]
def lazy_list.has_mem {α : out_param (Type u_1)} :
Equations
@[protected, instance]
def lazy_list.mem.decidable {α : Type u_1} [decidable_eq α] (x : α) (xs : lazy_list α) :
decidable (x xs)
Equations
@[simp]
theorem lazy_list.mem_nil {α : Type u_1} (x : α) :
@[simp]
theorem lazy_list.mem_cons {α : Type u_1} (x y : α) (ys : thunk (lazy_list α)) :
theorem lazy_list.forall_mem_cons {α : Type u_1} {p : α Prop} {a : α} {l : thunk (lazy_list α)} :
( (x : α), x lazy_list.cons a l p x) p a (x : α), x l unit.star() p x

map for partial functions #

@[simp]
def lazy_list.pmap {α : Type u_1} {β : Type u_2} {p : α Prop} (f : Π (a : α), p a β) (l : lazy_list α) :
( (a : α), a l p a) lazy_list β

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
def lazy_list.attach {α : Type u_1} (l : lazy_list α) :
lazy_list {x // x l}

"Attach" the proof that the elements of l are in l to produce a new lazy_list with the same elements but in the type {x // x ∈ l}.

Equations
@[protected, instance]
def lazy_list.has_repr {α : Type u_1} [has_repr α] :
Equations