Stream'.drop_succ
theorem Stream'.drop_succ : ∀ {α : Type u} (n : ℕ) (s : Stream' α), Stream'.drop n.succ s = Stream'.drop n s.tail := by
sorry
The theorem `Stream'.drop_succ` states that for any type `α`, any natural number `n`, and any stream `s` of type `α`, dropping the first `n+1` elements from `s` is equivalent to first removing the head of the stream (using `Stream'.tail`) and then dropping the first `n` elements from the resulting stream.
More concisely: For any type α, natural number n, and stream s of type α, (drop (n+1) s) = tail (drop n s).
|
Stream'.eta
theorem Stream'.eta : ∀ {α : Type u} (s : Stream' α), Stream'.cons s.head s.tail = s
The theorem `Stream'.eta` states that for any stream `s` of elements of any type `α`, if we take the head of `s` (the first element), then construct a new stream by prepending this head to the tail of `s` (the rest of the elements), we will end up with the original stream `s`. Essentially, this theorem captures the property that a stream is completely characterized by its head and its tail.
More concisely: For any stream `s` of type `α`, the stream obtained by prepending the head of `s` to the tail of `s` is equal to the original stream `s`.
|
Stream'.corec_eq
theorem Stream'.corec_eq :
∀ {α : Type u} {β : Type v} (f : α → β) (g : α → α) (a : α),
Stream'.corec f g a = Stream'.cons (f a) (Stream'.corec f g (g a))
The `Stream'.corec_eq` theorem states that for any types `α` and `β`, and for any functions `f` of type `α → β` and `g` of type `α → α`, and any element `a` of type `α`, the co-recursion of `f`, `g`, and `a` on a stream is equivalent to prepending the application of `f` to `a` (`f a`) onto the co-recursion of `f`, `g`, and the application of `g` to `a` (`g a`) on the stream. In simpler terms, this theorem establishes the behavior of the `Stream'.corec` function in terms of the `Stream'.cons` function and verifies its correctness in constructing streams using a co-recursive process.
More concisely: For any types `α` and `β`, functions `f : α → β` and `g : α → α`, and element `a : α`, the co-recursive definition of a stream using `Stream'.corec f g a` is equivalent to prepending `f a` to the stream obtained by co-recursively applying `f` and `g` starting from `g a`.
|
Stream'.tail_iterate
theorem Stream'.tail_iterate :
∀ {α : Type u} (f : α → α) (a : α), (Stream'.iterate f a).tail = Stream'.iterate f (f a)
This theorem, `Stream'.tail_iterate`, states that for any type `α`, any function `f` from `α` to `α`, and any element `a` of type `α`, the tail of the stream generated by iterating `f` starting at `a` is the same as the stream generated by iterating `f` starting at `f(a)`. In other words, removing the first element from the stream of iterates of `f` is equivalent to starting the iteration from the next step.
More concisely: For any type `α`, function `f` from `α` to `α`, and element `a` of type `α`, the tail of the iterated stream `(iterate f a)` is equal to the iterated stream `(iterate f (f a))`.
|
Stream'.cons_append_stream
theorem Stream'.cons_append_stream :
∀ {α : Type u} (a : α) (l : List α) (s : Stream' α), a :: l ++ₛ s = Stream'.cons a (l ++ₛ s)
This theorem, `Stream'.cons_append_stream`, states that for any type `α`, any element `a` of type `α`, any list `l` of elements of type `α`, and any Stream `s` of elements of type `α`, prepending `a` to the concatenation of `l` and `s` (`a :: l ++ₛ s`) is equivalent to creating a new Stream where `a` is the first element and the concatenation of `l` and `s` forms the rest of the Stream (`Stream'.cons a (l ++ₛ s)`).
More concisely: For any type α, the stream obtained by consing an element a to the concatenation of a list l and a stream s is equal to the stream obtained by consing a to the stream formed by the concatenation of l and s. In Lean notation: ∀α, a :: l ++ₛ s = Stream.cons a (l ++ₛ s).
|
Stream'.take_succ
theorem Stream'.take_succ :
∀ {α : Type u} (n : ℕ) (s : Stream' α), Stream'.take n.succ s = s.head :: Stream'.take n s.tail
The theorem `Stream'.take_succ` states that for any type `α`, any natural number `n`, and any stream `s` of type `α`, taking the first `n+1` elements of the stream `s` gives a list that starts with the first element of `s` (i.e., `Stream'.head s`), followed by the first `n` elements from the remainder of the stream (i.e., `Stream'.take n (Stream'.tail s)`). In other words, it describes how to construct a list from the first `n+1` elements of a stream by successively taking the head of the stream and the first `n` elements from the tail of the stream.
More concisely: For any stream `s` of type `α` and natural number `n`, the first `n+1` elements of `s` form a list equal to the cons of `Stream.head s` and the first `n` elements of `Stream.tail s`. (In mathematical notation: `take (n+1) s = cons (Stream.head s) (take n (Stream.tail s))`)
|
Stream'.coinduction
theorem Stream'.coinduction :
∀ {α : Type u} {s₁ s₂ : Stream' α},
s₁.head = s₂.head → (∀ (β : Type u) (fr : Stream' α → β), fr s₁ = fr s₂ → fr s₁.tail = fr s₂.tail) → s₁ = s₂
The `Stream'.coinduction` theorem expresses a coinduction principle for infinite streams of elements of a given type `α`. It asserts that for any two streams `s₁` and `s₂` of type `α`, if the head of `s₁` is equal to the head of `s₂` and for all types `β` and all functions `fr` from a stream to type `β`, if `fr` applied to `s₁` is equal to `fr` applied to `s₂`, then `fr` applied to the tail of `s₁` is equal to `fr` applied to the tail of `s₂`. This implies that the two streams `s₁` and `s₂` are equal. In other words, two streams are the same if they have the same head and their tails behave the same under any function from streams to another type.
More concisely: If two infinite streams over a type have equal heads and agree on the behavior of every function from streams to another type when applied to their tails, then the streams are equal.
|
Stream'.map_cons
theorem Stream'.map_cons :
∀ {α : Type u} {β : Type v} (f : α → β) (a : α) (s : Stream' α),
Stream'.map f (Stream'.cons a s) = Stream'.cons (f a) (Stream'.map f s)
The theorem `Stream'.map_cons` states that for any types `α` and `β`, any function `f` from `α` to `β`, any element `a` of type `α`, and any infinite sequence `s` (or stream) of elements of type `α`, the operation of mapping the function `f` over the stream that results from prepending `a` to `s` is the same as the operation of prepending `f(a)` to the stream that results from mapping `f` over `s`. In other words, it establishes that the `map` operation commutes with the `cons` operation, which is a key property in functional programming and stream processing.
More concisely: For any types `α` and `β`, functions `f` from `α` to `β`, elements `a` of type `α`, and infinite streams `s` over `α`, the following equality holds: `map f (cons a s) = cons (f a) (map f s)`.
|
Stream'.ext
theorem Stream'.ext : ∀ {α : Type u} {s₁ s₂ : Stream' α}, (∀ (n : ℕ), s₁.get n = s₂.get n) → s₁ = s₂
This theorem, `Stream'.ext`, states that for any type `α` and any two streams `s₁` and `s₂` of `α`, if every corresponding pair of elements from `s₁` and `s₂` are equal (i.e., the `n`-th element of `s₁` is equal to the `n`-th element of `s₂` for every natural number `n`), then the two streams `s₁` and `s₂` are identical. In other words, two streams are considered the same if they have the same elements in the same order.
More concisely: If two streams of the same type have equal elements at corresponding positions, then they are equal.
|
Stream'.get_succ
theorem Stream'.get_succ : ∀ {α : Type u} (n : ℕ) (s : Stream' α), s.get n.succ = s.tail.get n
The theorem `Stream'.get_succ` states that for any type `α`, natural number `n`, and stream `s` of type `α`, getting the `n+1`-th element of the stream `s` is the same as first getting the tail of the `s` and then getting its `n`-th element. In other words, the tail operation on a stream effectively reduces the index of each element by one. This is in alignment with the general understanding of the tail operation in the context of sequences or lists, where it usually refers to the remaining sequence after its first element has been removed.
More concisely: For any type `α`, natural number `n`, and stream `s` of type `α`, the `(n + 1)`-th element of `s` equals the `n`-th element of the tail of `s`.
|
Stream'.tail_cons
theorem Stream'.tail_cons : ∀ {α : Type u} (a : α) (s : Stream' α), (Stream'.cons a s).tail = s
The theorem `Stream'.tail_cons` states that for all types `α`, and for any element `a` of type `α` and any stream `s` of type `α`, the tail of the stream that results from prepending `a` to `s` is equal to `s` itself. In other words, if you prepend an element to a stream and then drop the first element of the new stream, you get the original stream back.
More concisely: For all types `α` and streams `s` of type `α`, the tail of the stream obtained by prepending an element `a` to `s` is equal to `s`. In other words, `Stream.tail (a :: s) = s`.
|
Stream'.drop_drop
theorem Stream'.drop_drop :
∀ {α : Type u} (n m : ℕ) (s : Stream' α), Stream'.drop n (Stream'.drop m s) = Stream'.drop (n + m) s
This theorem states that for any type `α`, any natural numbers `n` and `m`, and any stream `s` of `α`, dropping `n` elements from the stream produced by dropping `m` elements of `s` is the same as dropping `n + m` elements from the original stream `s` directly. Essentially, this theorem asserts the associativity of the "drop" function on streams: two consecutive "drop" operations can be combined into a single "drop" operation with the sum of the original "drop" counts.
More concisely: For any type `α`, given natural numbers `n` and `m`, the operation of dropping `n` elements from the stream obtained by dropping `m` elements is equal to dropping `n + m` elements directly from the original stream.
|
Stream'.eq_of_bisim
theorem Stream'.eq_of_bisim :
∀ {α : Type u} (R : Stream' α → Stream' α → Prop),
Stream'.IsBisimulation R → ∀ {s₁ s₂ : Stream' α}, R s₁ s₂ → s₁ = s₂
The theorem `Stream'.eq_of_bisim` states that for any type `α` and any relation `R` on streams of type `α`, if `R` is a bisimulation (meaning for any two streams `s₁` and `s₂`, if they are related by `R`, then they have the same head and their tails are also related by `R`), then any two streams `s₁` and `s₂` that are related by `R` are actually equal. In other words, bisimulations preserve the identity of streams.
More concisely: If `R` is a bisimulation relation on streams of type `α`, then for any `s₁` and `s₂` related by `R`, we have `s₁ = s₂`.
|