Documentation

Mathlib.Data.Seq.Seq

Possibly infinite lists #

This file provides a Seq α type representing possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

def Stream'.IsSeq {α : Type u} (s : Stream' (Option α)) :

A stream s : Option α is a sequence if s.get n = none implies s.get (n + 1) = none.

Equations
Instances For
    def Stream'.Seq (α : Type u) :

    Seq α is the type of possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

    Equations
    Instances For
      def Stream'.Seq1 (α : Type u_1) :
      Type u_1

      Seq1 α is the type of nonempty sequences.

      Equations
      Instances For

        The empty sequence

        Equations
        Instances For
          Equations
          • Stream'.Seq.instInhabitedSeq = { default := Stream'.Seq.nil }
          def Stream'.Seq.cons {α : Type u} (a : α) (s : Stream'.Seq α) :

          Prepend an element to a sequence

          Equations
          Instances For
            @[simp]
            theorem Stream'.Seq.val_cons {α : Type u} (s : Stream'.Seq α) (x : α) :
            def Stream'.Seq.get? {α : Type u} :
            Stream'.Seq αOption α

            Get the nth element of a sequence (if it exists)

            Equations
            • Stream'.Seq.get? = Subtype.val
            Instances For
              @[simp]
              theorem Stream'.Seq.get?_mk {α : Type u} (f : Stream' (Option α)) (hf : Stream'.IsSeq f) :
              Stream'.Seq.get? { val := f, property := hf } = f
              @[simp]
              theorem Stream'.Seq.get?_nil {α : Type u} (n : ) :
              Stream'.Seq.get? Stream'.Seq.nil n = none
              @[simp]
              theorem Stream'.Seq.get?_cons_zero {α : Type u} (a : α) (s : Stream'.Seq α) :
              @[simp]
              theorem Stream'.Seq.get?_cons_succ {α : Type u} (a : α) (s : Stream'.Seq α) (n : ) :
              theorem Stream'.Seq.ext {α : Type u} {s : Stream'.Seq α} {t : Stream'.Seq α} (h : ∀ (n : ), Stream'.Seq.get? s n = Stream'.Seq.get? t n) :
              s = t
              def Stream'.Seq.TerminatedAt {α : Type u} (s : Stream'.Seq α) (n : ) :

              A sequence has terminated at position n if the value at position n equals none.

              Equations
              Instances For

                It is decidable whether a sequence terminates at a given position.

                Equations

                A sequence terminates if there is some position n at which it has terminated.

                Equations
                Instances For
                  def Stream'.Seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : βγ) :
                  Option (α × β)Option (α × γ)

                  Functorial action of the functor Option (α × _)

                  Equations
                  Instances For
                    def Stream'.Seq.head {α : Type u} (s : Stream'.Seq α) :

                    Get the first element of a sequence

                    Equations
                    Instances For
                      def Stream'.Seq.tail {α : Type u} (s : Stream'.Seq α) :

                      Get the tail of a sequence (or nil if the sequence is nil)

                      Equations
                      Instances For
                        def Stream'.Seq.Mem {α : Type u} (a : α) (s : Stream'.Seq α) :

                        member definition for Seq

                        Equations
                        Instances For
                          Equations
                          • Stream'.Seq.instMembershipSeq = { mem := Stream'.Seq.Mem }
                          theorem Stream'.Seq.le_stable {α : Type u} (s : Stream'.Seq α) {m : } {n : } (h : m n) :
                          Stream'.Seq.get? s m = noneStream'.Seq.get? s n = none

                          If a sequence terminated at position n, it also terminated at m ≥ n.

                          theorem Stream'.Seq.ge_stable {α : Type u} (s : Stream'.Seq α) {aₙ : α} {n : } {m : } (m_le_n : m n) (s_nth_eq_some : Stream'.Seq.get? s n = some aₙ) :
                          ∃ (aₘ : α), Stream'.Seq.get? s m = some aₘ

                          If s.get? n = some aₙ for some value aₙ, then there is also some value aₘ such that s.get? = some aₘ for m ≤ n.

                          theorem Stream'.Seq.not_mem_nil {α : Type u} (a : α) :
                          ¬a Stream'.Seq.nil
                          theorem Stream'.Seq.mem_cons {α : Type u} (a : α) (s : Stream'.Seq α) :
                          theorem Stream'.Seq.mem_cons_of_mem {α : Type u} (y : α) {a : α} {s : Stream'.Seq α} :
                          a sa Stream'.Seq.cons y s
                          theorem Stream'.Seq.eq_or_mem_of_mem_cons {α : Type u} {a : α} {b : α} {s : Stream'.Seq α} :
                          a Stream'.Seq.cons b sa = b a s
                          @[simp]
                          theorem Stream'.Seq.mem_cons_iff {α : Type u} {a : α} {b : α} {s : Stream'.Seq α} :

                          Destructor for a sequence, resulting in either none (for nil) or some (a, s) (for cons a s).

                          Equations
                          Instances For
                            theorem Stream'.Seq.destruct_eq_nil {α : Type u} {s : Stream'.Seq α} :
                            Stream'.Seq.destruct s = nones = Stream'.Seq.nil
                            theorem Stream'.Seq.destruct_eq_cons {α : Type u} {s : Stream'.Seq α} {a : α} {s' : Stream'.Seq α} :
                            @[simp]
                            theorem Stream'.Seq.destruct_nil {α : Type u} :
                            Stream'.Seq.destruct Stream'.Seq.nil = none
                            @[simp]
                            theorem Stream'.Seq.destruct_cons {α : Type u} (a : α) (s : Stream'.Seq α) :
                            @[simp]
                            theorem Stream'.Seq.head_nil {α : Type u} :
                            Stream'.Seq.head Stream'.Seq.nil = none
                            @[simp]
                            theorem Stream'.Seq.head_cons {α : Type u} (a : α) (s : Stream'.Seq α) :
                            @[simp]
                            theorem Stream'.Seq.tail_nil {α : Type u} :
                            Stream'.Seq.tail Stream'.Seq.nil = Stream'.Seq.nil
                            @[simp]
                            theorem Stream'.Seq.tail_cons {α : Type u} (a : α) (s : Stream'.Seq α) :
                            def Stream'.Seq.recOn {α : Type u} {C : Stream'.Seq αSort v} (s : Stream'.Seq α) (h1 : C Stream'.Seq.nil) (h2 : (x : α) → (s : Stream'.Seq α) → C (Stream'.Seq.cons x s)) :
                            C s

                            Recursion principle for sequences, compare with List.recOn.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              theorem Stream'.Seq.mem_rec_on {α : Type u} {C : Stream'.Seq αProp} {a : α} {s : Stream'.Seq α} (M : a s) (h1 : ∀ (b : α) (s' : Stream'.Seq α), a = b C s'C (Stream'.Seq.cons b s')) :
                              C s
                              def Stream'.Seq.Corec.f {α : Type u} {β : Type v} (f : βOption (α × β)) :
                              Option βOption α × Option β

                              Corecursor over pairs of Option values

                              Equations
                              Instances For
                                def Stream'.Seq.corec {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) :

                                Corecursor for Seq α as a coinductive type. Iterates f to produce new elements of the sequence until none is obtained.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem Stream'.Seq.corec_eq {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) :
                                  def Stream'.Seq.BisimO {α : Type u} (R : Stream'.Seq αStream'.Seq αProp) :

                                  Bisimilarity relation over Option of Seq1 α

                                  Equations
                                  Instances For

                                    a relation is bisimilar if it meets the BisimO test

                                    Equations
                                    Instances For
                                      theorem Stream'.Seq.eq_of_bisim {α : Type u} (R : Stream'.Seq αStream'.Seq αProp) (bisim : Stream'.Seq.IsBisimulation R) {s₁ : Stream'.Seq α} {s₂ : Stream'.Seq α} (r : R s₁ s₂) :
                                      s₁ = s₂
                                      theorem Stream'.Seq.coinduction {α : Type u} {s₁ : Stream'.Seq α} {s₂ : Stream'.Seq α} :
                                      Stream'.Seq.head s₁ = Stream'.Seq.head s₂(∀ (β : Type u) (fr : Stream'.Seq αβ), fr s₁ = fr s₂fr (Stream'.Seq.tail s₁) = fr (Stream'.Seq.tail s₂))s₁ = s₂
                                      theorem Stream'.Seq.coinduction2 {α : Type u} {β : Type v} (s : Stream'.Seq α) (f : Stream'.Seq αStream'.Seq β) (g : Stream'.Seq αStream'.Seq β) (H : ∀ (s : Stream'.Seq α), Stream'.Seq.BisimO (fun (s1 s2 : Stream'.Seq β) => ∃ (s : Stream'.Seq α), s1 = f s s2 = g s) (Stream'.Seq.destruct (f s)) (Stream'.Seq.destruct (g s))) :
                                      f s = g s
                                      def Stream'.Seq.ofList {α : Type u} (l : List α) :

                                      Embed a list as a sequence

                                      Equations
                                      Instances For
                                        instance Stream'.Seq.coeList {α : Type u} :
                                        Coe (List α) (Stream'.Seq α)
                                        Equations
                                        • Stream'.Seq.coeList = { coe := Stream'.Seq.ofList }
                                        @[simp]
                                        theorem Stream'.Seq.ofList_nil {α : Type u} :
                                        [] = Stream'.Seq.nil
                                        @[simp]
                                        theorem Stream'.Seq.ofList_get {α : Type u} (l : List α) (n : ) :
                                        @[simp]
                                        theorem Stream'.Seq.ofList_cons {α : Type u} (a : α) (l : List α) :
                                        (a :: l) = Stream'.Seq.cons a l
                                        def Stream'.Seq.ofStream {α : Type u} (s : Stream' α) :

                                        Embed an infinite stream as a sequence

                                        Equations
                                        Instances For
                                          instance Stream'.Seq.coeStream {α : Type u} :
                                          Equations
                                          • Stream'.Seq.coeStream = { coe := Stream'.Seq.ofStream }

                                          Embed a LazyList α as a sequence. Note that even though this is non-meta, it will produce infinite sequences if used with cyclic LazyLists created by meta constructions.

                                          Equations
                                          Instances For
                                            instance Stream'.Seq.coeLazyList {α : Type u} :
                                            Equations
                                            • Stream'.Seq.coeLazyList = { coe := Stream'.Seq.ofLazyList }
                                            unsafe def Stream'.Seq.toLazyList {α : Type u} :

                                            Translate a sequence into a LazyList. Since LazyList and List are isomorphic as non-meta types, this function is necessarily meta.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              unsafe def Stream'.Seq.forceToList {α : Type u} (s : Stream'.Seq α) :
                                              List α

                                              Translate a sequence to a list. This function will run forever if run on an infinite sequence.

                                              Equations
                                              Instances For

                                                The sequence of natural numbers some 0, some 1, ...

                                                Equations
                                                Instances For
                                                  def Stream'.Seq.append {α : Type u} (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq α) :

                                                  Append two sequences. If s₁ is infinite, then s₁ ++ s₂ = s₁, otherwise it puts s₂ at the location of the nil in s₁.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    def Stream'.Seq.map {α : Type u} {β : Type v} (f : αβ) :

                                                    Map a function over a sequence.

                                                    Equations
                                                    Instances For

                                                      Flatten a sequence of sequences. (It is required that the sequences be nonempty to ensure productivity; in the case of an infinite sequence of nil, the first element is never generated.)

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        def Stream'.Seq.drop {α : Type u} (s : Stream'.Seq α) :

                                                        Remove the first n elements from the sequence.

                                                        Equations
                                                        Instances For
                                                          def Stream'.Seq.take {α : Type u} :
                                                          Stream'.Seq αList α

                                                          Take the first n elements of the sequence (producing a list)

                                                          Equations
                                                          Instances For
                                                            def Stream'.Seq.splitAt {α : Type u} :
                                                            Stream'.Seq αList α × Stream'.Seq α

                                                            Split a sequence at n, producing a finite initial segment and an infinite tail.

                                                            Equations
                                                            Instances For
                                                              def Stream'.Seq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s₁ : Stream'.Seq α) (s₂ : Stream'.Seq β) :

                                                              Combine two sequences with a function

                                                              Equations
                                                              Instances For
                                                                @[simp]
                                                                theorem Stream'.Seq.get?_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s : Stream'.Seq α) (s' : Stream'.Seq β) (n : ) :
                                                                def Stream'.Seq.zip {α : Type u} {β : Type v} :
                                                                Stream'.Seq αStream'.Seq βStream'.Seq (α × β)

                                                                Pair two sequences into a sequence of pairs

                                                                Equations
                                                                Instances For
                                                                  def Stream'.Seq.unzip {α : Type u} {β : Type v} (s : Stream'.Seq (α × β)) :

                                                                  Separate a sequence of pairs into two sequences

                                                                  Equations
                                                                  Instances For
                                                                    def Stream'.Seq.enum {α : Type u} (s : Stream'.Seq α) :

                                                                    Enumerate a sequence by tagging each element with its index.

                                                                    Equations
                                                                    Instances For
                                                                      @[simp]
                                                                      theorem Stream'.Seq.enum_nil {α : Type u} :
                                                                      Stream'.Seq.enum Stream'.Seq.nil = Stream'.Seq.nil

                                                                      Convert a sequence which is known to terminate into a list

                                                                      Equations
                                                                      Instances For

                                                                        Convert a sequence which is known not to terminate into a stream

                                                                        Equations
                                                                        Instances For

                                                                          Convert a sequence into either a list or a stream depending on whether it is finite or infinite. (Without decidability of the infiniteness predicate, this is not constructively possible.)

                                                                          Equations
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem Stream'.Seq.nil_append {α : Type u} (s : Stream'.Seq α) :
                                                                            Stream'.Seq.append Stream'.Seq.nil s = s
                                                                            @[simp]
                                                                            theorem Stream'.Seq.append_nil {α : Type u} (s : Stream'.Seq α) :
                                                                            Stream'.Seq.append s Stream'.Seq.nil = s
                                                                            @[simp]
                                                                            theorem Stream'.Seq.map_nil {α : Type u} {β : Type v} (f : αβ) :
                                                                            Stream'.Seq.map f Stream'.Seq.nil = Stream'.Seq.nil
                                                                            @[simp]
                                                                            theorem Stream'.Seq.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (s : Stream'.Seq α) :
                                                                            @[simp]
                                                                            theorem Stream'.Seq.map_id {α : Type u} (s : Stream'.Seq α) :
                                                                            @[simp]
                                                                            theorem Stream'.Seq.map_tail {α : Type u} {β : Type v} (f : αβ) (s : Stream'.Seq α) :
                                                                            theorem Stream'.Seq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : Stream'.Seq α) :
                                                                            @[simp]
                                                                            theorem Stream'.Seq.map_append {α : Type u} {β : Type v} (f : αβ) (s : Stream'.Seq α) (t : Stream'.Seq α) :
                                                                            @[simp]
                                                                            theorem Stream'.Seq.map_get? {α : Type u} {β : Type v} (f : αβ) (s : Stream'.Seq α) (n : ) :
                                                                            Equations
                                                                            @[simp]
                                                                            theorem Stream'.Seq.join_nil {α : Type u} :
                                                                            Stream'.Seq.join Stream'.Seq.nil = Stream'.Seq.nil
                                                                            @[simp]
                                                                            theorem Stream'.Seq.ofStream_cons {α : Type u} (a : α) (s : Stream' α) :
                                                                            @[simp]
                                                                            theorem Stream'.Seq.ofList_append {α : Type u} (l : List α) (l' : List α) :
                                                                            (l ++ l') = Stream'.Seq.append l l'
                                                                            @[simp]
                                                                            theorem Stream'.Seq.ofStream_append {α : Type u} (l : List α) (s : Stream' α) :
                                                                            (l ++ₛ s) = Stream'.Seq.append l s
                                                                            def Stream'.Seq.toList' {α : Type u_1} (s : Stream'.Seq α) :

                                                                            Convert a sequence into a list, embedded in a computation to allow for the possibility of infinite sequences (in which case the computation never returns anything).

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              theorem Stream'.Seq.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : Stream'.Seq α} :
                                                                              a sf a Stream'.Seq.map f s
                                                                              theorem Stream'.Seq.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : Stream'.Seq α} :
                                                                              b Stream'.Seq.map f s∃ (a : α), a s f a = b
                                                                              theorem Stream'.Seq.of_mem_append {α : Type u} {s₁ : Stream'.Seq α} {s₂ : Stream'.Seq α} {a : α} (h : a Stream'.Seq.append s₁ s₂) :
                                                                              a s₁ a s₂
                                                                              theorem Stream'.Seq.mem_append_left {α : Type u} {s₁ : Stream'.Seq α} {s₂ : Stream'.Seq α} {a : α} (h : a s₁) :

                                                                              Convert a Seq1 to a sequence.

                                                                              Equations
                                                                              Instances For
                                                                                instance Stream'.Seq1.coeSeq {α : Type u} :
                                                                                Equations
                                                                                • Stream'.Seq1.coeSeq = { coe := Stream'.Seq1.toSeq }
                                                                                def Stream'.Seq1.map {α : Type u} {β : Type v} (f : αβ) :

                                                                                Map a function on a Seq1

                                                                                Equations
                                                                                Instances For
                                                                                  theorem Stream'.Seq1.map_pair {α : Type u} {β : Type v} {f : αβ} {a : α} {s : Stream'.Seq α} :
                                                                                  Stream'.Seq1.map f (a, s) = (f a, Stream'.Seq.map f s)

                                                                                  Flatten a nonempty sequence of nonempty sequences

                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For
                                                                                    @[simp]
                                                                                    theorem Stream'.Seq1.join_nil {α : Type u} (a : α) (S : Stream'.Seq (Stream'.Seq1 α)) :
                                                                                    Stream'.Seq1.join ((a, Stream'.Seq.nil), S) = (a, Stream'.Seq.join S)
                                                                                    @[simp]
                                                                                    theorem Stream'.Seq1.join_cons {α : Type u} (a : α) (b : α) (s : Stream'.Seq α) (S : Stream'.Seq (Stream'.Seq1 α)) :
                                                                                    def Stream'.Seq1.ret {α : Type u} (a : α) :

                                                                                    The return operator for the Seq1 monad, which produces a singleton sequence.

                                                                                    Equations
                                                                                    Instances For
                                                                                      Equations
                                                                                      def Stream'.Seq1.bind {α : Type u} {β : Type v} (s : Stream'.Seq1 α) (f : αStream'.Seq1 β) :

                                                                                      The bind operator for the Seq1 monad, which maps f on each element of s and appends the results together. (Not all of s may be evaluated, because the first few elements of s may already produce an infinite result.)

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        theorem Stream'.Seq1.join_map_ret {α : Type u} (s : Stream'.Seq α) :
                                                                                        Stream'.Seq.join (Stream'.Seq.map Stream'.Seq1.ret s) = s
                                                                                        @[simp]
                                                                                        theorem Stream'.Seq1.bind_ret {α : Type u} {β : Type v} (f : αβ) (s : Stream'.Seq1 α) :
                                                                                        Stream'.Seq1.bind s (Stream'.Seq1.ret f) = Stream'.Seq1.map f s
                                                                                        @[simp]
                                                                                        theorem Stream'.Seq1.ret_bind {α : Type u} {β : Type v} (a : α) (f : αStream'.Seq1 β) :
                                                                                        @[simp]
                                                                                        theorem Stream'.Seq1.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Stream'.Seq1 α) (f : αStream'.Seq1 β) (g : βStream'.Seq1 γ) :