Documentation

Batteries.Data.LazyList

Lazy lists #

Deprecated. This module is deprecated and will be removed in the future. Most use cases can use MLList. Without custom support from the kernel (previously provided in Lean 3) this type is not very useful, but was ported from Lean 3 anyway.

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 α.)

@[deprecated]
inductive LazyList (α : Type u) :

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

Instances For
    instance LazyList.instInhabited {α : Type u_1} :
    Equations
    • LazyList.instInhabited = { default := LazyList.nil }
    def LazyList.singleton {α : Type u_1} :
    αLazyList α

    The singleton lazy list.

    Equations
    Instances For
      def LazyList.ofList {α : Type u_1} :
      List αLazyList α

      Constructs a lazy list from a list.

      Equations
      Instances For
        @[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
        Instances For
          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
          Instances For
            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
            Instances For
              @[irreducible]
              def LazyList.append {α : Type u_1} :
              LazyList αThunk (LazyList α)LazyList α

              Appends two lazy lists.

              Equations
              Instances For
                @[irreducible]
                def LazyList.map {α : Type u_1} {β : Type u_2} (f : αβ) :
                LazyList αLazyList β

                Maps a function over a lazy list.

                Equations
                Instances For
                  @[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
                  Instances For
                    def LazyList.zip {α : Type u_1} {β : Type u_2} :
                    LazyList αLazyList βLazyList (α × β)

                    Zips two lazy lists.

                    Equations
                    Instances For
                      @[irreducible]
                      def LazyList.join {α : Type u_1} :

                      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 }
                      Instances For
                        def LazyList.take {α : Type u_1} :
                        NatLazyList αList α

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

                        Equations
                        Instances For
                          @[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
                          Instances For
                            def LazyList.get? {α : Type u_1} :
                            LazyList αNatOption α

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

                            Equations
                            Instances For
                              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.

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

                              Equations
                              Instances For
                                @[irreducible]
                                Equations
                                @[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
                                Instances For
                                  @[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
                                  Instances For
                                    @[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
                                    Instances For
                                      @[irreducible]
                                      def LazyList.interleave {α : Type u_1} :
                                      LazyList αLazyList αLazyList α

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

                                      Equations
                                      Instances For
                                        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
                                        Instances For
                                          @[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 }
                                          Instances For
                                            def LazyList.reverse {α : Type u_1} (xs : 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
                                            Instances For
                                              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
                                              Instances For
                                                @[irreducible]
                                                def LazyList.Mem {α : Type u_1} (x : α) :
                                                LazyList αProp

                                                Membership in lazy lists

                                                Equations
                                                Instances For
                                                  instance LazyList.instMembership {α : Type u_1} :
                                                  Equations
                                                  • LazyList.instMembership = { mem := LazyList.Mem }
                                                  @[irreducible]
                                                  instance LazyList.Mem.decidable {α : Type u_1} [DecidableEq α] (x : α) (xs : LazyList α) :
                                                  Decidable (x xs)
                                                  Equations
                                                  @[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 lp x) p a ∀ (x : α), x l.getp 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 lp 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
                                                  Instances For
                                                    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
                                                    Instances For
                                                      instance LazyList.instRepr {α : Type u_1} [Repr α] :
                                                      Equations
                                                      • LazyList.instRepr = { reprPrec := fun (xs : LazyList α) (x : Nat) => repr xs.toList }