Computation.liftRel_bind
theorem Computation.liftRel_bind :
∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
{s2 : Computation β} {f1 : α → Computation γ} {f2 : β → Computation δ},
Computation.LiftRel R s1 s2 →
(∀ {a : α} {b : β}, R a b → Computation.LiftRel S (f1 a) (f2 b)) →
Computation.LiftRel S (s1.bind f1) (s2.bind f2)
This theorem, `Computation.liftRel_bind`, states that for any types `α`, `β`, `γ`, and `δ`, and any relations `R` and `S` on these types, if we have two computations `s1` and `s2` of type `α` and `β` respectively, and two functions `f1` and `f2` mapping `α` to `Computation γ` and `β` to `Computation δ` respectively, then if `s1` and `s2` are related by `R` and for any `a` in `α` and `b` in `β` that satisfy `R a b`, `f1 a` and `f2 b` are related by `S`, it follows that the computations resulting from binding `s1` to `f1` and `s2` to `f2` are related by `S` as well.
In simpler terms, if the start computations are related and the transformations maintain this relation under certain conditions, then the computations resulting from applying the transformations will also be related.
More concisely: For any types `α`, `β`, `γ`, `δ`, relations `R` and `S`, computations `s1 : Computation α`, `s2 : Computation β`, functions `f1 : α → Computation γ`, `f2 : β → Computation δ`, if `s1` and `s2` are related by `R` and for all `a : α` and `b : β` related by `R`, `f1 a` and `f2 b` are related by `S`, then `bind f1 s1` and `bind f2 s2` are related by `S`.
|
Computation.destruct_eq_think
theorem Computation.destruct_eq_think : ∀ {α : Type u} {s s' : Computation α}, s.destruct = Sum.inr s' → s = s'.think
The theorem `Computation.destruct_eq_think` states that for any type `α` and any two computations `s` and `s'` of type `α`, if the destructor of `s` yields `s'` encapsulated in the right component of the sum type (`Sum.inr s'`), then `s` must be a computation that delays for one "tick" and then performs the computation `s'` (i.e., `s = Computation.think s'`). In other words, if the destruction of a computation gives another computation, then the original computation is actually a delayed version of the resulting computation.
More concisely: If `s` and `s'` are computations of type `α` such that `s` destructs to `Sum.inr s'`, then `s` is equal to the delayed computation `Computation.think s'`.
|
Computation.LiftRel.imp
theorem Computation.LiftRel.imp :
∀ {α : Type u} {β : Type v} {R S : α → β → Prop},
(∀ {a : α} {b : β}, R a b → S a b) →
∀ (s : Computation α) (t : Computation β), Computation.LiftRel R s t → Computation.LiftRel S s t
This theorem states that for any types `α` and `β`, and any relations `R` and `S` between `α` and `β`, if `R` implies `S` for every pair of elements `(a, b)` from `α` and `β` respectively, then for any computations `s` of type `α` and `t` of type `β`, if the computation relation `LiftRel` holds for `R`, `s`, and `t`, then it also holds for `S`, `s`, and `t`. In other words, if a relation `R` between the results of two computations implies another relation `S`, and `R` holds according to the `LiftRel` definition, then `S` also holds according to the `LiftRel` definition.
More concisely: If relation R implies relation S between types α and β, and LiftRel(R) holds for computations s : α and t : β, then LiftRel(S) also holds for s and t.
|
Computation.destruct_think
theorem Computation.destruct_think : ∀ {α : Type u} (s : Computation α), s.think.destruct = Sum.inr s
The theorem `Computation.destruct_think` states that for any type `α` and any computation `s` of type `α`, destructing (or breaking down) the computation after delaying it for one "tick" using the `Computation.think` function will always return the original computation `s`. This is represented by `Sum.inr s` in the sum type `α ⊕ Computation α`, where `Sum.inr` indicates the right element of the sum type, referring to the original computation `s`.
More concisely: For any type `α` and computation `s` of type `α`, `Computation.think (Computation.delay s) = s`. (The `Computation.think` function applied to a delayed computation returns the original computation.)
|
Computation.mem_unique
theorem Computation.mem_unique : ∀ {α : Type u} {s : Computation α} {a b : α}, a ∈ s → b ∈ s → a = b
The theorem `Computation.mem_unique` states that for any type `α`, given a computation `s` of type `α`, and any two elements `a` and `b` of type `α`, if `a` is in `s` and `b` is in `s`, then `a` must be equal to `b`. This ensures the uniqueness of the element within a computation, i.e., a computation can only yield a unique result.
More concisely: For any computation `s` and type `α`, if `α` contains elements `a` and `b` such that `a` is in `s` and `b` is in `s`, then `a = b`.
|
Computation.exists_of_mem_map
theorem Computation.exists_of_mem_map :
∀ {α : Type u} {β : Type v} {f : α → β} {b : β} {s : Computation α}, b ∈ Computation.map f s → ∃ a ∈ s, f a = b
The theorem `Computation.exists_of_mem_map` states that for all types `α` and `β`, for every function `f` from `α` to `β`, and for every value `b` of type `β` and computation `s` of type `α`, if `b` is in the computation obtained by mapping `f` over `s`, then there exists a value `a` in the computation `s` such that `f(a) = b`. In other words, if a value is in the result of a computation after applying a function to it, then that value must have come from applying the function to some value in the original computation.
More concisely: For all types `α` and `β`, and for every function `f` from `α` to `β` and computation `s` of type `α`, if `b ∈ map f s`, then there exists `a ∈ s` such that `f(a) = b`.
|
Computation.mem_bind
theorem Computation.mem_bind :
∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {a : α} {b : β},
a ∈ s → b ∈ f a → b ∈ s.bind f
The theorem `Computation.mem_bind` states that for any types `α` and `β`, a computation `s` of type `α`, a function `f` mapping from type `α` to a computation of type `β`, and any elements `a` of type `α` and `b` of type `β`, if `a` is an element of `s` and `b` is an element of `f(a)`, then `b` is also an element of the computation resulting from binding `s` with `f`. This theorem essentially describes the property of monadic bind operation in the context of computations.
More concisely: If `a` is an element of computation `s` and `b` is an element of `f(a)`, then `b` is an element of the computation obtained by binding `s` with `f`. In other words, `Computation.mem_bind` asserts the monadic law of binding for computations.
|
Computation.Results.length
theorem Computation.Results.length :
∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ} [_T : s.Terminates], s.Results a n → s.length = n
This theorem states that for any computation `s` of type `α` that terminates, if `s` produces a result `a` after exactly `n` steps (which is expressed by `Computation.Results s a n`), then the length of computation `s` (i.e., the number of steps it took to terminate) is exactly `n`. In other words, the 'length' of a terminating computation is defined by the number of steps it took to reach the final result.
More concisely: For any computation `s` of type `α` that terminates in `n` steps with result `a`, the length of `s` equals `n`.
|
Computation.Results.mem
theorem Computation.Results.mem : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.Results a n → a ∈ s
The theorem `Computation.Results.mem` states that for any type `α`, any computation `s` of type `α`, any element `a` of type `α`, and any natural number `n`, if the computation `s` terminates after `n` steps with the result `a` (denoted as `Computation.Results s a n`), then the element `a` is indeed an element in the computation `s` (denoted as `a ∈ s`). This means that if the computation terminates with a certain result, that result must come from the computation itself.
More concisely: For any type `α`, computation `s` of type `α`, element `a` of type `α`, and natural number `n`, if `Computation.Results s a n`, then `a ∈ s`.
|
Computation.destruct_eq_pure
theorem Computation.destruct_eq_pure :
∀ {α : Type u} {s : Computation α} {a : α}, s.destruct = Sum.inl a → s = Computation.pure a
The theorem `Computation.destruct_eq_pure` states that for any type `α`, computation `s` of type `α`, and element `a` of type `α`, if the destructor of `s` (`Computation.destruct s`) results in the left outcome (`Sum.inl a`) of a sum type, then the computation `s` is identical to the computation that immediately terminates with result `a` (i.e., `s` is equal to `Computation.pure a`). Essentially, if a computation can be destructed to a pure result `a`, then the computation must have been the computation yielding `a` in the first place.
More concisely: If `s` is a computation of type `α`, `a` is an element of type `α`, and `Computation.destruct s` equals `Sum.inl a`, then `s` equals `Computation.pure a`.
|
Computation.ret_mem
theorem Computation.ret_mem : ∀ {α : Type u} (a : α), a ∈ Computation.pure a
This theorem, `Computation.ret_mem`, states that for any type `α` and any element `a` of this type, `a` is an element of the computation that immediately terminates with result `a`. In other words, whenever a computation is defined to immediately terminate with a result `a`, `a` is guaranteed to be a part of that computation.
More concisely: For any type `α` and element `a` of `α`, the computation that immediately terminates with result `a` is an element of the computation that represents `a`.
|
Computation.think_mem
theorem Computation.think_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → a ∈ s.think
The theorem `Computation.think_mem` states that for any type `α`, any computation `s` of type `α`, and any element `a` of type `α`, if `a` is a member of `s`, then `a` is also a member of the computation obtained by delaying `s` for one "tick" (i.e., `Computation.think s`). In other words, if a computation produces a certain result, then delaying that computation will also produce the same result.
More concisely: For any computation `s` of type `α` and any element `a` of type `α` in `s`, `a` is also an element of `Computation.think s`.
|
Computation.map_pure'
theorem Computation.map_pure' :
∀ {α β : Type u_1} (f : α → β) (a : α), f <$> Computation.pure a = Computation.pure (f a)
The theorem `Computation.map_pure'` states that for any two types `α` and `β` and a function `f` from `α` to `β`, applying `f` to the result of the computation that immediately terminates with a result `a` (represented by `Computation.pure a`) is equivalent to the computation that immediately terminates with the result of applying `f` to `a` (represented by `Computation.pure (f a)`). In other words, it asserts that the `map` operation preserves the `pure` operation under function application in the context of computations.
More concisely: For all types `α` and `β` and functions `f` from `α` to `β`, `Computation.map_pure f (Computation.pure a) = Computation.pure (f a)`.
|
Computation.Results.len_unique
theorem Computation.Results.len_unique :
∀ {α : Type u} {s : Computation α} {a b : α} {m n : ℕ}, s.Results a m → s.Results b n → m = n
The theorem `Computation.Results.len_unique` asserts that for any computation `s` of a certain type `α`, and any two results `a` and `b` of the same type, if the computation `s` terminates with result `a` after `m` steps, and with result `b` after `n` steps, then `m` and `n` must be equal. This theorem essentially states that the number of steps required for a computation to terminate is unique.
More concisely: For any computation `s` of type `α`, if `s` terminates after `m` steps to result `a` and after `n` steps to result `b`, then `m = n`.
|
Computation.results_think
theorem Computation.results_think :
∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.Results a n → s.think.Results a (n + 1)
The theorem `Computation.results_think` states that for any type `α`, computation `s` of that type, element `a` of that type, and a natural number `n`, if the computation `s` terminates after exactly `n` steps with the result `a`, then the computation which is the result of delaying `s` for one "tick" (using the function `Computation.think`) terminates after exactly `n + 1` steps with the same result `a`.
More concisely: For any type `α`, computation `s` of type `Computation α`, element `a` of type `α`, and natural number `n`, if `s` terminates after exactly `n` steps to yield `a`, then `Computation.think (s)` terminates after exactly `n + 1` steps with result `a`.
|
Computation.get_mem
theorem Computation.get_mem : ∀ {α : Type u} (s : Computation α) [h : s.Terminates], s.get ∈ s
The theorem `Computation.get_mem` states that for any type `α` and any computation `s` of type `Computation α` that terminates (denoted by `Computation.Terminates s`), the result of the computation (obtained by `Computation.get s`) is a member of `s`. In other words, the computed value of any terminating computation is an element of the set defined by that computation.
More concisely: For any terminating computation `s : Computation α` in Lean 4, the result `Computation.get s` is an element of the set defined by `s` (i.e., `Computation.get s ∈ {x | Computation.apply s x}`).
|
Computation.of_think_mem
theorem Computation.of_think_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s.think → a ∈ s
The theorem `Computation.of_think_mem` states that for any type `α`, computation `s` of type `Computation α`, and a value `a` of type `α`, if `a` is a member of the computation `Computation.think s` (which is the computation `s` delayed for one "tick"), then `a` is also a member of the computation `s`. In other words, delaying the computation does not change its result.
More concisely: For any type `α`, computation `s` of type `Computation α`, and value `a` of type `α`, if `a ∈ Computation.think s`, then `a ∈ s`.
|
Computation.think_bind
theorem Computation.think_bind :
∀ {α : Type u} {β : Type v} (c : Computation α) (f : α → Computation β), c.think.bind f = (c.bind f).think := by
sorry
The theorem `Computation.think_bind` states that for all types `α` and `β`, and for any computation `c` of type `α` and any function `f` from `α` to a computation of type `β`, the result of binding the computation `Computation.think c` (which represents delaying the computation `c` by one "tick") with the function `f` is the same as delaying (by one "tick") the result of binding the original computation `c` with `f`. In essence, it captures the property that delaying a computation before applying a function via bind is the same as applying the function via bind and then delaying the result, demonstrating that the `think` operation is compatible with the bind operation in this computation model.
More concisely: For all types `α` and `β`, and computations `c` of type `α` and `f` from `α` to a computation of type `β`, `Computation.think (bind c f) = bind (Computation.think c) f`.
|
Computation.eq_of_bisim
theorem Computation.eq_of_bisim :
∀ {α : Type u} (R : Computation α → Computation α → Prop),
Computation.IsBisimulation R → ∀ {s₁ s₂ : Computation α}, R s₁ s₂ → s₁ = s₂
The theorem `Computation.eq_of_bisim` states that for any type `α` and any relation `R` on computations of type `α`, if `R` is a bisimulation -- meaning it relates two computations if and only if their "next steps" (as given by the `Computation.destruct` function) are also related by `R` -- then any two computations related by `R` are in fact equal. In other words, if two computations behave the same way (as witnessed by the bisimulation `R`), then they are the same computation.
More concisely: If `R` is a bisimulation relation on computations of type `α`, then for all `c₁` and `c₂` related by `R`, we have `c₁ = c₂`.
|
Computation.results_pure
theorem Computation.results_pure : ∀ {α : Type u} (a : α), (Computation.pure a).Results a 0
This theorem, `Computation.results_pure`, states that for any type 'α' and an instance 'a' of that type, the computation that immediately terminates with result 'a' (i.e., `Computation.pure a`) is characterized by the `Computation.Results` with zero steps. In other words, `Computation.pure a` will conclude after exactly 0 steps with the result 'a'.
More concisely: The `Computation.pure` function returns a computation that concludes in 0 steps with the given result.
|
Computation.exists_of_mem_bind
theorem Computation.exists_of_mem_bind :
∀ {α : Type u} {β : Type v} {s : Computation α} {f : α → Computation β} {b : β}, b ∈ s.bind f → ∃ a ∈ s, b ∈ f a
This theorem, `Computation.exists_of_mem_bind`, states that for any types `α` and `β`, a computation `s` of type `α`, a function `f` from `α` to a computation of type `β`, and an element `b` of type `β`, if `b` is an element of the computation that results from binding `s` with `f` (using the `Computation.bind` operation), then there exists an element `a` in the computation `s` such that `b` is an element of the computation `f(a)`. In other words, if `b` is produced by the combined computation, it must have been produced by applying `f` to some element of the original computation `s`.
More concisely: If `b` is an element of the computation `Computation.bind (s) f`, then there exists an element `a` in `s` such that `b` is an element of `f(a)`.
|
Computation.terminates_of_mem
theorem Computation.terminates_of_mem : ∀ {α : Type u} {s : Computation α} {a : α}, a ∈ s → s.Terminates
This theorem states that for any type `α`, any computation `s` of type `α`, and any element `a` of type `α`, if `a` belongs to `s` then the computation `s` terminates. In other words, if an element `a` is in the set of outcomes of the computation `s`, then the computation `s` is guaranteed to eventually reach a stopping point.
More concisely: For any type `α`, computation `s` of type `α`, and element `a` of type `α` in `s`, the computation `s` terminates.
|
Computation.terminates_def
theorem Computation.terminates_def : ∀ {α : Type u} (s : Computation α), s.Terminates ↔ ∃ n, (↑s n).isSome = true := by
sorry
The theorem `Computation.terminates_def` states that for any computation `s` of type `α`, `s` terminates if and only if there exists a natural number `n` such that the `n`th term of the computation is some value, i.e., it is not `none`. In other words, a computation is considered terminating if there is a point `n` after which the computation yields a definite value rather than none.
More concisely: A computation of type `α` terminates if and only if there exists a natural number `n` such that the `n`th step of the computation yields a value.
|
Computation.corec_eq
theorem Computation.corec_eq :
∀ {α : Type u} {β : Type v} (f : β → α ⊕ β) (b : β),
(Computation.corec f b).destruct = Computation.rmap (Computation.corec f) (f b)
The theorem `Computation.corec_eq` states that for all types `α` and `β`, and for any function `f` that maps from `β` to the sum type of `α ⊕ β` and an element `b` of type `β`, the result of destructing the computation formed by co-recursion on `f` and `b` is equal to the result of applying the right map (with the co-recursive computation as the mapping function) to the output of `f b`. In other words, destructing the computation created by co-recursion is equivalent to applying the right map to the original function's result.
More concisely: For all types `α` and `β`, and for any function `f : β → α ⊕ β`, the computation formed by co-recursion on `f` and an element `b` of type `β` is equal to the application of the right map to `f b`.
|
Computation.Terminates.term
theorem Computation.Terminates.term : ∀ {α : Type u} {s : Computation α} [self : s.Terminates], ∃ a, a ∈ s
This theorem asserts that for any computation `s` of type `α` that is guaranteed to terminate, there exists an element `a` of type `α` that this computation yields. In other words, if we have a computation that we know will eventually finish, this theorem confirms that there is some term `a` produced by this computation.
More concisely: For any terminating computation `s` in Lean 4, there exists an output `a` of type `α` that can be obtained from it.
|
Computation.thinkN_mem
theorem Computation.thinkN_mem : ∀ {α : Type u} {s : Computation α} {a : α} (n : ℕ), a ∈ s.thinkN n ↔ a ∈ s
The theorem `Computation.thinkN_mem` states that for any type `α`, any computation `s` of type `Computation α`, any element `a` of type `α`, and any natural number `n`, the element `a` is an element of the computation obtained by delaying `s` for `n` ticks using `Computation.thinkN` if and only if `a` is an element of `s`. In other words, delaying a computation does not change the set of elements that the computation can return.
More concisely: For any computation `s` of type `Computation α`, any element `a` of type `α`, and any natural number `n`, `Computation.thinkN a n s` returns `a` if and only if `s` returns `a`.
|
Computation.LiftRel.swap
theorem Computation.LiftRel.swap :
∀ {α : Type u} {β : Type v} (R : α → β → Prop) (ca : Computation α) (cb : Computation β),
Computation.LiftRel (Function.swap R) cb ca ↔ Computation.LiftRel R ca cb
The theorem `Computation.LiftRel.swap` states that for any types `α` and `β`, a relation `R` from `α` to `β`, and computations `ca` and `cb` of types `α` and `β` respectively, the property of `Computation.LiftRel` being true for the swapped relation `Function.swap R` and swapped computations `cb` and `ca` is equivalent to `Computation.LiftRel` being true for the original relation `R` and computations `ca` and `cb`. In other words, the termination relationship between two computations as defined by `Computation.LiftRel` remains the same even if we swap the relation and the computations.
More concisely: For any types `α` and `β`, relation `R` from `α` to `β`, and computations `ca` and `cb`, `Computation.LiftRel` holds for `R` and `ca` if and only if it holds for `Function.swap R` and `cb`.
|
Computation.eq_of_pure_mem
theorem Computation.eq_of_pure_mem : ∀ {α : Type u} {a a' : α}, a' ∈ Computation.pure a → a' = a
The theorem `Computation.eq_of_pure_mem` states that for any type `α` and any two elements `a` and `a'` of type `α`, if `a'` is in the computation that immediately terminates with result `a` (`Computation.pure a`), then `a'` must be equal to `a`. In other words, the only element that can be in the computation `Computation.pure a` is `a` itself.
More concisely: For any type `α` and elements `a, a'` of type `α`, if `Computation.pure a` contains `a'`, then `a = a'`.
|
Computation.mem_map
theorem Computation.mem_map :
∀ {α : Type u} {β : Type v} (f : α → β) {a : α} {s : Computation α}, a ∈ s → f a ∈ Computation.map f s
This theorem states that for any types `α` and `β`, a function `f` from `α` to `β`, a value `a` of type `α`, and a computation `s` of type `α`, if `a` is a result of the computation `s`, then `f(a)` is a result of the computation obtained by applying `f` to all results of `s` (i.e., `f(a)` is in the computation resulting from the mapping of `f` over `s`).
More concisely: For any functions `f` and computations `s` from type `α` to type `β`, and value `a` of type `α` being a result of `s`, `f(a)` is a result of the application of `f` to the results of `s`.
|
Computation.results_of_terminates
theorem Computation.results_of_terminates :
∀ {α : Type u} (s : Computation α) [_T : s.Terminates], s.Results s.get s.length
The theorem `Computation.results_of_terminates` states that for any computation `s` of type `α` that terminates, `s` returns a result after exactly its computed length number of steps. This result is exactly the one obtained using the `Computation.get` function. In other words, if you have a terminating computation, the result of that computation and the length of the computation (in terms of steps) are perfectly characterized by the `Computation.Results` predicate.
More concisely: For any terminating computation `s` of type `α` in Lean, the result `Computation.get s` is equal to the value obtained after exactly `Computation.length s` steps.
|
Mathlib.Data.Seq.Computation._auxLemma.5
theorem Mathlib.Data.Seq.Computation._auxLemma.5 :
∀ {α : Type u} {β : Type v} (R : α → β → Prop) (a : α) (b : β),
Computation.LiftRel R (Computation.pure a) (Computation.pure b) = R a b
This theorem states that for any types `α` and `β` and a relation `R` between them, and for any elements `a` of type `α` and `b` of type `β`, the `Computation.LiftRel` of the relation `R` and the computations which immediately terminate with `a` and `b` respectively, is equivalent to the relation `R` holding between `a` and `b`. In other words, it says that lifting the relation `R` through the computations that yield `a` and `b` simply boils down to checking the relation `R` on `a` and `b` directly.
More concisely: For any types `α`, `β` and relation `R` between them, the computational lifting of `R` on elements `a : α` and `b : β` is equivalent to `R(a)` holding.
|
Computation.of_results_think
theorem Computation.of_results_think :
∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.think.Results a n → ∃ m, s.Results a m ∧ n = m + 1
The theorem `Computation.of_results_think` states that for any type `α`, any computation `s` of type `α`, any element `a` of type `α`, and any natural number `n`, if `s` returns `a` after exactly `n` steps when it is delayed for one "tick" (`Computation.Results (Computation.think s) a n`), then there exists a natural number `m` such that `s` returns `a` after exactly `m` steps without delay (`Computation.Results s a m`) and `n` is equal to `m + 1`. In other words, adding a delay "tick" to a computation increases the number of steps required to reach a result by exactly one.
More concisely: For any computation `s` and natural numbers `n` and `m`, if `s` returns `a` after `n` delayed steps and `m` non-delayed steps, then `n = m + 1`.
|
Computation.ret_bind
theorem Computation.ret_bind :
∀ {α : Type u} {β : Type v} (a : α) (f : α → Computation β), (Computation.pure a).bind f = f a
The theorem `Computation.ret_bind` states that for all types `α` and `β`, and for any element `a` of type `α` and any function `f` from `α` to `Computation β`, binding the computation that immediately terminates with result `a` (i.e., `Computation.pure a`) with the function `f` is equal to applying `f` directly to `a`. This is an important property of the bind operation in the context of computations, reflecting that binding with a "pure" or immediately terminating computation doesn't change the effect of the function applied.
More concisely: For all types `α` and `β`, and for any `a : α` and `f : α → Computation β`, `Computation.pure a >>= f = f a`.
|
Computation.bind_pure
theorem Computation.bind_pure :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α), s.bind (Computation.pure ∘ f) = Computation.map f s
The theorem `Computation.bind_pure` states that for any types `α` and `β`, and any function `f : α → β`, and any computation `s` of type `α`, binding the computation `s` with the function `f` composed with `pure` is equivalent to mapping the function `f` over the computation `s`. In other words, it means that the operation of transforming the result of a computation by applying a function (using `map`) can also be achieved by first applying the function to the result and then making a new computation that immediately terminates with that result (using `bind` with `pure ∘ f`).
More concisely: For any type `α`, type `β`, function `f : α → β`, and computation `s : α`, `map f (pure s) = bind s (λ x => pure (f x))`.
|
Computation.map_think
theorem Computation.map_think :
∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α),
Computation.map f s.think = (Computation.map f s).think
The theorem `Computation.map_think` states that for any type `α` and `β`, and a function `f` from `α` to `β`, and a computation `s` of type `α`, the computation that first delays the execution of `s` for one tick and then applies the function `f` on the result (represented by `Computation.map f (Computation.think s)`) is the same as the computation that first applies the function `f` on the computation `s` and then delays the execution of the result for one tick (represented by `Computation.think (Computation.map f s)`). This theorem establishes the distributivity of the `map` and `think` operations on computations.
More concisely: For any type `α` and function `f` from `α` to `β`, and computation `s` of type `α`, `Computation.map f (Computation.think s)` is equal to `Computation.think (Computation.map f s)`.
|
Computation.get_eq_of_mem
theorem Computation.get_eq_of_mem : ∀ {α : Type u} (s : Computation α) [h : s.Terminates] {a : α}, a ∈ s → s.get = a
The theorem `Computation.get_eq_of_mem` states that for any type `α`, given a terminating computation `s` of type `α`, and an element `a` of type `α`, if `a` is an element of the computation `s`, then the result of the computation `s` (obtained using `Computation.get`) is equal to `a`. This means that, if a computation produces a certain result, and that result is an element of the computation, then when we get the result of the computation, it's guaranteed to be that element.
More concisely: If `s` is a terminating computation of type `α` and `a` is an element of `s`, then `Computation.get s = a`.
|