Documentation

Mathlib.Data.Seq.WSeq

Partially defined possibly infinite lists #

This file provides a WSeq α type representing partially defined possibly infinite lists (referred here as weak sequences).

def Stream'.WSeq (α : Type u_1) :
Type u_1

Weak sequences.

While the Seq structure allows for lists which may not be finite, a weak sequence also allows the computation of each element to involve an indeterminate amount of computation, including possibly an infinite loop. This is represented as a regular Seq interspersed with none elements to indicate that computation is ongoing.

This model is appropriate for Haskell style lazy lists, and is closed under most interesting computation patterns on infinite lists, but conversely it is difficult to extract elements from it.

Equations
Instances For

    Turn a sequence into a weak sequence

    Equations
    Instances For
      def Stream'.WSeq.ofList {α : Type u} (l : List α) :

      Turn a list into a weak sequence

      Equations
      • l = l
      Instances For

        Turn a stream into a weak sequence

        Equations
        • l = l
        Instances For
          instance Stream'.WSeq.coeSeq {α : Type u} :
          Equations
          • Stream'.WSeq.coeSeq = { coe := Stream'.WSeq.ofSeq }
          instance Stream'.WSeq.coeList {α : Type u} :
          Equations
          • Stream'.WSeq.coeList = { coe := Stream'.WSeq.ofList }
          instance Stream'.WSeq.coeStream {α : Type u} :
          Equations
          • Stream'.WSeq.coeStream = { coe := Stream'.WSeq.ofStream }

          The empty weak sequence

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

            Prepend an element to a weak sequence

            Equations
            Instances For

              Compute for one tick, without producing any elements

              Equations
              Instances For

                Destruct a weak sequence, to (eventually possibly) produce either none for nil or some (a, s) if an element is produced.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  def Stream'.WSeq.recOn {α : Type u} {C : Stream'.WSeq αSort v} (s : Stream'.WSeq α) (h1 : C Stream'.WSeq.nil) (h2 : (x : α) → (s : Stream'.WSeq α) → C (Stream'.WSeq.cons x s)) (h3 : (s : Stream'.WSeq α) → C s.think) :
                  C s

                  Recursion principle for weak sequences, compare with List.recOn.

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

                    membership for weak sequences

                    Equations
                    Instances For
                      Equations
                      • Stream'.WSeq.membership = { mem := Stream'.WSeq.Mem }
                      theorem Stream'.WSeq.not_mem_nil {α : Type u} (a : α) :
                      ¬a Stream'.WSeq.nil

                      Get the head of a weak sequence. This involves a possibly infinite computation.

                      Equations
                      Instances For

                        Encode a computation yielding a weak sequence into additional think constructors in a weak sequence

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          Get the tail of a weak sequence. This doesn't need a Computation wrapper, unlike head, because flatten allows us to hide this in the construction of the weak sequence itself.

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

                            drop the first n elements from s.

                            Equations
                            • s.drop 0 = s
                            • s.drop n.succ = (s.drop n).tail
                            Instances For
                              def Stream'.WSeq.get? {α : Type u} (s : Stream'.WSeq α) (n : ) :

                              Get the nth element of s.

                              Equations
                              • s.get? n = (s.drop n).head
                              Instances For

                                Convert s to a list (if it is finite and completes in finite time).

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  Get the length of s (if it is finite and completes in finite time).

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

                                    A weak sequence is finite if toList s terminates. Equivalently, it is a finite number of think and cons applied to nil.

                                    • out : s.toList.Terminates
                                    Instances
                                      theorem Stream'.WSeq.IsFinite.out {α : Type u} {s : Stream'.WSeq α} [self : s.IsFinite] :
                                      s.toList.Terminates
                                      instance Stream'.WSeq.toList_terminates {α : Type u} (s : Stream'.WSeq α) [h : s.IsFinite] :
                                      s.toList.Terminates
                                      Equations
                                      • =
                                      def Stream'.WSeq.get {α : Type u} (s : Stream'.WSeq α) [s.IsFinite] :
                                      List α

                                      Get the list corresponding to a finite weak sequence.

                                      Equations
                                      • s.get = s.toList.get
                                      Instances For

                                        A weak sequence is productive if it never stalls forever - there are always a finite number of thinks between cons constructors. The sequence itself is allowed to be infinite though.

                                        • get?_terminates : ∀ (n : ), (s.get? n).Terminates
                                        Instances
                                          theorem Stream'.WSeq.Productive.get?_terminates {α : Type u} {s : Stream'.WSeq α} [self : s.Productive] (n : ) :
                                          (s.get? n).Terminates
                                          theorem Stream'.WSeq.productive_iff {α : Type u} (s : Stream'.WSeq α) :
                                          s.Productive ∀ (n : ), (s.get? n).Terminates
                                          instance Stream'.WSeq.get?_terminates {α : Type u} (s : Stream'.WSeq α) [h : s.Productive] (n : ) :
                                          (s.get? n).Terminates
                                          Equations
                                          • =
                                          instance Stream'.WSeq.head_terminates {α : Type u} (s : Stream'.WSeq α) [s.Productive] :
                                          s.head.Terminates
                                          Equations
                                          • =
                                          def Stream'.WSeq.updateNth {α : Type u} (s : Stream'.WSeq α) (n : ) (a : α) :

                                          Replace the nth element of s with a.

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

                                            Remove the nth element of s.

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

                                              Map the elements of s over f, removing any values that yield none.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                def Stream'.WSeq.filter {α : Type u} (p : αProp) [DecidablePred p] :

                                                Select the elements of s that satisfy p.

                                                Equations
                                                Instances For
                                                  def Stream'.WSeq.find {α : Type u} (p : αProp) [DecidablePred p] (s : Stream'.WSeq α) :

                                                  Get the first element of s satisfying p.

                                                  Equations
                                                  Instances For
                                                    def Stream'.WSeq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq β) :

                                                    Zip a function over two weak sequences

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

                                                      Zip two weak sequences into a single sequence of pairs

                                                      Equations
                                                      Instances For

                                                        Get the list of indexes of elements of s satisfying p

                                                        Equations
                                                        Instances For
                                                          def Stream'.WSeq.findIndex {α : Type u} (p : αProp) [DecidablePred p] (s : Stream'.WSeq α) :

                                                          Get the index of the first element of s satisfying p

                                                          Equations
                                                          Instances For

                                                            Get the index of the first occurrence of a in s

                                                            Equations
                                                            Instances For

                                                              Get the indexes of occurrences of a in s

                                                              Equations
                                                              Instances For
                                                                def Stream'.WSeq.union {α : Type u} (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq α) :

                                                                union s1 s2 is a weak sequence which interleaves s1 and s2 in some order (nondeterministically).

                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For

                                                                  Returns true if s is nil and false if s has an element

                                                                  Equations
                                                                  Instances For

                                                                    Calculate one step of computation

                                                                    Equations
                                                                    Instances For
                                                                      def Stream'.WSeq.take {α : Type u} (s : Stream'.WSeq α) (n : ) :

                                                                      Get the first n elements of a weak sequence

                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        Split the sequence at position n into a finite initial segment and the weak sequence tail

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

                                                                          Returns true if any element of s satisfies p

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

                                                                            Returns true if every element of s satisfies p

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

                                                                              Apply a function to the elements of the sequence to produce a sequence of partial results. (There is no scanr because this would require working from the end of the sequence, which may not exist.)

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For

                                                                                Get the weak sequence of initial segments of the input sequence

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

                                                                                  Like take, but does not wait for a result. Calculates n steps of computation and returns the sequence computed so far

                                                                                  Equations
                                                                                  Instances For

                                                                                    Append two weak sequences. As with Seq.append, this may not use the second sequence if the first one takes forever to compute

                                                                                    Equations
                                                                                    • Stream'.WSeq.append = Stream'.Seq.append
                                                                                    Instances For
                                                                                      def Stream'.WSeq.map {α : Type u} {β : Type v} (f : αβ) :

                                                                                      Map a function over a weak sequence

                                                                                      Equations
                                                                                      Instances For

                                                                                        Flatten a sequence of weak sequences. (Note that this allows empty sequences, unlike Seq.join.)

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

                                                                                          Monadic bind operator for weak sequences

                                                                                          Equations
                                                                                          Instances For
                                                                                            def Stream'.WSeq.LiftRelO {α : Type u} {β : Type v} (R : αβProp) (C : Stream'.WSeq αStream'.WSeq βProp) :
                                                                                            Option (α × Stream'.WSeq α)Option (β × Stream'.WSeq β)Prop

                                                                                            lift a relation to a relation over weak sequences

                                                                                            Equations
                                                                                            Instances For
                                                                                              theorem Stream'.WSeq.LiftRelO.imp {α : Type u} {β : Type v} {R : αβProp} {S : αβProp} {C : Stream'.WSeq αStream'.WSeq βProp} {D : Stream'.WSeq αStream'.WSeq βProp} (H1 : ∀ (a : α) (b : β), R a bS a b) (H2 : ∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s tD s t) {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)} :
                                                                                              theorem Stream'.WSeq.LiftRelO.imp_right {α : Type u} {β : Type v} (R : αβProp) {C : Stream'.WSeq αStream'.WSeq βProp} {D : Stream'.WSeq αStream'.WSeq βProp} (H : ∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s tD s t) {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)} :
                                                                                              def Stream'.WSeq.BisimO {α : Type u} (R : Stream'.WSeq αStream'.WSeq αProp) :
                                                                                              Option (α × Stream'.WSeq α)Option (α × Stream'.WSeq α)Prop

                                                                                              Definition of bisimilarity for weak sequences

                                                                                              Equations
                                                                                              Instances For
                                                                                                theorem Stream'.WSeq.BisimO.imp {α : Type u} {R : Stream'.WSeq αStream'.WSeq αProp} {S : Stream'.WSeq αStream'.WSeq αProp} (H : ∀ (s t : Stream'.WSeq α), R s tS s t) {o : Option (α × Stream'.WSeq α)} {p : Option (α × Stream'.WSeq α)} :
                                                                                                def Stream'.WSeq.LiftRel {α : Type u} {β : Type v} (R : αβProp) (s : Stream'.WSeq α) (t : Stream'.WSeq β) :

                                                                                                Two weak sequences are LiftRel R related if they are either both empty, or they are both nonempty and the heads are R related and the tails are LiftRel R related. (This is a coinductive definition.)

                                                                                                Equations
                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                Instances For

                                                                                                  If two sequences are equivalent, then they have the same values and the same computational behavior (i.e. if one loops forever then so does the other), although they may differ in the number of thinks needed to arrive at the answer.

                                                                                                  Equations
                                                                                                  Instances For
                                                                                                    theorem Stream'.WSeq.liftRel_destruct {α : Type u} {β : Type v} {R : αβProp} {s : Stream'.WSeq α} {t : Stream'.WSeq β} :
                                                                                                    theorem Stream'.WSeq.liftRel_destruct_iff {α : Type u} {β : Type v} {R : αβProp} {s : Stream'.WSeq α} {t : Stream'.WSeq β} :
                                                                                                    theorem Stream'.WSeq.destruct_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} :
                                                                                                    s tComputation.LiftRel (Stream'.WSeq.BisimO fun (x1 x2 : Stream'.WSeq α) => x1 x2) s.destruct t.destruct
                                                                                                    theorem Stream'.WSeq.destruct_congr_iff {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} :
                                                                                                    s t Computation.LiftRel (Stream'.WSeq.BisimO fun (x1 x2 : Stream'.WSeq α) => x1 x2) s.destruct t.destruct
                                                                                                    theorem Stream'.WSeq.LiftRel.refl {α : Type u} (R : ααProp) (H : Reflexive R) :
                                                                                                    theorem Stream'.WSeq.LiftRel.swap_lem {α : Type u} {β : Type v} {R : αβProp} {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} (h : Stream'.WSeq.LiftRel R s1 s2) :
                                                                                                    theorem Stream'.WSeq.LiftRel.symm {α : Type u} (R : ααProp) (H : Symmetric R) :
                                                                                                    theorem Stream'.WSeq.LiftRel.trans {α : Type u} (R : ααProp) (H : Transitive R) :
                                                                                                    theorem Stream'.WSeq.Equiv.refl {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    s s
                                                                                                    theorem Stream'.WSeq.Equiv.symm {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} :
                                                                                                    s tt s
                                                                                                    theorem Stream'.WSeq.Equiv.trans {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} {u : Stream'.WSeq α} :
                                                                                                    s tt us u
                                                                                                    theorem Stream'.WSeq.Equiv.equivalence {α : Type u} :
                                                                                                    Equivalence Stream'.WSeq.Equiv
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.destruct_nil {α : Type u} :
                                                                                                    Stream'.WSeq.nil.destruct = Computation.pure none
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.destruct_cons {α : Type u} (a : α) (s : Stream'.WSeq α) :
                                                                                                    (Stream'.WSeq.cons a s).destruct = Computation.pure (some (a, s))
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.destruct_think {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    s.think.destruct = s.destruct.think
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.seq_destruct_nil {α : Type u} :
                                                                                                    Stream'.Seq.destruct Stream'.WSeq.nil = none
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.seq_destruct_think {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    Stream'.Seq.destruct s.think = some (none, s)
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.head_nil {α : Type u} :
                                                                                                    Stream'.WSeq.nil.head = Computation.pure none
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.head_cons {α : Type u} (a : α) (s : Stream'.WSeq α) :
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.head_think {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    s.think.head = s.head.think
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.destruct_flatten {α : Type u} (c : Computation (Stream'.WSeq α)) :
                                                                                                    (Stream'.WSeq.flatten c).destruct = c >>= Stream'.WSeq.destruct
                                                                                                    theorem Stream'.WSeq.head_terminates_iff {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    s.head.Terminates s.destruct.Terminates
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.tail_nil {α : Type u} :
                                                                                                    Stream'.WSeq.nil.tail = Stream'.WSeq.nil
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.tail_cons {α : Type u} (a : α) (s : Stream'.WSeq α) :
                                                                                                    (Stream'.WSeq.cons a s).tail = s
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.tail_think {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    s.think.tail = s.tail.think
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.dropn_nil {α : Type u} (n : ) :
                                                                                                    Stream'.WSeq.nil.drop n = Stream'.WSeq.nil
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.dropn_cons {α : Type u} (a : α) (s : Stream'.WSeq α) (n : ) :
                                                                                                    (Stream'.WSeq.cons a s).drop (n + 1) = s.drop n
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.dropn_think {α : Type u} (s : Stream'.WSeq α) (n : ) :
                                                                                                    s.think.drop n = (s.drop n).think
                                                                                                    theorem Stream'.WSeq.dropn_add {α : Type u} (s : Stream'.WSeq α) (m : ) (n : ) :
                                                                                                    s.drop (m + n) = (s.drop m).drop n
                                                                                                    theorem Stream'.WSeq.dropn_tail {α : Type u} (s : Stream'.WSeq α) (n : ) :
                                                                                                    s.tail.drop n = s.drop (n + 1)
                                                                                                    theorem Stream'.WSeq.get?_add {α : Type u} (s : Stream'.WSeq α) (m : ) (n : ) :
                                                                                                    s.get? (m + n) = (s.drop m).get? n
                                                                                                    theorem Stream'.WSeq.get?_tail {α : Type u} (s : Stream'.WSeq α) (n : ) :
                                                                                                    s.tail.get? n = s.get? (n + 1)
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.join_nil {α : Type u} :
                                                                                                    Stream'.WSeq.nil.join = Stream'.WSeq.nil
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.join_think {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) :
                                                                                                    S.think.join = S.join.think
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.join_cons {α : Type u} (s : Stream'.WSeq α) (S : Stream'.WSeq (Stream'.WSeq α)) :
                                                                                                    (Stream'.WSeq.cons s S).join = (s.append S.join).think
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.nil_append {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    Stream'.WSeq.nil.append s = s
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.cons_append {α : Type u} (a : α) (s : Stream'.WSeq α) (t : Stream'.WSeq α) :
                                                                                                    (Stream'.WSeq.cons a s).append t = Stream'.WSeq.cons a (s.append t)
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.think_append {α : Type u} (s : Stream'.WSeq α) (t : Stream'.WSeq α) :
                                                                                                    s.think.append t = (s.append t).think
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.append_nil {α : Type u} (s : Stream'.WSeq α) :
                                                                                                    s.append Stream'.WSeq.nil = s
                                                                                                    @[simp]
                                                                                                    theorem Stream'.WSeq.append_assoc {α : Type u} (s : Stream'.WSeq α) (t : Stream'.WSeq α) (u : Stream'.WSeq α) :
                                                                                                    (s.append t).append u = s.append (t.append u)

                                                                                                    auxiliary definition of tail over weak sequences

                                                                                                    Equations
                                                                                                    Instances For
                                                                                                      theorem Stream'.WSeq.destruct_tail {α : Type u} (s : Stream'.WSeq α) :
                                                                                                      s.tail.destruct = s.destruct >>= Stream'.WSeq.tail.aux

                                                                                                      auxiliary definition of drop over weak sequences

                                                                                                      Equations
                                                                                                      Instances For
                                                                                                        theorem Stream'.WSeq.destruct_dropn {α : Type u} (s : Stream'.WSeq α) (n : ) :
                                                                                                        (s.drop n).destruct = s.destruct >>= Stream'.WSeq.drop.aux n
                                                                                                        theorem Stream'.WSeq.head_terminates_of_head_tail_terminates {α : Type u} (s : Stream'.WSeq α) [T : s.tail.head.Terminates] :
                                                                                                        s.head.Terminates
                                                                                                        theorem Stream'.WSeq.destruct_some_of_destruct_tail_some {α : Type u} {s : Stream'.WSeq α} {a : α × Stream'.WSeq α} (h : some a s.tail.destruct) :
                                                                                                        ∃ (a' : α × Stream'.WSeq α), some a' s.destruct
                                                                                                        theorem Stream'.WSeq.head_some_of_head_tail_some {α : Type u} {s : Stream'.WSeq α} {a : α} (h : some a s.tail.head) :
                                                                                                        ∃ (a' : α), some a' s.head
                                                                                                        theorem Stream'.WSeq.head_some_of_get?_some {α : Type u} {s : Stream'.WSeq α} {a : α} {n : } (h : some a s.get? n) :
                                                                                                        ∃ (a' : α), some a' s.head
                                                                                                        instance Stream'.WSeq.productive_tail {α : Type u} (s : Stream'.WSeq α) [s.Productive] :
                                                                                                        s.tail.Productive
                                                                                                        Equations
                                                                                                        • =
                                                                                                        instance Stream'.WSeq.productive_dropn {α : Type u} (s : Stream'.WSeq α) [s.Productive] (n : ) :
                                                                                                        (s.drop n).Productive
                                                                                                        Equations
                                                                                                        • =
                                                                                                        def Stream'.WSeq.toSeq {α : Type u} (s : Stream'.WSeq α) [s.Productive] :

                                                                                                        Given a productive weak sequence, we can collapse all the thinks to produce a sequence.

                                                                                                        Equations
                                                                                                        • s.toSeq = fun (n : ) => (s.get? n).get,
                                                                                                        Instances For
                                                                                                          theorem Stream'.WSeq.get?_terminates_le {α : Type u} {s : Stream'.WSeq α} {m : } {n : } (h : m n) :
                                                                                                          (s.get? n).Terminates(s.get? m).Terminates
                                                                                                          theorem Stream'.WSeq.head_terminates_of_get?_terminates {α : Type u} {s : Stream'.WSeq α} {n : } :
                                                                                                          (s.get? n).Terminatess.head.Terminates
                                                                                                          theorem Stream'.WSeq.destruct_terminates_of_get?_terminates {α : Type u} {s : Stream'.WSeq α} {n : } (T : (s.get? n).Terminates) :
                                                                                                          s.destruct.Terminates
                                                                                                          theorem Stream'.WSeq.mem_rec_on {α : Type u} {C : Stream'.WSeq αProp} {a : α} {s : Stream'.WSeq α} (M : a s) (h1 : ∀ (b : α) (s' : Stream'.WSeq α), a = b C s'C (Stream'.WSeq.cons b s')) (h2 : ∀ (s : Stream'.WSeq α), C sC s.think) :
                                                                                                          C s
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.mem_think {α : Type u} (s : Stream'.WSeq α) (a : α) :
                                                                                                          a s.think a s
                                                                                                          theorem Stream'.WSeq.eq_or_mem_iff_mem {α : Type u} {s : Stream'.WSeq α} {a : α} {a' : α} {s' : Stream'.WSeq α} :
                                                                                                          some (a', s') s.destruct(a s a = a' a s')
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.mem_cons_iff {α : Type u} (s : Stream'.WSeq α) (b : α) {a : α} :
                                                                                                          theorem Stream'.WSeq.mem_cons_of_mem {α : Type u} {s : Stream'.WSeq α} (b : α) {a : α} (h : a s) :
                                                                                                          theorem Stream'.WSeq.mem_cons {α : Type u} (s : Stream'.WSeq α) (a : α) :
                                                                                                          theorem Stream'.WSeq.mem_of_mem_tail {α : Type u} {s : Stream'.WSeq α} {a : α} :
                                                                                                          a s.taila s
                                                                                                          theorem Stream'.WSeq.mem_of_mem_dropn {α : Type u} {s : Stream'.WSeq α} {a : α} {n : } :
                                                                                                          a s.drop na s
                                                                                                          theorem Stream'.WSeq.get?_mem {α : Type u} {s : Stream'.WSeq α} {a : α} {n : } :
                                                                                                          some a s.get? na s
                                                                                                          theorem Stream'.WSeq.exists_get?_of_mem {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a s) :
                                                                                                          ∃ (n : ), some a s.get? n
                                                                                                          theorem Stream'.WSeq.exists_dropn_of_mem {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a s) :
                                                                                                          ∃ (n : ), ∃ (s' : Stream'.WSeq α), some (a, s') (s.drop n).destruct
                                                                                                          theorem Stream'.WSeq.liftRel_dropn_destruct {α : Type u} {β : Type v} {R : αβProp} {s : Stream'.WSeq α} {t : Stream'.WSeq β} (H : Stream'.WSeq.LiftRel R s t) (n : ) :
                                                                                                          Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) (s.drop n).destruct (t.drop n).destruct
                                                                                                          theorem Stream'.WSeq.exists_of_liftRel_left {α : Type u} {β : Type v} {R : αβProp} {s : Stream'.WSeq α} {t : Stream'.WSeq β} (H : Stream'.WSeq.LiftRel R s t) {a : α} (h : a s) :
                                                                                                          ∃ (b : β), b t R a b
                                                                                                          theorem Stream'.WSeq.exists_of_liftRel_right {α : Type u} {β : Type v} {R : αβProp} {s : Stream'.WSeq α} {t : Stream'.WSeq β} (H : Stream'.WSeq.LiftRel R s t) {b : β} (h : b t) :
                                                                                                          ∃ (a : α), a s R a b
                                                                                                          theorem Stream'.WSeq.head_terminates_of_mem {α : Type u} {s : Stream'.WSeq α} {a : α} (h : a s) :
                                                                                                          s.head.Terminates
                                                                                                          theorem Stream'.WSeq.of_mem_append {α : Type u} {s₁ : Stream'.WSeq α} {s₂ : Stream'.WSeq α} {a : α} :
                                                                                                          a s₁.append s₂a s₁ a s₂
                                                                                                          theorem Stream'.WSeq.mem_append_left {α : Type u} {s₁ : Stream'.WSeq α} {s₂ : Stream'.WSeq α} {a : α} :
                                                                                                          a s₁a s₁.append s₂
                                                                                                          theorem Stream'.WSeq.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : Stream'.WSeq α} :
                                                                                                          b Stream'.WSeq.map f s∃ (a : α), a s f a = b
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.liftRel_nil {α : Type u} {β : Type v} (R : αβProp) :
                                                                                                          Stream'.WSeq.LiftRel R Stream'.WSeq.nil Stream'.WSeq.nil
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.liftRel_cons {α : Type u} {β : Type v} (R : αβProp) (a : α) (b : β) (s : Stream'.WSeq α) (t : Stream'.WSeq β) :
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.liftRel_think_left {α : Type u} {β : Type v} (R : αβProp) (s : Stream'.WSeq α) (t : Stream'.WSeq β) :
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.liftRel_think_right {α : Type u} {β : Type v} (R : αβProp) (s : Stream'.WSeq α) (t : Stream'.WSeq β) :
                                                                                                          theorem Stream'.WSeq.cons_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (a : α) (h : s t) :
                                                                                                          theorem Stream'.WSeq.think_equiv {α : Type u} (s : Stream'.WSeq α) :
                                                                                                          s.think s
                                                                                                          theorem Stream'.WSeq.think_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) :
                                                                                                          s.think t.think
                                                                                                          theorem Stream'.WSeq.head_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} :
                                                                                                          s ts.head.Equiv t.head
                                                                                                          theorem Stream'.WSeq.tail_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) :
                                                                                                          s.tail t.tail
                                                                                                          theorem Stream'.WSeq.dropn_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) (n : ) :
                                                                                                          s.drop n t.drop n
                                                                                                          theorem Stream'.WSeq.get?_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) (n : ) :
                                                                                                          (s.get? n).Equiv (t.get? n)
                                                                                                          theorem Stream'.WSeq.mem_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) (a : α) :
                                                                                                          a s a t
                                                                                                          theorem Stream'.WSeq.productive_congr {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) :
                                                                                                          s.Productive t.Productive
                                                                                                          theorem Stream'.WSeq.Equiv.ext {α : Type u} {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : ∀ (n : ), (s.get? n).Equiv (t.get? n)) :
                                                                                                          s t
                                                                                                          theorem Stream'.WSeq.length_eq_map {α : Type u} (s : Stream'.WSeq α) :
                                                                                                          s.length = Computation.map List.length s.toList
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.ofList_nil {α : Type u} :
                                                                                                          [] = Stream'.WSeq.nil
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.ofList_cons {α : Type u} (a : α) (l : List α) :
                                                                                                          (a :: l) = Stream'.WSeq.cons a l
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.toList'_nil {α : Type u} (l : List α) :
                                                                                                          Computation.corec (fun (x : List α × Stream'.WSeq α) => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.nil) = Computation.pure l.reverse
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.toList'_cons {α : Type u} (l : List α) (s : Stream'.WSeq α) (a : α) :
                                                                                                          Computation.corec (fun (x : List α × Stream'.WSeq α) => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, Stream'.WSeq.cons a s) = (Computation.corec (fun (x : List α × Stream'.WSeq α) => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (a :: l, s)).think
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.toList'_think {α : Type u} (l : List α) (s : Stream'.WSeq α) :
                                                                                                          Computation.corec (fun (x : List α × Stream'.WSeq α) => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s.think) = (Computation.corec (fun (x : List α × Stream'.WSeq α) => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s)).think
                                                                                                          theorem Stream'.WSeq.toList'_map {α : Type u} (l : List α) (s : Stream'.WSeq α) :
                                                                                                          Computation.corec (fun (x : List α × Stream'.WSeq α) => match x with | (l, s) => match Stream'.Seq.destruct s with | none => Sum.inl l.reverse | some (none, s') => Sum.inr (l, s') | some (some a, s') => Sum.inr (a :: l, s')) (l, s) = (fun (x : List α) => l.reverse ++ x) <$> s.toList
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.toList_cons {α : Type u} (a : α) (s : Stream'.WSeq α) :
                                                                                                          (Stream'.WSeq.cons a s).toList = (List.cons a <$> s.toList).think
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.toList_nil {α : Type u} :
                                                                                                          Stream'.WSeq.nil.toList = Computation.pure []
                                                                                                          theorem Stream'.WSeq.toList_ofList {α : Type u} (l : List α) :
                                                                                                          l (↑l).toList
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.destruct_ofSeq {α : Type u} (s : Stream'.Seq α) :
                                                                                                          (↑s).destruct = Computation.pure (Option.map (fun (a : α) => (a, s.tail)) s.head)
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.head_ofSeq {α : Type u} (s : Stream'.Seq α) :
                                                                                                          (↑s).head = Computation.pure s.head
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.tail_ofSeq {α : Type u} (s : Stream'.Seq α) :
                                                                                                          (↑s).tail = s.tail
                                                                                                          @[simp]
                                                                                                          theorem Stream'.WSeq.dropn_ofSeq {α : Type u} (s : Stream'.Seq α) (n : ) :
                                                                                                          (↑s).drop n = (s.drop n)
                                                                                                          theorem Stream'.WSeq.get?_ofSeq {α : Type u} (s : Stream'.Seq α) (n : ) :
                                                                                                          (↑s).get? n = Computation.pure (s.get? n)
                                                                                                          instance Stream'.WSeq.productive_ofSeq {α : Type u} (s : Stream'.Seq α) :
                                                                                                          (↑s).Productive
                                                                                                          Equations
                                                                                                          • =
                                                                                                          theorem Stream'.WSeq.toSeq_ofSeq {α : Type u} (s : Stream'.Seq α) :
                                                                                                          (↑s).toSeq = s
                                                                                                          def Stream'.WSeq.ret {α : Type u} (a : α) :

                                                                                                          The monadic return a is a singleton list containing a.

                                                                                                          Equations
                                                                                                          Instances For
                                                                                                            @[simp]
                                                                                                            theorem Stream'.WSeq.map_nil {α : Type u} {β : Type v} (f : αβ) :
                                                                                                            Stream'.WSeq.map f Stream'.WSeq.nil = Stream'.WSeq.nil
                                                                                                            @[simp]
                                                                                                            theorem Stream'.WSeq.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (s : Stream'.WSeq α) :
                                                                                                            @[simp]
                                                                                                            theorem Stream'.WSeq.map_think {α : Type u} {β : Type v} (f : αβ) (s : Stream'.WSeq α) :
                                                                                                            Stream'.WSeq.map f s.think = (Stream'.WSeq.map f s).think
                                                                                                            @[simp]
                                                                                                            theorem Stream'.WSeq.map_id {α : Type u} (s : Stream'.WSeq α) :
                                                                                                            @[simp]
                                                                                                            theorem Stream'.WSeq.map_ret {α : Type u} {β : Type v} (f : αβ) (a : α) :
                                                                                                            @[simp]
                                                                                                            theorem Stream'.WSeq.map_append {α : Type u} {β : Type v} (f : αβ) (s : Stream'.WSeq α) (t : Stream'.WSeq α) :
                                                                                                            Stream'.WSeq.map f (s.append t) = (Stream'.WSeq.map f s).append (Stream'.WSeq.map f t)
                                                                                                            theorem Stream'.WSeq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : Stream'.WSeq α) :
                                                                                                            theorem Stream'.WSeq.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : Stream'.WSeq α} :
                                                                                                            a sf a Stream'.WSeq.map f s
                                                                                                            theorem Stream'.WSeq.exists_of_mem_join {α : Type u} {a : α} {S : Stream'.WSeq (Stream'.WSeq α)} :
                                                                                                            a S.join∃ (s : Stream'.WSeq α), s S a s
                                                                                                            theorem Stream'.WSeq.exists_of_mem_bind {α : Type u} {β : Type v} {s : Stream'.WSeq α} {f : αStream'.WSeq β} {b : β} (h : b s.bind f) :
                                                                                                            ∃ (a : α), a s b f a
                                                                                                            theorem Stream'.WSeq.destruct_map {α : Type u} {β : Type v} (f : αβ) (s : Stream'.WSeq α) :
                                                                                                            theorem Stream'.WSeq.liftRel_map {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} {f1 : αγ} {f2 : βδ} (h1 : Stream'.WSeq.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bS (f1 a) (f2 b)) :
                                                                                                            theorem Stream'.WSeq.map_congr {α : Type u} {β : Type v} (f : αβ) {s : Stream'.WSeq α} {t : Stream'.WSeq α} (h : s t) :

                                                                                                            auxiliary definition of destruct_append over weak sequences

                                                                                                            Equations
                                                                                                            Instances For
                                                                                                              theorem Stream'.WSeq.destruct_append {α : Type u} (s : Stream'.WSeq α) (t : Stream'.WSeq α) :
                                                                                                              (s.append t).destruct = s.destruct.bind (Stream'.WSeq.destruct_append.aux t)

                                                                                                              auxiliary definition of destruct_join over weak sequences

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                theorem Stream'.WSeq.destruct_join {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) :
                                                                                                                S.join.destruct = S.destruct.bind Stream'.WSeq.destruct_join.aux
                                                                                                                theorem Stream'.WSeq.liftRel_append {α : Type u} {β : Type v} (R : αβProp) {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq α} {t1 : Stream'.WSeq β} {t2 : Stream'.WSeq β} (h1 : Stream'.WSeq.LiftRel R s1 t1) (h2 : Stream'.WSeq.LiftRel R s2 t2) :
                                                                                                                Stream'.WSeq.LiftRel R (s1.append s2) (t1.append t2)
                                                                                                                theorem Stream'.WSeq.liftRel_join.lem {α : Type u} {β : Type v} (R : αβProp) {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq β)} {U : Stream'.WSeq αStream'.WSeq βProp} (ST : Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) (HU : ∀ (s1 : Stream'.WSeq α) (s2 : Stream'.WSeq β), (∃ (s : Stream'.WSeq α), ∃ (t : Stream'.WSeq β), ∃ (S : Stream'.WSeq (Stream'.WSeq α)), ∃ (T : Stream'.WSeq (Stream'.WSeq β)), s1 = s.append S.join s2 = t.append T.join Stream'.WSeq.LiftRel R s t Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T)U s1 s2) {a : Option (α × Stream'.WSeq α)} (ma : a S.join.destruct) :
                                                                                                                ∃ (b : Option (β × Stream'.WSeq β)), b T.join.destruct Stream'.WSeq.LiftRelO R U a b
                                                                                                                theorem Stream'.WSeq.liftRel_join {α : Type u} {β : Type v} (R : αβProp) {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq β)} (h : Stream'.WSeq.LiftRel (Stream'.WSeq.LiftRel R) S T) :
                                                                                                                Stream'.WSeq.LiftRel R S.join T.join
                                                                                                                theorem Stream'.WSeq.join_congr {α : Type u} {S : Stream'.WSeq (Stream'.WSeq α)} {T : Stream'.WSeq (Stream'.WSeq α)} (h : Stream'.WSeq.LiftRel Stream'.WSeq.Equiv S T) :
                                                                                                                S.join T.join
                                                                                                                theorem Stream'.WSeq.liftRel_bind {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : αβProp) (S : γδProp) {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β} {f1 : αStream'.WSeq γ} {f2 : βStream'.WSeq δ} (h1 : Stream'.WSeq.LiftRel R s1 s2) (h2 : ∀ {a : α} {b : β}, R a bStream'.WSeq.LiftRel S (f1 a) (f2 b)) :
                                                                                                                Stream'.WSeq.LiftRel S (s1.bind f1) (s2.bind f2)
                                                                                                                theorem Stream'.WSeq.bind_congr {α : Type u} {β : Type v} {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq α} {f1 : αStream'.WSeq β} {f2 : αStream'.WSeq β} (h1 : s1 s2) (h2 : ∀ (a : α), f1 a f2 a) :
                                                                                                                s1.bind f1 s2.bind f2
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.join_ret {α : Type u} (s : Stream'.WSeq α) :
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.join_map_ret {α : Type u} (s : Stream'.WSeq α) :
                                                                                                                (Stream'.WSeq.map Stream'.WSeq.ret s).join s
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.join_append {α : Type u} (S : Stream'.WSeq (Stream'.WSeq α)) (T : Stream'.WSeq (Stream'.WSeq α)) :
                                                                                                                (S.append T).join S.join.append T.join
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.bind_ret {α : Type u} {β : Type v} (f : αβ) (s : Stream'.WSeq α) :
                                                                                                                s.bind (Stream'.WSeq.ret f) Stream'.WSeq.map f s
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.ret_bind {α : Type u} {β : Type v} (a : α) (f : αStream'.WSeq β) :
                                                                                                                (Stream'.WSeq.ret a).bind f f a
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.map_join {α : Type u} {β : Type v} (f : αβ) (S : Stream'.WSeq (Stream'.WSeq α)) :
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.join_join {α : Type u} (SS : Stream'.WSeq (Stream'.WSeq (Stream'.WSeq α))) :
                                                                                                                SS.join.join (Stream'.WSeq.map Stream'.WSeq.join SS).join
                                                                                                                @[simp]
                                                                                                                theorem Stream'.WSeq.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Stream'.WSeq α) (f : αStream'.WSeq β) (g : βStream'.WSeq γ) :
                                                                                                                (s.bind f).bind g s.bind fun (x : α) => (f x).bind g