Computable.of_eq
theorem Computable.of_eq :
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α → σ},
Computable f → (∀ (n : α), f n = g n) → Computable g
The theorem `Computable.of_eq` states that for any two functions `f` and `g` from a type `α` to a type `σ`, where `α` and `σ` are primcodable (meaning, they can be encoded as natural numbers), if `f` is computable and `f` and `g` are equal for every `α`, then `g` is also computable. This theorem therefore shows that computability is preserved under function equality.
More concisely: If `f` and `g` are equal computable functions from a primcodable type `α` to a type `σ`, then `g` is computable.
|
Computable.option_some
theorem Computable.option_some : ∀ {α : Type u_1} [inst : Primcodable α], Computable some
This theorem states that for any type `α` that has an instance of `Primcodable`, the function `some` (which wraps a value in an option) is computable. In other words, if we can encode and decode values of type `α`, then we can also effectively compute the function that takes a value of `α` and produces its 'option' version.
More concisely: If `α` has an instance of `Primcodable`, then the `some` function from `α` to `option α` is computable.
|
Primrec₂.to_comp
theorem Primrec₂.to_comp :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α → β → σ}, Primrec₂ f → Computable₂ f
The theorem `Primrec₂.to_comp` states that for all types `α`, `β`, and `σ` that are primcodable (i.e., have a primitive recursive coding), and for any function `f` that takes arguments of type `α` and `β` and returns a value of type `σ`, if `f` is a binary primitive recursive function (as defined by `Primrec₂`), then `f` is also a computable function (as defined by `Computable₂`). Essentially, this theorem establishes a connection between the concepts of primitive recursiveness and computability for binary functions, asserting that primitive recursiveness implies computability.
More concisely: If `α`, `β`, and `σ` are primcodable types and `f : α → β → σ` is a binary primitive recursive function, then `f` is computable.
|
Computable.const
theorem Computable.const :
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] (s : σ), Computable fun x => s := by
sorry
The theorem named `Computable.const` states that for any types `α` and `σ` that have a `Primcodable` instance (indicating that elements of these types can be encoded as natural numbers), and for any specific value `s` of type `σ`, the function that maps every element of type `α` to the constant value `s` is `Computable`. In other words, constant functions are computable.
More concisely: For types `α` and `σ` with `Primcodable` instances, and a fixed `σ` value `s`, the function mapping `α` elements to the constant `s` is computable.
|
Computable.to₂
theorem Computable.to₂ :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α × β → σ}, Computable f → Computable₂ fun a b => f (a, b)
The theorem `Computable.to₂` states that for any three types `α`, `β`, and `σ` which have instances of `Primcodable`, and a function `f` from the product of `α` and `β` to `σ`, if this function `f` is computable (as defined by the `Computable` property), then the function `f` is also computable when viewed as a two-argument function (as defined by the `Computable₂` property). This essentially means that computable functions remain computable even when their arguments are rearranged.
More concisely: If `f` is a computable function from the product of types `α` and `β` to `σ`, where `α`, `β`, and `σ` have `Primcodable` instances, then `f` is also computable as a two-argument function.
|
Computable.ofOption
theorem Computable.ofOption :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → Option β},
Computable f → Partrec fun a => ↑(f a)
The theorem `Computable.ofOption` states that for any two types `α` and `β` that are Primcodable (that is, they can be encoded as and decoded from natural numbers), given a function `f` from `α` to `Option β`, if `f` is computable, then the function that maps each element `a` in `α` to the part of `f a` is partial recursive. In other words, if you can compute `f` on any input, then you can also compute the partial function that converts `f(a)` to a part, verifying that `f(a)` is defined, for any `a` in `α`.
More concisely: If `f : α → Option β` is a computable function between Primcodable types `α` and `β`, then the function that extracts the part of `f` is partial recursive.
|
Vector.mOfFn_part_some
theorem Vector.mOfFn_part_some :
∀ {α : Type u_1} {n : ℕ} (f : Fin n → α), (Vector.mOfFn fun i => Part.some (f i)) = Part.some (Vector.ofFn f) := by
sorry
The theorem `Vector.mOfFn_part_some` states that for any type `α` and natural number `n`, given a function `f` that maps `Fin n` (a finite set of size `n`) to `α`, the monadic function operation `Vector.mOfFn` applied on `Part.some` of the function `f` (which transforms the function value into a `Part` type with domain `True`) is equal to `Part.some` of the `Vector.ofFn` applied on `f`. In simpler terms, this theorem describes how the operation of creating a vector from a function and then wrapping it with the `Part.some` function is equivalent to first wrapping each function value with `Part.some` and then creating a vector from these values.
More concisely: Given a function `f` from `Fin n` to type `α`, `Vector.mOfFn (Part.some f) = Part.some (Vector.ofFn f)`.
|
Partrec.nat_iff
theorem Partrec.nat_iff : ∀ {f : ℕ →. ℕ}, Partrec f ↔ Nat.Partrec f
The theorem `Partrec.nat_iff` states that for any function `f` from natural numbers to partial natural numbers (i.e., the function may not necessarily return a value for all input natural numbers), `f` is partial recursive (`Partrec`) if and only if `f` is partial recursive according to the natural numbers definition (`Nat.Partrec`). In other words, the function `f` is partial recursive in the context of the general definition of partial recursive functions if it is also partial recursive when considered specifically over the domain of natural numbers.
More concisely: The theorem `Partrec.nat_iff` asserts that a function from natural numbers to partial natural numbers is partial recursive according to the general definition if and only if it is partial recursive when considered over the domain of natural numbers according to the specific definition.
|
Computable₂.comp
theorem Computable₂.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : β → γ → σ} {g : α → β} {h : α → γ},
Computable₂ f → Computable g → Computable h → Computable fun a => f (g a) (h a)
The theorem `Computable₂.comp` states that, given types `α`, `β`, `γ`, and `σ` that have a `Primcodable` instance, and given functions `f` from `β` and `γ` to `σ`, `g` from `α` to `β`, and `h` from `α` to `γ`, if `f` is a computable function of two variables, and `g` and `h` are computable functions of one variable, then the function that takes an input `a` of type `α` and returns the result of applying `f` to `g(a)` and `h(a)` is also a computable function. This theorem essentially asserts the closure of computable functions under composition.
More concisely: If `f: β → σ`, `g: α → β`, and `h: α → γ` are computable functions, and `f` is computable in two variables, then the function `x ↦ f (g x) (h x)` is computable.
|
Nat.Partrec.of_primrec
theorem Nat.Partrec.of_primrec : ∀ {f : ℕ → ℕ}, Nat.Primrec f → Nat.Partrec ↑f
This theorem states that for any function `f` from natural numbers to natural numbers, if `f` is primitive recursive (denoted as `Nat.Primrec f`), then `f` is partially recursive (denoted as `Nat.Partrec ↑f`). In other words, the set of primitive recursive functions is a subset of the set of partial recursive functions.
More concisely: Every primitive recursive function is partially recursive.
|
Computable.id
theorem Computable.id : ∀ {α : Type u_1} [inst : Primcodable α], Computable id
The theorem `Computable.id` states that, for any type `α` that can be encoded as a primitive (as specified by the typeclass `Primcodable α`), the identity function (`id`) on that type is computable. In other words, it asserts that the identity function on any primitively codable type is partially recursive, where partial recursive functions are a generalization of the familiar recursive functions and can express all computable functions.
More concisely: The identity function on types encodable as primitives is computable, i.e., partially recursive.
|
Partrec.comp
theorem Partrec.comp :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : β →. σ} {g : α → β}, Partrec f → Computable g → Partrec fun a => f (g a)
The theorem `Partrec.comp` states that for any three types `α`, `β`, and `σ` which are all Primcodable, if we have a partially recursive function `f` from `β` to `σ` and a computable function `g` from `α` to `β`, then the composition of `f` and `g`, i.e., the function that applies `g` to an input from `α` and then applies `f` to the result, is itself partially recursive. This is essentially a statement about the closure of the class of partially recursive functions under function composition with a computable function.
More concisely: If `f` is a partially recursive function from `β` to `σ` and `g` is a computable function from `α` to `β`, then the function `COMP(g, f)` defined as `COMP(g, f) (x) = f (g (x))` is also partially recursive.
|
Computable.encode_iff
theorem Computable.encode_iff :
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
(Computable fun a => Encodable.encode (f a)) ↔ Computable f
This theorem states that for any types `α` and `σ`, and any function `f` from `α` to `σ`, if `α` and `σ` are both primcodable (i.e., they can be effectively encoded as natural numbers), then the function `f` is computable if and only if the function that applies `f` to an argument `a` and then encodes the result using `Encodable.encode` is also computable. In simpler terms, encoding the output of a computable function does not affect its computability.
More concisely: For functions between primcodable types in Lean 4, computability is preserved under encoding: a computable function `f : α → σ` is computable if and only if the composed function ` Encodable.encode ∘ f` is computable.
|
Partrec.bind
theorem Partrec.bind :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α →. β} {g : α → β →. σ},
Partrec f → Partrec₂ g → Partrec fun a => (f a).bind (g a)
The theorem `Partrec.bind` states that for all types `α`, `β`, and `σ` that have instances of `Primcodable`, and for all partial functions `f` from `α` to `β` and `g` from `α` and `β` to `σ`, if `f` is a partial recursive function (`Partrec`) and `g` is a two argument partial recursive function (`Partrec₂`), then the function which, for each `a`, binds the result of `f(a)` to `g(a)` using the `Part.bind` operation, is also a partial recursive function. This means that the composition of two partial recursive functions via the bind operation retains the property of being partial recursive.
More concisely: If `f` is a partial recursive function from `α` to `β` and `g` is a two-argument partial recursive function from `α × β` to `σ`, then the function `x ↔→ y. g (f x)` is partial recursive. (Here, `↔→` denotes the bind operation in Lean.)
|
Computable₂.partrec₂
theorem Computable₂.partrec₂ :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α → β → σ}, Computable₂ f → Partrec₂ fun a => ↑(f a)
The theorem `Computable₂.partrec₂` states that for any two types `α` and `β`, and result type `σ`, all of which have instances of `Primcodable`, if a function `f` from `α` and `β` to `σ` is computable (as defined by the `Computable₂` definition), then a function that applies `f` to a pair of inputs and lifts the result to an optional value (using the `Partrec₂` definition) is partially recursive. In other words, the computability of a two-argument function implies the partial recursiveness of the corresponding function that maps inputs to optional outputs.
More concisely: If `f : α × β -> σ` is a computable function between types `α`, `β`, and `σ` with `Primcodable` instances, then the function `x y => some (f x y)` is partially recursive.
|
Computable.sum_casesOn
theorem Computable.sum_casesOn :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ},
Computable f → Computable₂ g → Computable₂ h → Computable fun a => Sum.casesOn (f a) (g a) (h a)
The theorem `Computable.sum_casesOn` states that for any three types α, β, γ, and σ, where α, β, γ, and σ are primcodable, and given three functions `f : α → β ⊕ γ`, `g : α → β → σ`, and `h : α → γ → σ`, if `f` is computable and both `g` and `h` are computable with two arguments (computable₂), then the function that takes a value of type α and applies `f` to it to produce a value of type β or γ (β ⊕ γ), then depending on the result applies either `g` or `h` to that pair (the original α and the result β or γ), is also computable. In other words, we can always computably decide which of two computable functions to apply based on the result of another computable function.
More concisely: If `f : α → β ⊕ γ` is computable, `g : α → β → σ` and `h : α → γ → σ` are computable with two arguments, then the function that applies `g` or `h` based on the result of `f` is also computable.
|
Computable.decode
theorem Computable.decode : ∀ {α : Type u_1} [inst : Primcodable α], Computable Encodable.decode
This theorem states that for any type `α` that has a `Primcodable` instance (which means, intuitively, that values of type `α` can be encoded as natural numbers), the function `Encodable.decode` is computable. The `Encodable.decode` function is a decoding function that takes a natural number and returns an optional `α`, i.e., it may fail to return an `α`. In the theorem, `Computable` is a predicate over functions that, roughly speaking, says that there exists an algorithm that computes the function. Therefore, the theorem states that there exists an algorithm that computes the `Encodable.decode` function for any primcodable type.
More concisely: For any type `α` with a `Primcodable` instance, the decoding function `Encodable.decode` from natural numbers to optional `α` values is computable.
|
Computable.snd
theorem Computable.snd :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Computable Prod.snd
The theorem `Computable.snd` asserts that for any two types `α` and `β` which are Primcodable (i.e., they have an instance of the Primcodable type class), the second projection function `Prod.snd` is computable. In other words, given any pair of elements of types `α` and `β`, the function that returns the second element of the pair is always computable.
More concisely: For any two Primcodable types `α` and `β`, the second projection function `Prod.snd` on their product type is a computable function.
|
Partrec.of_eq
theorem Partrec.of_eq :
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α →. σ},
Partrec f → (∀ (n : α), f n = g n) → Partrec g
The theorem `Partrec.of_eq` states that for any two partial functions `f` and `g` from a type `α` to another type `σ` (both of which are encoded by a primitive recursive function), if `f` is partial recursive and `f` equals `g` for all values in `α`, then `g` is also partial recursive. In other words, the partial recursive property is preserved under pointwise equality between two functions.
More concisely: If two partial functions from type α to σ, encoded by primitive recursive functions, are equal at all values in α where they are defined, then the second function is also partial recursive.
|
Nat.Partrec.of_eq
theorem Nat.Partrec.of_eq : ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → (∀ (n : ℕ), f n = g n) → Nat.Partrec g
This theorem states that for any two functions `f` and `g` from natural numbers to partitional natural numbers, if `f` is partial recursive (denoted by `Nat.Partrec f`) and `g` equals `f` for all natural numbers `n` (expressed as `(∀ (n : ℕ), f n = g n)`), then `g` is also partial recursive (expressed as `Nat.Partrec g`). In other words, if `f` is a partial recursive function and `g` is identical to `f` for every natural number, then `g` is also a partial recursive function.
More concisely: If `f` is a partial recursive function and `f(n) = g(n)` for all natural numbers `n`, then `g` is also partial recursive.
|
Computable.pair
theorem Computable.pair :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {f : α → β} {g : α → γ}, Computable f → Computable g → Computable fun a => (f a, g a)
The theorem `Computable.pair` states that for any three types α, β, and γ, where α, β, and γ are Primcodable, and for any two functions `f` from α to β and `g` from α to γ, if `f` and `g` are Computable, then the function that takes an input of type α and produces a pair consisting of the result of applying `f` and `g` to that input is also Computable. In other words, if we have computable functions `f : α → β` and `g : α → γ`, then the function `h : α → β × γ` defined by `h(a) = (f(a), g(a))` is also computable.
More concisely: If `f : α -> β` and `g : α -> γ` are Computable functions with Primcodable types α, β, and γ, then the function `h : α -> β x γ` defined by `h(x) = (f x, g x)` is also Computable.
|
Partrec.map
theorem Partrec.map :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α →. β} {g : α → β → σ},
Partrec f → Computable₂ g → Partrec fun a => Part.map (g a) (f a)
The theorem `Partrec.map` states that for all types `α`, `β`, and `σ`, which have instances of `Primcodable` (i.e., they can be encoded as natural numbers), and for all functions `f` from `α` to `β` and `g` from `α` and `β` to `σ`, if `f` is partial recursive (`Partrec`) and `g` is computable with two inputs (`Computable₂`), then the function which takes an `α`, applies `f` to it, and then maps `g` over the result, is also partial recursive (`Partrec`). Essentially, this theorem tells us about the preservation of the property of being partial recursive under the mapping operation with a computable function.
More concisely: If `f` is partial recursive and `g` is computable with two inputs, then the function `x mapsto g(x, f x)` is partial recursive.
|
Partrec.to₂
theorem Partrec.to₂ :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α × β →. σ}, Partrec f → Partrec₂ fun a b => f (a, b)
The theorem `Partrec.to₂` states that for any types `α`, `β`, and `σ` that are Primcodable (i.e., they can be encoded as natural numbers), if a function `f` from a pair of type `α` and `β` to a partial function on `σ` is partially recursive (defined by `Partrec`), then this function `f` can be treated as a function of two variables (defined by `Partrec₂`). This essentially means that the partial recursion property is preserved when we treat a function of a pair as a function of two variables.
More concisely: If `f` is a partially recursive function from `α × β` to the partial functions on `σ`, where `α`, `β`, and `σ` are Primcodable types, then `f` is equivalent to a function `g` of two variables, defined by `Partrec₂`, such that the application of `g` to arguments `(a, b)` is equal to the application of `f` to the pair `(a, b)`.
|
Partrec₂.comp
theorem Partrec₂.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] [inst_3 : Primcodable σ] {f : β → γ →. σ} {g : α → β} {h : α → γ},
Partrec₂ f → Computable g → Computable h → Partrec fun a => f (g a) (h a)
The theorem `Partrec₂.comp` states that for all types `α`, `β`, `γ`, and `σ` that are `Primcodable`, if we have three functions `f` (from `β` and `γ` to an option type `σ`, i.e., `f` may not return a value for some inputs), `g` (from `α` to `β`), and `h` (from `α` to `γ`), then if `f` is partially recursive (in two variables) and both `g` and `h` are computable, then the function that takes `a` of type `α` and applies `f` to `g(a)` and `h(a)` is also partially recursive.
Essentially, this theorem expresses a property of composition of functions in the context of computability theory - given computable and partially recursive functions, we can construct a new function that is also partially recursive by applying these functions in a certain way.
More concisely: If `f` is a partially recursive function from `β` to `option σ` and `g : α → β` and `h : α → γ` are computable functions, then the function `x ↦ some (f (g x)) (h x)` is also partially recursive from `α` to `option σ`.
|
Nat.Partrec.ppred
theorem Nat.Partrec.ppred : Nat.Partrec fun n => ↑n.ppred
This theorem states that the partial predecessor operation is partially recursive. In other words, the function that takes a natural number `n` and returns the predecessor of `n` if `n` is not zero, and returns nothing (`none`) if `n` is zero, is computable according to the definition of partial recursive functions in the natural numbers.
More concisely: The predicate `∂` defining the partial predecessor operation on natural numbers is partial recursive.
|
Computable.comp
theorem Computable.comp :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : β → σ} {g : α → β}, Computable f → Computable g → Computable fun a => f (g a)
The theorem `Computable.comp` states that for any three types `α`, `β`, and `σ`, given that they are `Primcodable` (which means there exists a primitive recursive encoding of these types), if a function `f` from `β` to `σ` is computable and a function `g` from `α` to `β` is also computable, then the composition of these two functions, represented as `f(g(a))`, is also computable. This composition means applying function `g` to `a` first, and then applying function `f` to the result. This theorem embodies the property of closure under composition for computable functions.
More concisely: If `f` is a computable function from `β` to `σ` and `g` is a computable function from `α` to `β`, then the composition `f ∘ g` from `α` to `σ` is also computable.
|
Computable.encode
theorem Computable.encode : ∀ {α : Type u_1} [inst : Primcodable α], Computable Encodable.encode
The theorem `Computable.encode` states that for any type `α` which has a primary codable instance `inst`, the function `Encodable.encode` is computable. Here, `Encodable.encode` is a function that takes an instance of a type `α` and converts it into a natural number (`ℕ`). Essentially, this theorem is about the computability of the encoding process from a general type to natural numbers when the type is primary codable.
More concisely: For any type `α` with a primary codable instance `inst`, the encoding function `Encodable.encode` is a computable function.
|
Computable.fst
theorem Computable.fst :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Computable Prod.fst
The theorem `Computable.fst` states that for any two types `α` and `β`, if these types are Primcodable (meaning there exists a primitive recursive encoding for elements of these types), then the function `Prod.fst` is computable. `Prod.fst` is a function that takes a pair of type `α × β` and returns its first element of type `α`. So, in essence, this theorem asserts that the process of extracting the first element from a pair is a computable operation when the types of the elements in the pair are Primcodable.
More concisely: If types `α` and `β` are Primcodable, then the function `Prod.fst` that extracts the first element from a pair of type `α × β` is a computable function.
|
Primrec.to_comp
theorem Primrec.to_comp :
∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
Primrec f → Computable f
The theorem `Primrec.to_comp` states that for any two types `α` and `σ` that are primcodable, and any function `f` from `α` to `σ`, if `f` is primitively recursive (as defined by `Primrec`), then `f` is also computable (as defined by `Computable`). In other words, this theorem states that primitive recursiveness of a function implies its computability.
More concisely: If `f` is a primitively recursive function between types `α` and `σ` that are primcodable, then `f` is computable.
|