Stream'.WSeq.liftRel_destruct_iff
theorem Stream'.WSeq.liftRel_destruct_iff :
∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
Stream'.WSeq.LiftRel R s t ↔
Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) s.destruct t.destruct
The theorem `Stream'.WSeq.liftRel_destruct_iff` establishes an equivalence between two conditions when given two weak sequences, `s` and `t`, of types `α` and `β` respectively and a relation `R` between `α` and `β`. The conditions are:
1. The weak sequences `s` and `t` are `LiftRel R` related, meaning either both are empty, or they are both non-empty and the first elements of each are `R` related and the rest of the sequences are `LiftRel R` related.
2. The computations resulting from destructing `s` and `t` are `LiftRel` related with respect to the relation `Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)`, meaning that if the destruction of `s` terminates with a certain value, then the destruction of `t` terminates with a value that is related to the former by this relation, and vice versa.
This theorem provides a connection between sequence-relatedness and the relatedness of their deconstructed computations, which can be used to simplify proofs involving streams and computations.
More concisely: Given two weak sequences `s` and `t` of types `α` and `β` respectively, and a relation `R` between `α` and `β`, the weak sequences `s` and `t` are `LiftRel R` related if and only if the computations resulting from their destructive recursion are `LiftRel` related with respect to `Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)`.
|
Stream'.WSeq.LiftRelO.imp_right
theorem Stream'.WSeq.LiftRelO.imp_right :
∀ {α : Type u} {β : Type v} (R : α → β → Prop) {C D : Stream'.WSeq α → Stream'.WSeq β → Prop},
(∀ (s : Stream'.WSeq α) (t : Stream'.WSeq β), C s t → D s t) →
∀ {o : Option (α × Stream'.WSeq α)} {p : Option (β × Stream'.WSeq β)},
Stream'.WSeq.LiftRelO R C o p → Stream'.WSeq.LiftRelO R D o p
The theorem `Stream'.WSeq.LiftRelO.imp_right` states that for any types `α` and `β`, and any relation `R` between `α` and `β`, if for any weak sequences `s` of `α` and `t` of `β`, a relation `C` between `s` and `t` implies a relation `D` between `s` and `t`, then for any option `o` of a pair of an `α` and a weak sequence of `α`, and any option `p` of a pair of a `β` and a weak sequence of `β`, if the lifted relation `LiftRelO` with respect to `R` and `C` holds between `o` and `p`, then the lifted relation `LiftRelO` with respect to `R` and `D` also holds between `o` and `p`.
In other words, if a relation `C` between two weak sequences implies another relation `D`, then the lifted versions of these relations with respect to another relation `R` and certain optional pairs also hold the implication relationship.
More concisely: If relation `C` implies relation `D` between weak sequences, then the lifted relations `LiftRelO(R, C)` and `LiftRelO(R, D)` hold the implication relationship for any type `α`, `β`, and option pairs of `α` and weak sequences of `α`, and `β` and weak sequences of `β`, with respect to relation `R`.
|
Stream'.WSeq.ofList_cons
theorem Stream'.WSeq.ofList_cons : ∀ {α : Type u} (a : α) (l : List α), ↑(a :: l) = Stream'.WSeq.cons a ↑l
This theorem, denoted as `Stream'.WSeq.ofList_cons`, establishes a property about weak sequences in the context of Stream' in Lean 4. For any type `α`, and any element `a` of type `α` and list `l` of elements of type `α`, it states that the weak sequence generated from the list obtained by prepending `a` to `l` (i.e., `a :: l`) is equal to the weak sequence obtained by invoking the `cons` operation on `a` and the weak sequence generated from `l`. In simpler terms, prepending an element to a list and converting it to a weak sequence is equivalent to prepending the same element to the weak sequence generated from the list.
More concisely: For any type `α` and elements `a` and `x` of type `α`, the weak sequence obtained from the list `a :: xs` is equal to the weak sequence obtained from `xs` by prepending `a` using the `cons` operation.
|
Stream'.WSeq.join_nil
theorem Stream'.WSeq.join_nil : ∀ {α : Type u}, Stream'.WSeq.nil.join = Stream'.WSeq.nil
The theorem `Stream'.WSeq.join_nil` states that for all types `α`, joining an empty weak sequence (`Stream'.WSeq.nil`) results in an empty weak sequence. In other words, the operation of joining does not produce any elements when applied to an empty weak sequence, irrespective of the type `α` of the elements that could potentially be in the sequence.
More concisely: For all types `α`, the join of an empty weak sequence `Stream'.WSeq.nil` is the empty weak sequence.
|
Stream'.WSeq.join_cons
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
The theorem `Stream'.WSeq.join_cons` states that for any type `α`, any weak sequence `s` of type `α` and any weak sequence `S` of weak sequences of type `α`, joining a weak sequence consisting of `s` and `S` is equivalent to appending `s` to the result of joining `S` after one computational step. In other words, prepending `s` to `S` before joining is the same as first thinking (computing for one step without producing any elements), then appending `s` to the joined `S`.
More concisely: For any type `α`, the join of a weak sequence `s` with the join of a weak sequence of weak sequences `S` is equivalent to appending `s` to the result of joining `S`, up to the next computation step.
|
Stream'.WSeq.exists_get?_of_mem
theorem Stream'.WSeq.exists_get?_of_mem : ∀ {α : Type u} {s : Stream'.WSeq α} {a : α}, a ∈ s → ∃ n, some a ∈ s.get? n
This theorem states that for any type `α`, any infinite sequence `s` of type `α`, and any element `a` of type `α`, if `a` is an element of `s`, then there exists a natural number `n` such that `a` is the `n`th element of `s`. In other words, if an element is in an infinite sequence, you can find its position in the sequence.
More concisely: For any type `α`, any infinite sequence `s` of type `α`, and any element `a` of type `α` in `s`, there exists a natural number `n` such that `a = s!(n)`, where `s!` denotes the `n`-th element of `s`.
|
Stream'.WSeq.destruct_nil
theorem Stream'.WSeq.destruct_nil : ∀ {α : Type u}, Stream'.WSeq.nil.destruct = Computation.pure none
The theorem `Stream'.WSeq.destruct_nil` states that for all types `α`, destructing an empty weak sequence (`Stream'.WSeq.nil`) results in a computation that immediately terminates with the result `none`. This is regardless of the particular type `α` of the elements that the sequence could potentially hold. Essentially, the theorem connects the concept of destructing an empty sequence in the weak sequence space with the concept of a computation that yields `none` instantaneously.
More concisely: For all types `α`, destructing an empty weak sequence `Stream'.WSeq.nil` in Lean 4 yields an immediate computation of `none`.
|
Stream'.WSeq.liftRel_destruct
theorem Stream'.WSeq.liftRel_destruct :
∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
Stream'.WSeq.LiftRel R s t →
Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)) s.destruct t.destruct
This theorem, `Stream'.WSeq.liftRel_destruct`, states that for any two types `α` and `β` and any relation `R` between `α` and `β`, if two weak sequences `s` and `t` (of types `α` and `β` respectively) are related by the `LiftRel R` relation, then the computations resulting from the destruction of `s` and `t` (i.e., `Stream'.WSeq.destruct s` and `Stream'.WSeq.destruct t` respectively) are related by the `Computation.LiftRel` relation applied to the `Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R)` relation. In other words, if `s` and `t` are related in a certain way, then the computations that deconstruct `s` and `t` are also related in a similar way.
More concisely: For any types `α` and `β` and relation `R` between them, if two weak sequences `s` and `t` of types `α` and `β` respectively are related by `LiftRel R`, then their destruction computations `Stream'.WSeq.destruct s` and `Stream'.WSeq.destruct t` are related by `Computation.LiftRel (Stream'.WSeq.LiftRelO R (Stream'.WSeq.LiftRel R))`.
|
Stream'.WSeq.flatten_pure
theorem Stream'.WSeq.flatten_pure :
∀ {α : Type u} (s : Stream'.WSeq α), Stream'.WSeq.flatten (Computation.pure s) = s
The theorem `Stream'.WSeq.flatten_pure` states that for every weak sequence `s` of some Type `α`, when `s` is encoded into a computation using the `Computation.pure` function and then flattened using the `Stream'.WSeq.flatten` function, it remains the same. This essentially demonstrates that the process of encoding a weak sequence into a computation and then flattening it doesn't change the weak sequence.
More concisely: For any weak sequence `s` of type `α`, the application of `Stream'.WSeq.flatten` to the computation obtained by encoding `s` using `Computation.pure` is equal to the original weak sequence `s`.
|
Stream'.WSeq.destruct_cons
theorem Stream'.WSeq.destruct_cons :
∀ {α : Type u} (a : α) (s : Stream'.WSeq α), (Stream'.WSeq.cons a s).destruct = Computation.pure (some (a, s)) := by
sorry
The theorem `Stream'.WSeq.destruct_cons` states that for any type `α` and any element `a` of type `α` and weak sequence `s` of type `α`, the result of destructing a weak sequence obtained by prepending `a` to `s` is equivalent to the computation that immediately terminates with the result `some (a, s)`. Here, a weak sequence is a possibly infinite sequence that can be partially undefined, and the `destruct` operation is used to deconstruct this sequence into its elements.
More concisely: For any type `α` and element `a` of type `α`, the destructed result of prepending `a` to a weak sequence `s` is equal to the `some` computation with value `(a, s)`.
|
Stream'.WSeq.destruct_think
theorem Stream'.WSeq.destruct_think : ∀ {α : Type u} (s : Stream'.WSeq α), s.think.destruct = s.destruct.think := by
sorry
The theorem `Stream'.WSeq.destruct_think` states that for any weak sequence `s` of an arbitrary type `α`, the computation action of destructing the weak sequence after one computational tick (done using the `Stream'.WSeq.think` function on `s`) is the same as the computation of destructing `s` delayed by one tick (done using the `Computation.think` function on `Stream'.WSeq.destruct s`). In other words, delaying the computation before or after the destruct action gives the same result.
More concisely: For any weak sequence `s` of type `α`, `Stream'.WSeq.think (Stream'.WSeq.destruct s) = Computation.think (Stream'.WSeq.destruct s).`
Or, in mathematical notation:
The computation of destructing a weak sequence `s` after one tick using `Stream'.WSeq.think` is equivalent to destructing `s` with a one-tick delay using `Computation.think`.
|
Stream'.WSeq.exists_of_liftRel_left
theorem Stream'.WSeq.exists_of_liftRel_left :
∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s : Stream'.WSeq α} {t : Stream'.WSeq β},
Stream'.WSeq.LiftRel R s t → ∀ {a : α}, a ∈ s → ∃ b ∈ t, R a b
The theorem `Stream'.WSeq.exists_of_liftRel_left` states that for every type `α` and `β`, and every relation `R` between `α` and `β`, if `s` and `t` are weak sequences of type `α` and `β` respectively such that `s` and `t` are related by the `LiftRel R` relation, then for any element `a` of `s`, there exists an element `b` in `t` such that `a` and `b` are related by the relation `R`.
More concisely: For every type `α`, `β`, and relation `R` between `α` and `β`, if `s` and `t` are weak sequences of type `α` and `β` respectively with `LiftRel R`(s, t), then for each `a` in `s`, there exists `b` in `t` such that `R(a, b)`.
|
Stream'.WSeq.map_comp
theorem Stream'.WSeq.map_comp :
∀ {α : Type u} {β : Type v} {γ : Type w} (f : α → β) (g : β → γ) (s : Stream'.WSeq α),
Stream'.WSeq.map (g ∘ f) s = Stream'.WSeq.map g (Stream'.WSeq.map f s)
The theorem `Stream'.WSeq.map_comp` states that for any types `α`, `β`, and `γ`, and any functions `f` from `α` to `β` and `g` from `β` to `γ`, and any weak sequence `s` of type `α`, mapping the composition of `g` and `f` over `s` is equivalent to first mapping `f` over `s` and then mapping `g` over the result. This theorem is essentially stating the property of function composition in the context of mapping over a weak sequence.
More concisely: For any types `α`, `β`, and `γ`, and functions `f : α → β` and `g : β → γ`, the mapping of `g ∘ f` over a weak sequence `s` of type `α` is equal to the composition of mapping `f` over `s` and then mapping `g` over the result.
|
Stream'.WSeq.flatten_think
theorem Stream'.WSeq.flatten_think :
∀ {α : Type u} (c : Computation (Stream'.WSeq α)), Stream'.WSeq.flatten c.think = (Stream'.WSeq.flatten c).think
The theorem `Stream'.WSeq.flatten_think` states that for any computation `c` of a weak sequence (a sequence of optional values) of any type `α`, running the computation `c` for one "tick" and then flattening the result is the same as first flattening the computation `c` and then running the result for one "tick". In other words, the order of flattening (converting a computation yielding a weak sequence into a weak sequence) and "thinking" (running a computation for one tick) doesn't change the final outcome of the computation. This theorem is essentially about the commutativity of these two operations.
More concisely: For any weak sequence computation `c` of type `α`, the result of thinking `c` and then flattening is equal to flattening `c` and then thinking the resulting weak sequence.
|
Stream'.WSeq.destruct_flatten
theorem Stream'.WSeq.destruct_flatten :
∀ {α : Type u} (c : Computation (Stream'.WSeq α)),
(Stream'.WSeq.flatten c).destruct = c >>= Stream'.WSeq.destruct
The theorem `Stream'.WSeq.destruct_flatten` states that for any computation `c` that yields a weak sequence of type `α`, the process of destructing the flattened version of `c` is the same as the process of destructing the weak sequence resulting from computing and then destructing `c`. In other words, it asserts that the operation of destructing a computation after flattening it is equivalent to the operation of computing a weak sequence first and then destructing it.
More concisely: For any computation `c` yielding a weak sequence of type `α`, destructing the flattened version of `c` is equivalent to first computing and then destructing the resulting weak sequence.
|