Stream'.Seq.terminated_stable
theorem Stream'.Seq.terminated_stable :
∀ {α : Type u} (s : Stream'.Seq α) {m n : ℕ}, m ≤ n → s.TerminatedAt m → s.TerminatedAt n
This theorem states that for any type `α`, and any sequence `s` of type `α`, if the sequence `s` terminates at position `m`, then it also terminates at any position `n` where `n` is greater than or equal to `m`. In other words, once a sequence has ended, all subsequent positions in the sequence are also at the end of the sequence.
More concisely: If a sequence `s` of type `α` terminates at position `m`, then it also terminates at every position `n` with `n ≥ m`.
|
Stream'.Seq.cons_append
theorem Stream'.Seq.cons_append :
∀ {α : Type u} (a : α) (s t : Stream'.Seq α), (Stream'.Seq.cons a s).append t = Stream'.Seq.cons a (s.append t)
The `Stream'.Seq.cons_append` theorem states that for any type `α`, any element `a` of type `α`, and any two sequences `s` and `t` of type `α`, appending sequence `t` to the sequence obtained by prepending `a` to sequence `s` (`Stream'.Seq.append (Stream'.Seq.cons a s) t`) is equivalent to prepending `a` to the sequence obtained by appending `s` and `t` (`Stream'.Seq.cons a (Stream'.Seq.append s t)`). This is a property of sequence concatenation and prepending in potentially infinite lists, which mirrors the traditional property of list concatenation and cons operation in finite lists.
More concisely: For any type `α` and sequences `s`, `t` of type `α`, `Stream'.Seq.cons_append (Stream'.Seq.cons a s) t` is equal to `Stream'.Seq.cons a (Stream'.Seq.append s t)`.
|
Stream'.Seq.map_get?
theorem Stream'.Seq.map_get? :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.Seq α) (n : ℕ),
(Stream'.Seq.map f s).get? n = Option.map f (s.get? n)
The theorem `Stream'.Seq.map_get?` states that for any types `α` and `β`, a function `f` from `α` to `β`, a sequence `s` of type `α`, and a natural number `n`, the `n`-th element of the sequence obtained by mapping `f` over `s` is equal to the result of applying `f` to the `n`-th element of `s`. In other words, mapping a function over a sequence and then getting the `n`-th element is the same as first getting the `n`-th element and then applying the function.
More concisely: For any types α and β, function f from α to β, sequence s of length n + 1 in α, and natural number n, the (n+1)-th element of the sequence obtained by applying f to each element of s is equal to f applied to the n-th element of s.
|
Stream'.Seq.destruct_eq_cons
theorem Stream'.Seq.destruct_eq_cons :
∀ {α : Type u} {s : Stream'.Seq α} {a : α} {s' : Stream'.Seq α},
s.destruct = some (a, s') → s = Stream'.Seq.cons a s'
This theorem, `Stream'.Seq.destruct_eq_cons`, states that for any type `α`, and for any sequences `s` and `s'` of type `α`, and for any element `a` of type `α`, if the destruct operation on sequence `s` yields `some` tuple consisting of `a` and `s'`, then the sequence `s` is equal to the sequence obtained by prepending `a` to `s'`. In other words, if destructing a sequence gives us an element and another sequence, this original sequence must have been constructed by consing (adding at the beginning) that element onto the second sequence.
More concisely: If two sequences `s` and `s'` of type `α`, and an element `a` of type `α`, satisfy `s = some (a, s')` from the destruct operation on `s`, then `s` is equal to the sequence obtained by appending `a` to `s'`.
|
Stream'.Seq.ext
theorem Stream'.Seq.ext : ∀ {α : Type u} {s t : Stream'.Seq α}, (∀ (n : ℕ), s.get? n = t.get? n) → s = t
This theorem states that for any two sequences `s` and `t` of the same type `α`, if for all natural numbers `n`, the `n`-th element of sequence `s` is the same as the `n`-th element of sequence `t`, then the sequences `s` and `t` are equal. In other words, two sequences are equal if and only if their corresponding elements are equal at every position.
More concisely: Two sequences of the same type are equal if and only if they have identical elements at corresponding positions.
|
Stream'.Seq.map_cons
theorem Stream'.Seq.map_cons :
∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream'.Seq α),
Stream'.Seq.map f (Stream'.Seq.cons a s) = Stream'.Seq.cons (f a) (Stream'.Seq.map f s)
This theorem, named `Stream'.Seq.map_cons`, states that for any types `α` and `β`, any function `f` from `α` to `β`, any element `a` of type `α`, and any sequence `s` of type `α`, mapping function `f` over the sequence obtained by prepending `a` to `s` is equivalent to prepending `f(a)` to the sequence obtained by mapping `f` over `s`. In essence, this theorem describes the property of the function `Stream'.Seq.map` commuting with the function `Stream'.Seq.cons`, a key characteristic of the functorial nature of sequences.
More concisely: For any types `α` and `β`, functions `f : α → β`, elements `a : α`, and sequences `s : Stream α`, the application of `f` to the sequence obtained by consing `a` to `s` is equal to the sequence obtained by consing `f a` to the sequence obtained by applying `f` to `s`.
|
Stream'.Seq.destruct_cons
theorem Stream'.Seq.destruct_cons :
∀ {α : Type u} (a : α) (s : Stream'.Seq α), (Stream'.Seq.cons a s).destruct = some (a, s)
The theorem `Stream'.Seq.destruct_cons` states that for any type `α` and any element `a` of that type and sequence `s` of the same type, when we append the element to the start of the sequence using `Stream'.Seq.cons a s` and then apply the `Stream'.Seq.destruct` function, we get `some (a, s)`. In essence, destructing a sequence that had an element prepended to it will yield the prepended element and the original sequence.
More concisely: For any type `α` and element `a` of `α` and sequence `s` of type `Stream α`, `Stream.destruct (Stream.cons a s) = some (a, s)`.
|
Stream'.Seq.coinduction2
theorem Stream'.Seq.coinduction2 :
∀ {α : Type u} {β : Type v} (s : Stream'.Seq α) (f g : Stream'.Seq α → Stream'.Seq β),
(∀ (s : Stream'.Seq α),
Stream'.Seq.BisimO (fun s1 s2 => ∃ s, s1 = f s ∧ s2 = g s) (f s).destruct (g s).destruct) →
f s = g s
The theorem `Stream'.Seq.coinduction2` states that for any sequence `s` of type `α` and any two functions `f` and `g` from sequences of `α` to sequences of `β`, if for all sequences `s` of `α`, the `Stream'.Seq.BisimO` relation holds between the destruction of `f s` and `g s` (where this relation is defined as the existence of a sequence such that `s1 = f s` and `s2 = g s`), then `f s = g s`. In simpler terms, if two sequence transformations `f` and `g` have the same effect on the structure of all sequences, as captured by the bisimulation relation, then `f s` equals `g s` for any sequence `s`.
More concisely: If for all sequences `s`, the `Stream.Seq.BisimO` relation holds between `fs` and `gs`, then `fs = gs`.
|
Stream'.Seq.map_tail
theorem Stream'.Seq.map_tail :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Stream'.Seq α),
Stream'.Seq.map f s.tail = (Stream'.Seq.map f s).tail
This theorem, named `Stream'.Seq.map_tail`, states that for all types `α` and `β` and for all functions `f` from `α` to `β` and for any sequence `s` of type `α`, mapping the function `f` over the tail of the sequence `s` is the same as taking the tail of the sequence that results from mapping `f` over `s`. In other words, the ordering of applying the map operation and the tail operation does not matter. This can be seen as a property of commutativity between the two operations 'map' and 'tail' on sequences.
More concisely: For all types `α` and `β` and functions `f` from `α` to `β`, the operation of taking the tail of the sequence obtained by mapping `f` over a sequence `s` is equal to mapping `f` over the tail of sequence `s`.
|
Stream'.Seq.join_nil
theorem Stream'.Seq.join_nil : ∀ {α : Type u}, Stream'.Seq.nil.join = Stream'.Seq.nil
This theorem states that for all types `α`, the operation of joining an empty sequence of sequences (conducted by the function `Stream'.Seq.join`) results in an empty sequence. The function `Stream'.Seq.join` flattens a sequence of sequences, and `Stream'.Seq.nil` represents an empty sequence. This theorem essentially asserts that joining or flattening an empty sequence of sequences does not produce any elements, hence the result remains an empty sequence.
More concisely: For all types `α`, the operation of joining an empty sequence of sequences of `α` results in an empty sequence.
|
Stream'.Seq.get?_nil
theorem Stream'.Seq.get?_nil : ∀ {α : Type u} (n : ℕ), Stream'.Seq.nil.get? n = none
The theorem `Stream'.Seq.get?_nil` states that for all types `α` and for any natural number `n`, when you try to get the `n`th element of an empty sequence, you get `None`. This essentially means that retrieving an element from an empty sequence always results in `None` regardless of the index `n`, signifying that the element does not exist.
More concisely: For all types `α` and for every empty sequence `x : Stream α`, `get? (n: nat) x = None`.
|
Stream'.Seq.corec_eq
theorem Stream'.Seq.corec_eq :
∀ {α : Type u} {β : Type v} (f : β → Option (α × β)) (b : β),
(Stream'.Seq.corec f b).destruct = Stream'.Seq.omap (Stream'.Seq.corec f) (f b)
The theorem `Stream'.Seq.corec_eq` establishes an equality between the destruction of a coinductively built sequence and the functorial action on the function used to build this sequence. Specifically, for any types `α` and `β`, and a function `f` from `β` to `Option (α × β)` and an element `b` of type `β`, the result of destructing the sequence formed by co-recursively applying `f` to `b` (using `Stream'.Seq.corec`) is the same as the outcome of applying the functorial action (`Stream'.Seq.omap`) of `Stream'.Seq.corec f` to `f b`. This theorem essentially links the operations of destruction and functorial action in the context of coinductively generated sequences.
More concisely: For any types `α` and `β` and function `f` from `β` to `Option (α × β)`, the co-recursively constructed sequence `Stream'.Seq.corec f` applied to an element `b` of type `β` is equal to the functorial action `Stream'.Seq.omap (Stream'.Seq.corec f)` applied to `f` on `b`.
|
Stream'.Seq.join_cons
theorem Stream'.Seq.join_cons :
∀ {α : Type u} (a : α) (s : Stream'.Seq α) (S : Stream'.Seq (Stream'.Seq1 α)),
(Stream'.Seq.cons (a, s) S).join = Stream'.Seq.cons a (s.append S.join)
The theorem `Stream'.Seq.join_cons` states that for any type `α`, given an element `a` of type `α`, a sequence `s` of type `α`, and a sequence `S` of non-empty sequences of type `α`, if we join the sequence that results from prepending the pair `(a, s)` to `S`, it is equivalent to prepending `a` to the sequence obtained by appending `s` to the joined sequence of `S`. In other words, joining a sequence that starts with `(a, s)` is the same as starting with `a` and then following with the rest of `s` and the joined sequence of `S`.
More concisely: For any type `α` and any `a : α` and non-empty sequences `s : List α` and `S : List (List α)`, the sequences obtained by prepending `(a, s)` to `S` and appending `s` to the sequence obtained by joining `S` are equal.
|
Stream'.Seq.map_comp
theorem Stream'.Seq.map_comp :
∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Stream'.Seq α),
Stream'.Seq.map (g ∘ f) s = Stream'.Seq.map g (Stream'.Seq.map f s)
The theorem `Stream'.Seq.map_comp` asserts that for all types `α`, `β`, and `γ`, and for all functions `f` from `α` to `β` and `g` from `β` to `γ`, and for any sequence `s` of type `α`, mapping the composition of `g` and `f` over the sequence `s` is equivalent to first mapping `f` over `s`, and then mapping `g` over the resulting sequence. This is a statement of function composition compatibility with sequence mapping, a property akin to one in function composition in standard mathematics: `(g ∘ f)(x) = g(f(x))` for all `x` in the domain of `f`.
More concisely: For any types `α`, `β`, `γ`, functions `f : α → β` and `g : β → γ`, and sequences `s : Stream α`, the application of `g` followed by `f` to each element in `s` is equal to the application of `f` followed by `g` to `s`. In other words, `Stream.map (g ∘ f) s = Stream.map g (Stream.map f s)`.
|
Stream'.Seq.ge_stable
theorem Stream'.Seq.ge_stable :
∀ {α : Type u} (s : Stream'.Seq α) {aₙ : α} {n m : ℕ}, m ≤ n → s.get? n = some aₙ → ∃ aₘ, s.get? m = some aₘ := by
sorry
The theorem `Stream'.Seq.ge_stable` states that for any sequence `s` of a certain type `α` and any two natural numbers `m` and `n` such that `m` is less than or equal to `n`, if the `n`-th element of the sequence `s` is a certain value `aₙ`, then there exists a value `aₘ` such that the `m`-th element of the sequence `s` is `aₘ`. This expresses a stability property of these sequences: if an element exists at a certain position, then an element also exists at all preceding positions.
More concisely: For any sequence `s` of type `α` and natural numbers `m ≤ n`, if `s[n] = aₙ`, then there exists `aₘ` such that `s[m] = aₘ`.
|
Stream'.Seq.map_id
theorem Stream'.Seq.map_id : ∀ {α : Type u} (s : Stream'.Seq α), Stream'.Seq.map id s = s
This theorem, called `Stream'.Seq.map_id`, states that for any sequence of elements of any type `α`, mapping the identity function over this sequence leaves the sequence unchanged. In other words, for all sequences `s` of type `α`, the operation of mapping the identity function on `s` (denoted by `Stream'.Seq.map id s`) gives us the same sequence `s` again. This axiom formalizes the intuition that applying the identity function doesn't change the elements of the sequence.
More concisely: For any sequence `s` of type `α`, the operation `Stream'.Seq.map id s` equals the sequence `s`.
|
Stream'.Seq.ofList_cons
theorem Stream'.Seq.ofList_cons : ∀ {α : Type u} (a : α) (l : List α), ↑(a :: l) = Stream'.Seq.cons a ↑l
This theorem, `Stream'.Seq.ofList_cons`, states that for all types `α`, any element `a` of type `α`, and any list `l` of elements of type `α`, coercing (`↑`) the result of prepending `a` to `l` (denoted `a :: l`) to a sequence is equivalent to first coercing `l` to a sequence and then prepending `a` to the resulting sequence using the `Stream'.Seq.cons` function. Essentially, this theorem is establishing that the order of operations of prepending an element and converting from a list to a sequence does not matter.
More concisely: For all types `α` and elements `a` of type `α` and lists `l` of type `α`, the sequence obtained by prepending `a` to `l` is equivalent to prepending `a` to the sequence obtained from `l`.
|
Stream'.Seq.nil_append
theorem Stream'.Seq.nil_append : ∀ {α : Type u} (s : Stream'.Seq α), Stream'.Seq.nil.append s = s
This theorem states that for all sequences `s` of any type `α`, appending the empty sequence to `s` results in `s` itself. In other words, it states that the operation of appending an empty sequence to any given sequence has no effect, and the original sequence remains unchanged. This mirrors the behavior we would expect in standard list or string concatenation where an element concatenated with an empty element doesn't change the original element.
More concisely: For all sequences `s` of type `α`, appending the empty sequence to `s` yields `s`.
|