Primrec.option_some
theorem Primrec.option_some : ∀ {α : Type u_1} [inst : Primcodable α], Primrec some
The theorem `Primrec.option_some` states that for any type `α` that is Primcodable, the function `some`, which wraps a given value in an Option, is primitive recursive. In other words, the function `some` can be computed by a sequence of basic operations, loops, and conditionals, when both its input (of type `α`) and output (of type `Option α`) are encoded as natural numbers.
More concisely: The function `some : α → Option α` is primitive recursive for any type `α` that is Primcodable.
|
Primrec.of_eq
theorem Primrec.of_eq :
∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f g : α → σ},
Primrec f → (∀ (n : α), f n = g n) → Primrec g
The theorem `Primrec.of_eq` states that for any two functions `f` and `g` from a type `α` to a type `σ` (both of these types being primcodable), if `f` is primitive recursive and `g` equals `f` for every natural number `n` in the domain `α`, then `g` is also primitive recursive. This theorem allows one to reason about the preservation of the primitive recursive property under the condition of pointwise equality.
More concisely: If `f` is a primitive recursive function from type `α` to `σ`, and `f` equals `g` for all natural numbers `n` in the domain `α` of `f`, then `g` is also a primitive recursive function.
|
Nat.Primrec.of_eq
theorem Nat.Primrec.of_eq : ∀ {f g : ℕ → ℕ}, Nat.Primrec f → (∀ (n : ℕ), f n = g n) → Nat.Primrec g
This theorem states that if two functions `f` and `g`, both from natural numbers to natural numbers, are equal for every natural number (i.e., `f n = g n` for all `n`), and if `f` is a primitive recursive function, then `g` is also a primitive recursive function. Essentially, if `f` is proven to be a primitive recursive function, any function equal to `f` across all natural numbers will also be a primitive recursive function.
More concisely: If a primitive recursive function `f` is equal to function `g` for all natural numbers, then `g` is also a primitive recursive function.
|
Primrec.list_cons
theorem Primrec.list_cons : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ List.cons
The theorem `Primrec.list_cons` states that for any type `α` which is primcodable (denoted by `[inst : Primcodable α]`), the function `List.cons` is a binary primitive recursive function. `List.cons` is a function that takes two arguments: an element of type `α` and a list of elements of type `α`, and returns a new list formed by adding the given element to the head of the given list. The theorem asserts that this operation is primitive recursive, which means it can be computed using a limited set of basic operations and recursion.
More concisely: For any type `α` that is primcodable, the function `List.cons : α → List α → List α` is a primitive recursive function.
|
Primrec.ofNat
theorem Primrec.ofNat : ∀ (α : Type u_4) [inst : Denumerable α], Primrec (Denumerable.ofNat α)
The theorem `Primrec.ofNat` states that for all types `α` that are denumerable (meaning there is a one-to-one correspondence between `α` and the set of natural numbers), the function `Denumerable.ofNat α` is primitive recursive. In other words, given any type that can be paired off with the natural numbers, the function that returns the `n`-th element of `α` indexed by decoding is always a primitive recursive function which can be computed using a basic set of operations and recursion on the natural numbers.
More concisely: For any denumerable type `α`, the function `Denumerable.ofNat α` encoding its elements as natural numbers is primitive recursive.
|
Nat.Primrec.casesOn1
theorem Nat.Primrec.casesOn1 : ∀ {f : ℕ → ℕ} (m : ℕ), Nat.Primrec f → Nat.Primrec fun x => Nat.casesOn x m f
The theorem `Nat.Primrec.casesOn1` states that for any function `f` from natural numbers to natural numbers and any natural number `m`, if `f` is primitive recursive, then the function that applies `Nat.casesOn` to its argument `x` with the parameters `m` and `f` is also primitive recursive. In other words, given a primitive recursive function `f` and a natural number `m`, the function that returns `m` if its input is zero and applies `f` if its input is a successor is also primitive recursive.
More concisely: If `f` is a primitive recursive function, then the function `x => if hx = 0 then m else f (succ x)` is also primitive recursive, for any natural numbers `m` and `x`. (Here, `h` denotes the predicate `Nat.pred_eq_zero` and `succ` denotes the successor function.)
|
Primrec₂.natPair
theorem Primrec₂.natPair : Primrec₂ Nat.pair
This theorem states that the natural number pairing function `Nat.pair` is a binary primitive recursive function. In other words, given two natural numbers as inputs, the function combines them into a single number in such a way that original numbers can be recovered from it, and this process is achieved through a sequence of basic arithmetic operations, which shows the primality of the function. The representation of this function in Lean, as `Primrec₂ Nat.pair`, underlines the computability aspect of it.
More concisely: The natural number pairing function `Nat.pair` is a primitive recursive function.
|
Primrec.ofNat_iff
theorem Primrec.ofNat_iff :
∀ {α : Type u_4} {β : Type u_5} [inst : Denumerable α] [inst_1 : Primcodable β] {f : α → β},
Primrec f ↔ Primrec fun n => f (Denumerable.ofNat α n)
The theorem `Primrec.ofNat_iff` asserts that for any types `α` and `β`, given instances of `Denumerable α` and `Primcodable β`, and a function `f` from `α` to `β`, the function `f` is primitive recursive if and only if the function that maps each natural number `n` to `f` applied to the `n`-th element of `α` is also primitive recursive. In essence, it is stating a correspondence between the primitiveness of a function `f` and the primitiveness of the function obtained by applying `f` after enumerating the input type.
More concisely: For any types α and β, if α is denumerable, β is primcodable, and the function f from α to β is primitive recursive, then the function that maps each natural number n to f applied to the n-th element of α is also primitive recursive. Conversely, if the composed function is primitive recursive, then so is f.
|
Nat.Primrec'.sqrt
theorem Nat.Primrec'.sqrt : Nat.Primrec' fun v => v.head.sqrt
This theorem states that the square root function, when applied to the first element of a vector, is primitive recursive. In other words, it asserts that the computation of the integer square root of the first element of a given vector can be described by a series of simple, repeatable steps, which is the essence of primitive recursion.
More concisely: The function that computes the integer square root of the first element of a vector is primitive recursive.
|
Nat.Primrec'.prec'
theorem Nat.Primrec'.prec' :
∀ {n : ℕ} {f g : Vector ℕ n → ℕ} {h : Vector ℕ (n + 2) → ℕ},
Nat.Primrec' f →
Nat.Primrec' g → Nat.Primrec' h → Nat.Primrec' fun v => Nat.rec (g v) (fun y IH => h (y ::ᵥ IH ::ᵥ v)) (f v)
The theorem `Nat.Primrec'.prec'` states that for any natural number `n`, and for any functions `f`, `g`, `h` where `f` and `g` map a vector of length `n` to a natural number and `h` maps a vector of length `n + 2` to a natural number, if `f`, `g`, and `h` are primitive recursive (denoted by `Nat.Primrec'`), then the function defined by natural number recursion on `f v` with `g v` as the base case and `h` applied to the constructed vector as the recursive step is also primitive recursive.
More concisely: If `f` and `g` are primitive recursive functions mapping vectors of length `n` to natural numbers, and `h` is a primitive recursive function mapping vectors of length `n + 2` to natural numbers, then the function defined by natural number recursion on `f` with `g` as the base case and `h` as the recursive step is also primitive recursive.
|
Primrec₂.of_eq
theorem Primrec₂.of_eq :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f g : α → β → σ}, Primrec₂ f → (∀ (a : α) (b : β), f a b = g a b) → Primrec₂ g
The theorem `Primrec₂.of_eq` states that for any three types `α`, `β`, and `σ` where `α`, `β`, and `σ` are primitive recursive (i.e., we have instances of `Primcodable α`, `Primcodable β`, and `Primcodable σ`), if `f` and `g` are binary functions from `α` and `β` to `σ` such that `f` is primitive recursive (`Primrec₂ f`), and `g` is equal to `f` for all inputs `a` and `b` (from `α` and `β` respectively), then `g` is also primitive recursive (`Primrec₂ g`). In other words, if two binary functions are equal and one of them is primitive recursive, then the other one is also primitive recursive.
More concisely: If two binary functions `f` and `g` from primitive recursive types to a primitive recursive type are equal, then both `f` and `g` are primitive recursive.
|
Primrec.of_equiv_symm
theorem Primrec.of_equiv_symm : ∀ {α : Type u_1} [inst : Primcodable α] {β : Type u_4} {e : β ≃ α}, Primrec ⇑e.symm
The theorem `Primrec.of_equiv_symm` states that for any types `α` and `β`, given that `α` is Primcodable and there exists an equivalence `e` between `β` and `α`, the inverse function of `e` (denoted as `e.symm`) is primitive recursive. Here, a function is called primitive recursive if it can be represented in a certain restricted language that only includes basic arithmetic operations and recursions.
More concisely: If `α` is Primcodable and there exists an equivalence `e` between `α` and `β`, then `e.symm` is a primitive recursive function.
|
Primrec.list_append
theorem Primrec.list_append : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun x x_1 => x ++ x_1
The theorem `Primrec.list_append` states that for any given type `α` which is primcodable, the function that appends two lists, namely `x` and `x_1`, is a binary primitive recursive function. In simpler terms, it means that list concatenation operation is primitive recursive for any kind of elements as long as the type of those elements is primcodable.
More concisely: For any primcodable type α, the function that appends two lists of type list α is a primitive recursive function.
|
Primrec.vector_ofFn
theorem Primrec.vector_ofFn :
∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ},
(∀ (i : Fin n), Primrec (f i)) → Primrec fun a => Vector.ofFn fun i => f i a
The theorem `Primrec.vector_ofFn` states that for any types `α` and `σ` that have a primitive encoding (denoted by `Primcodable α` and `Primcodable σ`), for any natural number `n`, and for any function `f` that takes a finite ordinal (an element of `Fin n`) and an element of type `α` and returns an element of type `σ`, if each function `f i` (for each finite ordinal `i`) is primitive recursive, then the function that takes an element of type `α` and returns a vector of length `n` (each element of the vector is the result of applying `f i` to the element of `α`) is also primitive recursive.
More concisely: If `α` and `σ` are types with primitive encodings, `n` is a natural number, and `f` is a primitive recursive function that takes a finite ordinal and an element of `α` to produce an element of `σ`, then the function that maps an element of `α` to the vector of length `n` where the `i`-th component is `f (i x)` is also primitive recursive.
|
Primrec.dom_denumerable
theorem Primrec.dom_denumerable :
∀ {α : Type u_4} {β : Type u_5} [inst : Denumerable α] [inst_1 : Primcodable β] {f : α → β},
Primrec f ↔ Nat.Primrec fun n => Encodable.encode (f (Denumerable.ofNat α n))
The theorem `Primrec.dom_denumerable` states that for any types `α` and `β`, where `α` is denumerable (i.e., there exists a one-to-one correspondence between the elements of `α` and the natural numbers) and `β` is primcodable (i.e., it can be encoded as a natural number), a function `f` from `α` to `β` is primitive recursive (after encoding its input and output as natural numbers) if and only if the function that takes a natural number `n`, decodes it into an element of `α`, applies `f` and then encodes the result is primitive recursive in the natural numbers.
More concisely: For any denumerable type `α` and primcodable type `β`, a function `f` from `α` to `β` is primitive recursive if and only if the function that decodes a natural number into an element of `α`, applies `f` to it, and encodes the result as a natural number is primitive recursive.
|
Nat.Primrec'.of_eq
theorem Nat.Primrec'.of_eq :
∀ {n : ℕ} {f g : Vector ℕ n → ℕ}, Nat.Primrec' f → (∀ (i : Vector ℕ n), f i = g i) → Nat.Primrec' g
This theorem states that for any natural number `n`, and for two functions `f` and `g` that map a `Vector` of length `n` with elements of type `ℕ` to `ℕ`, if `f` is a primitive recursive function (`Nat.Primrec' f`) and if `f` and `g` are equal for every `Vector` of natural numbers of length `n` (i.e., `∀ (i : Vector ℕ n), f i = g i`), then `g` is also a primitive recursive function (`Nat.Primrec' g`). In simpler terms, this theorem establishes that the property of being primitive recursive is preserved under equation for functions from vectors of natural numbers to natural numbers.
More concisely: If `f` is a primitive recursive function mapping vectors of length `n` of natural numbers to natural numbers, and `f` equals `g` for all such vectors, then `g` is also a primitive recursive function.
|
Primrec.of_equiv
theorem Primrec.of_equiv : ∀ {α : Type u_1} [inst : Primcodable α] {β : Type u_4} {e : β ≃ α}, Primrec ⇑e
This theorem states that for any types `α` and `β`, if `α` is primitive encodable, and there exists a bijective function (or an equivalence) `e` from `β` to `α`, then the function represented by `e` (denoted by `⇑e`) is primitive recursive. In other words, if you can map every element of `β` to a unique element of `α` and vice versa, and `α` has a primitive encoding, then you can compute the function `e` in a primitive recursive manner.
More concisely: If `α` is a primitive encodable type and there exists a bijective function `e : β → α`, then the function representation `⇑e` is primitive recursive.
|
Primrec.snd
theorem Primrec.snd :
∀ {α : Type u_3} {β : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Prod.snd
The theorem `Primrec.snd` asserts that for any pair of types `α` and `β` which are Primcodable (i.e., they can be encoded as natural numbers), the function that retrieves the second component from a pair (denoted as `Prod.snd`) is considered primitive recursive. In other words, if we represent the input/output of `Prod.snd` as natural numbers, then the function corresponds to a primitive recursive function in number theory.
More concisely: The function `Prod.snd` on pairs of Primcodable types is a primitive recursive function in number theory.
|
Primrec.decode
theorem Primrec.decode : ∀ {α : Type u_1} [inst : Primcodable α], Primrec Encodable.decode
The theorem `Primrec.decode` states that for any type `α` that is primitive codable (i.e., can be encoded as and decoded from natural numbers), the function `Encodable.decode` is primitive recursive. In other words, it asserts that the process of decoding a natural number into an optional value of type `α` is a primitive recursive function. A primitive recursive function is one that can be computed using basic arithmetic operations and recursion in a finite number of steps.
More concisely: The function `Encodable.decode` for decoding a natural number into an optional value of a primitive codable type `α` is a primitive recursive function.
|
Primrec₂.encode_iff
theorem Primrec₂.encode_iff :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α → β → σ}, (Primrec₂ fun a b => Encodable.encode (f a b)) ↔ Primrec₂ f
The theorem `Primrec₂.encode_iff` states that for any types `α`, `β`, and `σ`, where each type is Primcodable, and any binary function `f` from `α` and `β` to `σ`, the encoding of the function `f` is a binary primitive recursive function if and only if `f` itself is a binary primitive recursive function. In other words, encoding doesn't change the primitive recursive nature of a binary function.
More concisely: The encoding of a binary primitive recursive function is a binary primitive recursive function.
|
Primrec.nat_rec'
theorem Primrec.nat_rec' :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → ℕ} {g : α → β}
{h : α → ℕ × β → β},
Primrec f → Primrec g → Primrec₂ h → Primrec fun a => Nat.rec (g a) (fun n IH => h a (n, IH)) (f a)
The theorem `Primrec.nat_rec'` asserts that for any types `α` and `β` that are primitive codable, and for any functions `f: α → ℕ`, `g: α → β`, `h: α → ℕ × β → β`, if `f`, `g`, and `h` are all primitive recursive functions, then the function that takes an input `a` from type `α` and applies the natural number recursion method on `f(a)`, starting from `g(a)` and with recursion function `h(a, (n, IH))`, is also a primitive recursive function. Here, `Nat.rec (g a) (fun n IH => h a (n, IH)) (f a)` is a way to represent recursion in the natural number `f(a)`, where `g(a)` is the base case and `h(a, (n, IH))` is the recursive step applied to each preceding result `IH` and its index `n`.
More concisely: If `f:` α -> Nat, `g:` α -> β, and `h:` α -> Nat x β are primitive recursive functions, then the function `Nat.rec (g a) (fun n IH => h a (n, IH)) (f a)` is also primitive recursive.
|
Primrec.ite
theorem Primrec.ite :
∀ {α : Type u_1} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Prop}
[inst_2 : DecidablePred c] {f g : α → σ},
PrimrecPred c → Primrec f → Primrec g → Primrec fun a => if c a then f a else g a
The theorem `Primrec.ite` states that for any types `α` and `σ` with instances of `Primcodable`, any decidable predicate `c : α → Prop`, and any two functions `f, g : α → σ`, if `c` is a primitive recursive predicate and `f` and `g` are primitive recursive functions, then the function which maps an element `a : α` to `f a` if `c a` holds and to `g a` otherwise is also primitive recursive. This corresponds to the primitive recursion of an if-then-else construct where the condition and both branches are primitive recursive.
More concisely: Given types `α` and `σ` with decidable and primitive recursive predicate `c : α → Prop` and primitive recursive functions `f, g : α → σ`, the function `x ↦ if h : c x then f x else g x` is primitive recursive.
|
Primrec.nat_casesOn
theorem Primrec.nat_casesOn :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → ℕ} {g : α → β}
{h : α → ℕ → β}, Primrec f → Primrec g → Primrec₂ h → Primrec fun a => Nat.casesOn (f a) (g a) (h a)
The theorem `Primrec.nat_casesOn` states that for any types `α` and `β` that can be encoded as natural numbers, and for any functions `f : α → ℕ`, `g : α → β`, and `h : α → ℕ → β`, if `f`, `g`, and `h` are all primitive recursive functions, then the function that takes an element `a` of type `α`, applies `f` to `a` to get a natural number, and then uses the `nat_casesOn` function to produce a value of type `β` based on whether the result of `f a` is zero or a successor of a natural number, is also a primitive recursive function. In other words, the primitive recursiveness is preserved under the operation of case analysis on natural numbers.
More concisely: If `f : α → ℕ`, `g : α → β`, and `h : α → ℕ → β` are primitive recursive functions, then the function `x => if h x 0 then g x else h x (S x)` is also primitive recursive, where `S` denotes the successor function.
|
Nat.Primrec'.comp₁
theorem Nat.Primrec'.comp₁ :
∀ (f : ℕ → ℕ),
(Nat.Primrec' fun v => f v.head) →
∀ {n : ℕ} {g : Vector ℕ n → ℕ}, Nat.Primrec' g → Nat.Primrec' fun v => f (g v)
This is a theorem about the composition of primitive recursive functions in natural numbers. The theorem states that for any function `f` from natural numbers to natural numbers, if `f` composed with the `head` function on a vector is primitive recursive, then for any natural number `n` and any function `g` from vectors of length `n` of natural numbers to natural numbers that is primitive recursive, the composition of `f` with `g` is also primitive recursive. In other words, if `f` and `g` are both primitive recursive functions, then their composition `f(g(v))` is also a primitive recursive function.
More concisely: If `f` is a primitive recursive function and `g` is a primitive recursive function from vectors of natural numbers to natural numbers, then their composition `f ∘ g` is also a primitive recursive function.
|
Primrec.comp₂
theorem Primrec.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 : α → β → γ},
Primrec f → Primrec₂ g → Primrec₂ fun a b => f (g a b)
The theorem `Primrec.comp₂` states that for any types `α`, `β`, `γ`, and `σ` which are primcodable, if a function `f` from `γ` to `σ` is primitive recursive and a binary function `g` from `α` and `β` to `γ` is also primitive recursive, then the binary function that first applies `g` to its inputs and then `f` to the result is also primitive recursive. In mathematical terms, the composition of two primitive recursive functions is still a primitive recursive function.
More concisely: If `f:` `γ` -> `σ` is primitive recursive and `g:` `α` x `β` -> `γ` is primitive recursive, then the composition `g` then `f:` `α` x `β` -> `σ` is primitive recursive.
|
Primrec.pred
theorem Primrec.pred : Primrec Nat.pred
The theorem `Primrec.pred` states that the predecessor function on natural numbers (`Nat.pred`) is primitive recursive. Here, the predecessor function is defined such that for any natural number `n`, if `n` is 0, its predecessor is 0; otherwise, its predecessor is `n - 1`. Primitive recursive functions are a class of functions that are defined using certain base functions and operations, and are a subset of total recursive functions. In this case, the theorem asserts that `Nat.pred` belongs to this class, after encoding its input and output as natural numbers.
More concisely: The predecessor function on natural numbers, defined as `Nat.pred(n) := if n = 0 then 0 else n - 1`, is a primitive recursive function.
|
Primrec.encode_iff
theorem Primrec.encode_iff :
∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
(Primrec fun a => Encodable.encode (f a)) ↔ Primrec f
The theorem `Primrec.encode_iff` states that for any two types `α` and `σ`, given both types are primitively encodable, and for any function `f` from `α` to `σ`, the function `f` is primitive recursive if and only if the function that applies `f` to an argument `a` from `α` and then encodes the result is also primitive recursive. This essentially says that encoding a function's output does not change whether the function is primitive recursive.
More concisely: For any primitively encodable types α and σ, and primitive recursive function f : α → σ, the function x ↦ encode (f x) is also primitive recursive, where encode is the primitively encodable function from σ to some codomain.
|
Nat.Primrec.pred
theorem Nat.Primrec.pred : Nat.Primrec Nat.pred
This theorem states that the predecessor function on natural numbers, as defined by `Nat.pred`, is primitive recursive. In the context of number theory, a function is said to be primitive recursive if it can be constructed from certain basic functions using composition and primitive recursion. Hence, this theorem is essentially a statement about the computability of the predecessor function in the natural number system.
More concisely: The predecessor function on natural numbers, defined as `Nat.pred`, is a primitive recursive function.
|
Nat.Primrec'.mul
theorem Nat.Primrec'.mul : Nat.Primrec' fun v => v.head * v.tail.head
The theorem `Nat.Primrec'.mul` states that the function taking a vector `v` to the product of its first element (i.e., the head of `v`) and the first element of the rest of the vector (i.e., the head of the tail of `v`), is primitive recursive. Here, primitive recursive means that the function can be computed using a finite number of steps, each of which may be an elementary arithmetic operation or a previously computed value.
More concisely: The function that maps a vector `v` to the product of its first element and the first element of its tail is a primitive recursive function.
|
Primrec₂.left
theorem Primrec₂.left :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec₂ fun a x => a
The theorem `Primrec₂.left` states that for any two types `α` and `β` that are primcodable (i.e., they can be encoded as natural numbers), the function which takes a pair of inputs `(a, x)` and simply returns the first element `a` is a binary primitive recursive function. In other words, the projection function that discards the second argument and returns the first one is primitive recursive.
More concisely: The function that projects the first element of a pair of primcodable types is a primitive recursive function.
|
Primrec₂.comp₂
theorem Primrec₂.comp₂ :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {σ : Type u_5} [inst : Primcodable α]
[inst_1 : Primcodable β] [inst_2 : Primcodable γ] [inst_3 : Primcodable δ] [inst_4 : Primcodable σ]
{f : γ → δ → σ} {g : α → β → γ} {h : α → β → δ},
Primrec₂ f → Primrec₂ g → Primrec₂ h → Primrec₂ fun a b => f (g a b) (h a b)
The theorem `Primrec₂.comp₂` states that if we have five types `α`, `β`, `γ`, `δ`, and `σ`, all of which have instances of `Primcodable`, and three binary functions `f`, `g`, and `h` where `f` maps from `γ` to `δ` to `σ`, `g` maps from `α` to `β` to `γ`, and `h` maps from `α` to `β` to `δ`. If these three functions `f`, `g` and `h` are primitive recursive (`Primrec₂`), then the binary function that maps `a` and `b` to `f (g a b) (h a b)` is also primitive recursive.
In simpler terms, if we have primitive recursive binary functions `f`, `g`, and `h`, then the composition of `f` with `g` and `h` is also a primitive recursive function.
More concisely: If `f : γ -> δ -> σ`, `g : α -> β -> γ`, and `h : α -> β -> δ` are primitive recursive functions, then the function `x y => f (g x y) (h x y)` is also primitive recursive.
|
Primrec.nat_rec
theorem Primrec.nat_rec :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} {g : α → ℕ × β → β},
Primrec f → Primrec₂ g → Primrec₂ fun a n => Nat.rec (f a) (fun n IH => g a (n, IH)) n
The theorem `Primrec.nat_rec` states that for all types `α` and `β` that can be encoded as natural numbers (as indicated by `[inst : Primcodable α]` and `[inst_1 : Primcodable β]`), given a function `f` from `α` to `β` and a function `g` from `α` and a pair of a natural number and `β` to `β`, if `f` is a primitive recursive function and `g` is a binary primitive recursive function, then the function that maps `a` and `n` to the result of the primitive recursive function `Nat.rec` applied to the result of `f` applied to `a` and `n` and the function that maps `n` and `IH` to the result of `g` applied to `a` and the pair `(n, IH)` is also a binary primitive recursive function. In simpler terms, it's saying that a certain type of combination of primitive recursive functions (specifically, those involving the natural number recursion function `Nat.rec`) yields another primitive recursive function.
More concisely: If `f` is a primitive recursive function from `α` to `β` and `g` is a binary primitive recursive function, then the function that maps `(a, n)` to `Nat.rec (f a n) (g a (n, IH))` is also a binary primitive recursive function.
|
Primrec.nat_mul
theorem Primrec.nat_mul : Primrec₂ fun x x_1 => x * x_1
This theorem states that the multiplication of two natural numbers is a binary primitive recursive function. In other words, the function `f(x, x_1) = x * x_1` is primitive recursive, where `x` and `x_1` are natural numbers. Primitive recursive functions are a class of functions which are computable in a certain sense, and this theorem confirms that natural number multiplication falls into this category.
More concisely: The natural number multiplication function is primitive recursive.
|
Primrec.list_foldr
theorem Primrec.list_foldr :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α → List β} {g : α → σ} {h : α → β × σ → σ},
Primrec f → Primrec g → Primrec₂ h → Primrec fun a => List.foldr (fun b s => h a (b, s)) (g a) (f a)
The theorem `Primrec.list_foldr` states that if we have three functions: `f` mapping from a type `α` to a list of type `β`, `g` mapping from type `α` to type `σ`, and `h` a binary function mapping from type `α` and a pair of type `β` and `σ` to type `σ`; if these three functions are all primitive recursive (they can be broken down into simpler recursive calls and a base case), then the function that takes an element of type `α` and applies the right-to-left fold operation on the list resulting from `f` with the binary function created from `h` and initial accumulator as the result of `g`, is also primitive recursive. In other words, it's saying that primitive recursiveness is preserved through right-to-left list folding operations.
More concisely: If `f : α -> list β`, `g : α -> σ`, and `h : α -> β -> σ -> σ` are primitive recursive functions, then the function that maps an element `x` of type `α` to the result of right-folding `h` over the list `(f x)` is also primitive recursive.
|
Primrec.option_map
theorem Primrec.option_map :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α → Option β} {g : α → β → σ},
Primrec f → Primrec₂ g → Primrec fun a => Option.map (g a) (f a)
The theorem `Primrec.option_map` states that for any types `α`, `β`, and `σ` that are primitive encodable, and any two functions `f : α → Option β` and `g : α → β → σ` that are primitive recursive, the composition of `f` and `Option.map (g a)` as `(a => Option.map (g a) (f a))` is also primitive recursive. This means that if we have a primitive recursive function `f` that maps an element of type `α` to an optional value of type `β`, and another binary primitive recursive function `g` that maps an element of type `α` and an element of type `β` to a value of type `σ`, then mapping `(g a)` over the possible values `f(a)` is primitive recursive, where `a` is from type `α`.
More concisely: Given primitive encodable types α, β, and σ, and primitive recursive functions f : α → Option β and g : α → β → σ, the function x => Option.map (g x) (f x) is primitive recursive.
|
Primrec.pair
theorem Primrec.pair :
∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {f : α → β} {g : α → γ}, Primrec f → Primrec g → Primrec fun a => (f a, g a)
The theorem `Primrec.pair` states that for any types `α`, `β`, and `γ` and any functions `f : α → β` and `g : α → γ`, if `f` and `g` are primitive recursive (i.e., their computations can be implemented using a limited set of operations and they terminate after a finite number of steps), then the function that takes an input `a` of type `α` and returns the pair `(f a, g a)` is also primitive recursive. This means that we can construct a new primitive recursive function by pairing the outputs of two given primitive recursive functions.
More concisely: If functions `f : α → β` and `g : α → γ` are primitive recursive, then the function `x ↦ (f x, g x)` from `α` to `β × γ` is also primitive recursive.
|
Primrec.subtype_val_iff
theorem Primrec.subtype_val_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {p : β → Prop}
[inst_2 : DecidablePred p] {hp : PrimrecPred p} {f : α → Subtype p}, (Primrec fun a => ↑(f a)) ↔ Primrec f
The theorem `Primrec.subtype_val_iff` states that for any two types `α` and `β` which are primcodable (i.e., they can be encoded as natural numbers), a decidable predicate `p` on `β`, a primitive recursive predicate `hp` which tests `p`, and a function `f : α → Subtype p` (that is, a function from `α` to the subtype of `β` determined by `p`), the function `f` is primitive recursive if and only if the function that gets the original element in `β` from the result of `f` is primitive recursive. Essentially, this theorem says that working with subtypes does not affect the property of being primitive recursive.
More concisely: For types `α` and `β` that are primcodable, a function `f : α → Subtype (p : β → Prop)` is primitive recursive if and only if the function `λ x, p x <| f x` is primitive recursive, where `<|` is the extraction operator for subtypes.
|
PrimrecPred.of_eq
theorem PrimrecPred.of_eq :
∀ {α : Type u_1} [inst : Primcodable α] {p q : α → Prop} [inst_1 : DecidablePred p] [inst_2 : DecidablePred q],
PrimrecPred p → (∀ (a : α), p a ↔ q a) → PrimrecPred q
The theorem `PrimrecPred.of_eq` states that for any type `α` that has a `Primcodable` instance and any two decidable predicates `p` and `q` over `α`, if `p` is a primitive recursive predicate and for all `α`, `p a` is logically equivalent to `q a`, then `q` is also a primitive recursive predicate. Essentially, this means that if two predicates are logically equivalent and one of them is known to be primitive recursive, then the other one is also guaranteed to be primitive recursive.
More concisely: If `p` is a primitive recursive predicate over type `α` and logically equivalent to decidable predicate `q`, then `q` is also primitive recursive.
|
Primrec.option_some_iff
theorem Primrec.option_some_iff :
∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {f : α → σ},
(Primrec fun a => some (f a)) ↔ Primrec f
The theorem `Primrec.option_some_iff` establishes an equivalence condition for the primitive recursiveness of a function `f` which maps from type `α` to `σ`, under the assumption that both `α` and `σ` are primcodable. Specifically, it states that wrapping the output of `f` with `some` (thereby mapping `α` to `Option σ`) is primitive recursive if and only if `f` itself is primitive recursive.
More concisely: The function `f : α -> σ` is primitive recursive if and only if the function `x => some (f x) : Option σ` is primitive recursive, given that both `α` and `σ` are primcodable.
|
Nat.Primrec'.tail
theorem Nat.Primrec'.tail : ∀ {n : ℕ} {f : Vector ℕ n → ℕ}, Nat.Primrec' f → Nat.Primrec' fun v => f v.tail
The theorem `Nat.Primrec'.tail` states that if we have a function `f`, which takes a vector of natural numbers of length `n` and returns a natural number, and this function `f` is primitive recursive (`Nat.Primrec' f`), then the function that applies `f` to the tail of its input vector (`fun v => f (Vector.tail v)`) is also primitive recursive. In other words, the theorem guarantees that getting the tail of a vector preserves the property of being primitive recursive.
More concisely: If `f` is a primitive recursive function from vectors of natural numbers to natural numbers, then the function `x => f (Vector.tail x)` is also primitive recursive.
|
Nat.Primrec'.of_prim
theorem Nat.Primrec'.of_prim : ∀ {n : ℕ} {f : Vector ℕ n → ℕ}, Primrec f → Nat.Primrec' f
The theorem `Nat.Primrec'.of_prim` states that for any natural number `n` and any function `f` from `Vector ℕ n` (a list of length `n` with elements of type `ℕ`) to `ℕ`, if `f` is primitive recursive (i.e., `Primrec f` holds), then `f` is also primitive recursive in the natural numbers (i.e., `Nat.Primrec' f` holds). In terms of computation theory, this theorem says that any function that can be computed using primitive recursion on arbitrary data types (as long as they can be encoded as natural numbers) can also be computed using primitive recursion directly on natural numbers.
More concisely: If a function from a vector of natural numbers to natural numbers is primitive recursive, then it is also primitive recursive as a function from natural numbers to natural numbers.
|
Primrec.const
theorem Primrec.const :
∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] (x : σ), Primrec fun x_1 => x := by
sorry
The theorem `Primrec.const` states that for any types `α` and `σ` that are encodable (as indicated by `Primcodable α` and `Primcodable σ`), and any constant `x` of type `σ`, the function that maps every element of type `α` to the constant `x` is primitive recursive. In other words, if we can encode the types `α` and `σ` as natural numbers, then a function that always returns a fixed value regardless of its input is considered primitive recursive.
More concisely: For types `α` and `σ` that are encodable as natural numbers and any constant `x` of type `σ`, the function that maps every `α` to `x` is primitive recursive.
|
Nat.Primrec.const
theorem Nat.Primrec.const : ∀ (n : ℕ), Nat.Primrec fun x => n
This theorem states that for any natural number `n`, a function that always returns `n` is a primitive recursive function. In other words, regardless of the input, if a function simply outputs a specific value - in this case, `n` - then it qualifies as a primitive recursive function according to the principles of Natural numbers and primitive recursion in Lean 4.
More concisely: Any constant function from natural numbers to natural numbers is primitive recursive.
|
Primrec.nat_add
theorem Primrec.nat_add : Primrec₂ fun x x_1 => x + x_1
The theorem `Primrec.nat_add` states that the function of two natural numbers that adds them together is a binary primitive recursive function. In other words, the addition operation for natural numbers can be computed using a sequence of basic arithmetic operations and control structures, such as loops or recursion, that halt after a finite number of steps.
More concisely: The `Primrec.nat_add` theorem asserts that the addition function on natural numbers is a primitive recursive function.
|
Nat.Primrec'.const
theorem Nat.Primrec'.const : ∀ {n : ℕ} (m : ℕ), Nat.Primrec' fun x => m
This theorem states that for any natural number `n` and `m`, the function that always returns `m` (i.e., a constant function) is primitive recursive. In other words, regardless of the input `x`, the function always outputs the constant value `m`, and this function is defined to be primitive recursive. Primitive recursive functions are a class of functions that can be obtained by a restricted set of operations, and the fact that a constant function is within this class is what this theorem asserts.
More concisely: The constant function from natural numbers to a constant value is a primitive recursive function.
|
Primrec.vector_cons
theorem Primrec.vector_cons : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec₂ Vector.cons
The theorem `Primrec.vector_cons` asserts that for any type `α` which is Primcodable (denoted by `[inst : Primcodable α]`), and for any natural number `n`, the function `Vector.cons` is a binary primitive recursive function. In other words, given any element of type `α` and a vector of `n` elements of type `α`, we can construct a new vector of length `n + 1` (by appending the element to the beginning of the existing vector) in a way that is computationally primitive recursive.
More concisely: For any type `α` that is Primcodable and natural number `n`, the function ` Vector.cons : α → Vector α n → Vector α (n + 1)` is a primitive recursive function.
|
Primrec.cond
theorem Primrec.cond :
∀ {α : Type u_1} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Bool} {f g : α → σ},
Primrec c → Primrec f → Primrec g → Primrec fun a => bif c a then f a else g a
The theorem `Primrec.cond` states that for all types `α` and `σ`, if `α` and `σ` are both primitive encodable, then for any functions `c : α → Bool`, `f : α → σ`, and `g : α → σ`, if `c`, `f`, and `g` are all primitive recursive (i.e., their input and output can be encoded as natural numbers), then the function which maps `a` in `α` to `f(a)` if `c(a)` is true and to `g(a)` if `c(a)` is false, is also primitive recursive. This essentially says that the "if-then-else" construction preserves primitive recursiveness.
More concisely: If `α` and `σ` are primitive encodable types, and `c : α → Bool`, `f : α → σ`, and `g : α → σ` are primitive recursive functions, then the function `x ↦ if h x then f x else g x` is also primitive recursive, for any `h : α → Bool`.
|
Nat.Primrec'.to_prim
theorem Nat.Primrec'.to_prim : ∀ {n : ℕ} {f : Vector ℕ n → ℕ}, Nat.Primrec' f → Primrec f
This theorem is stating that for all natural numbers `n` and for all functions `f` from `Vector ℕ n` to `ℕ` (i.e., functions taking a vector of `n` natural numbers and returning a natural number), if `f` is primitive recursive according to `Nat.Primrec'` definition, then `f` is also primitive recursive according to the `Primrec` definition. In other words, it is saying that the `Nat.Primrec'` primitive recursion concept implies the `Primrec` concept for functions from vectors of natural numbers to natural numbers.
More concisely: If `f` is a primitive recursive function from `Vector ℕ n` to `ℕ` according to the `Nat.Primrec'` definition, then `f` is also primitive recursive according to the `Primrec` definition.
|
Primrec.option_bind
theorem Primrec.option_bind :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α → Option β} {g : α → β → Option σ},
Primrec f → Primrec₂ g → Primrec fun a => (f a).bind (g a)
The `Primrec.option_bind` theorem states that for any types `α`, `β`, and `σ` that are `Primcodable` (meaning that there exists a way to encode objects of these types as natural numbers), if we have a primitive recursive function `f` from `α` to `Option β`, and a binary primitive recursive function `g` from `α` and `β` to `Option σ`, then the function that takes `a` in `α` and binds the result of `f a` to the second argument of `g a` using the `Option.bind` operation is also primitive recursive. This theorem essentially confirms that the `Option.bind` operation preserves the property of primitive recursion.
More concisely: If `f` is a primitive recursive function from `α` to `Option β`, and `g` is a binary primitive recursive function from `α` and `β` to `Option σ`, then the function `x ↦ Option.bind (f x) g` is primitive recursive.
|
Primrec.vector_tail
theorem Primrec.vector_tail : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec Vector.tail
This theorem states that for any type `α` which can be primarily encoded and for any natural number `n`, the function `Vector.tail`, which returns the tail of a vector (with an empty vector resulting in an empty tail), is a primitive recursive function. In other words, `Vector.tail` is a function that, after encoding its input and output as natural numbers, can be computed using only basic operations and recursion on natural numbers.
More concisely: The function `Vector.tail` on type `α` is a primitive recursive function on natural numbers.
|
Primrec₂.const
theorem Primrec₂.const :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] (x : σ), Primrec₂ fun x_1 x_2 => x
The theorem `Primrec₂.const` states that for any types `α`, `β`, and `σ` which have a `Primcodable` instance, and for any specific value `x` of type `σ`, the function that ignores its two inputs of types `α` and `β` and always returns the constant `x` is a binary primitive recursive function. This simply means that constant functions are considered primitive recursive regardless of the types of their inputs.
More concisely: For any types `α`, `β`, and `σ` with `Primcodable` instance, and any constant function `f : σ -> α -> β -> σ`, the function `f _ _ = x` is primitive recursive.
|
Primrec.vector_toList
theorem Primrec.vector_toList : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec Vector.toList
The theorem `Primrec.vector_toList` states that for any type `α` that is primcodable (i.e., can be encoded and decoded as natural numbers), and any natural number `n`, the function that converts a vector of length `n` of elements of type `α` to a list is primitive recursive. In other words, the operation of converting a vector to a list can be carried out via a sequence of simple computational steps, the number of which is determined by the size of the input vector.
More concisely: For any primcodable type `α` and natural number `n`, the function converting a vector of length `n` of `α` elements to a list is primitive recursive.
|
Primrec.list_get?
theorem Primrec.list_get? : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ List.get?
This theorem states that for all types `α` that have a `Primcodable` instance (meaning we can encode and decode values of type `α`), the binary function `List.get?` is a primitive recursive function. In simpler terms, the function `List.get?`, which takes a list and an index and returns the option of the element at that index (with `none` when the index is out of bounds), can be computed using only basic functions and recursion on nonnegative integers.
More concisely: For all types `α` with a `Primcodable` instance, the function `List.get? : ∀ (l : List α) (i : ℕ), Option α` is a primitive recursive function.
|
Nat.Primrec'.head
theorem Nat.Primrec'.head : ∀ {n : ℕ}, Nat.Primrec' Vector.head
This theorem states that for any natural number `n`, the `head` function, which retrieves the first element from a vector of length at least `1`, is a primitive recursive function. This means that the function `Vector.head` is computationally basic - it can be computed using a finite number of simple operations.
More concisely: The `Vector.head` function, which returns the first element of a non-empty vector, is a primitive recursive function.
|
Primrec.fst
theorem Primrec.fst :
∀ {α : Type u_3} {β : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec Prod.fst
The theorem `Primrec.fst` states that for all types `α` and `β` which have a primitive recursive encoding (i.e., they are instances of the `Primcodable` class), the first projection function `Prod.fst` is a primitive recursive function. In other words, given a pair of elements `(a, b)` where `a` is from type `α` and `b` is from type `β`, the function that retrieves the first element `a` from the pair is a primitive recursive function.
More concisely: For types `α` and `β` that are primitive recursively encodable, the first projection function `Prod.fst` on pairs of elements from types `α` and `β` is a primitive recursive function.
|
Primrec.encode
theorem Primrec.encode : ∀ {α : Type u_1} [inst : Primcodable α], Primrec Encodable.encode
The theorem `Primrec.encode` states that for any type `α` that is primcodable (i.e., it can be encoded as a natural number), the encoding function `Encodable.encode` is primitive recursive. In other words, the process of encoding an element of such a type `α` into a natural number can be defined using a finite set of basic operations and recursion.
More concisely: For any primcodable type `α`, the encoding function `Encodable.encode α` is primitive recursive.
|
Primrec.option_casesOn
theorem Primrec.option_casesOn :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {o : α → Option β} {f : α → σ} {g : α → β → σ},
Primrec o → Primrec f → Primrec₂ g → Primrec fun a => Option.casesOn (o a) (f a) (g a)
This theorem states that for any types `α`, `β`, and `σ` that are primcodable (that is, there is a way to represent their elements as natural numbers), given a function `o` mapping from `α` to `Option β`, a function `f` mapping from `α` to `σ`, and a binary function `g` mapping from `α` and `β` to `σ`, if `o`, `f`, and `g` are all primitive recursive (meaning they can be computed by a sequence of basic operations), then the function that takes an element of `α`, applies `o` to it and uses `Option.casesOn` to either apply `f` or `g` depending on whether `o` returns `None` or `Some`, is also primitive recursive.
More concisely: Given primcodable types `α`, `β`, and `σ`, if `o`: `α -> Option β`, `f: α -> σ`, and `g: α x β -> σ` are primitive recursive functions, then the function `x => Option.casesOn o x (λ none => f x) (λ some => g x some)` is also primitive recursive.
|
Primrec₂.comp
theorem Primrec₂.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 : α → γ},
Primrec₂ f → Primrec g → Primrec h → Primrec fun a => f (g a) (h a)
The theorem `Primrec₂.comp` states that for all types `α`, `β`, `γ`, and `σ`, if `f` is a binary primitive recursive function that maps values from type `β` and `γ` to type `σ`, `g` is a primitive recursive function that maps values from type `α` to `β`, and `h` is a primitive recursive function that maps values from type `α` to `γ`, then the function that takes an input of type `α` and maps it to `f(g(a), h(a))` is also a primitive recursive function. This means that the composition of primitive recursive functions is again primitive recursive.
More concisely: If `f` is a binary primitive recursive function and `g` and `h` are primitive recursive functions, then the composition `x ↦ f(g(x), h(x))` is a primitive recursive function.
|
Primrec.nat_double
theorem Primrec.nat_double : Primrec fun n => 2 * n
The theorem `Primrec.nat_double` states that the function which doubles a natural number is primitive recursive. In other words, if you take a natural number and multiply it by 2, the resulting function is guaranteed to be primitive recursive, meaning there is an algorithm that can compute it using a finite number of simple operations. The "Primrec" in the theorem's name refers to the property of being primitive recursive.
More concisely: The function that doubles a natural number is a primitive recursive function.
|
Primrec.id
theorem Primrec.id : ∀ {α : Type u_1} [inst : Primcodable α], Primrec id
The theorem `Primrec.id` states that for any type `α` that is primcodable (i.e., can be encoded as a natural number), the identity function `id` on `α` is primitive recursive. In other words, when the input and output of the identity function are encoded as natural numbers, the resulting function is primitive recursive.
More concisely: The identity function on a primcodable type is primitive recursive.
|
Nat.Primrec.id
theorem Nat.Primrec.id : Nat.Primrec id
This theorem states that the identity function is a primitive recursive function for natural numbers. In other words, given any natural number, its identity (i.e., the number itself) can be computed using only a finite number of steps that involve basic arithmetic operations and conditionals, a characteristic of primitive recursive functions.
More concisely: The Identity function is a primitive recursive function on natural numbers.
|
Primrec.nat_double_succ
theorem Primrec.nat_double_succ : Primrec fun n => 2 * n + 1
This theorem states that the function that maps each natural number `n` to `2*n + 1` is primitive recursive. In other words, for every natural number `n`, the operation of doubling `n` and then adding 1 can be computed using a fixed, finite number of steps, with each step being a basic arithmetic operation or a test for zero or equality.
More concisely: The function that maps each natural number `n` to `2*n + 1` is a primitive recursive function.
|
Nat.Primrec'.if_lt
theorem Nat.Primrec'.if_lt :
∀ {n : ℕ} {a b f g : Vector ℕ n → ℕ},
Nat.Primrec' a →
Nat.Primrec' b → Nat.Primrec' f → Nat.Primrec' g → Nat.Primrec' fun v => if a v < b v then f v else g v
This theorem states that for any natural number `n`, and for any functions `a`, `b`, `f`, and `g` that map a vector of natural numbers of length `n` to a natural number, if `a`, `b`, `f`, and `g` are all primitive recursive (denoted by `Nat.Primrec'`), then the function that takes a vector `v` and returns the result of `f v` if `a v` is less than `b v`, otherwise returns `g v`, is also primitive recursive. Essentially, it asserts the primitive recursiveness of an 'if-then-else' construct where the condition involves a comparison of two primitive recursive functions and the 'then' and 'else' parts are also primitive recursive functions.
More concisely: If `a`, `b`, `f`, and `g` are primitive recursive functions mapping a vector of natural numbers to natural numbers, then the function that applies `f` if `a` is less than `b` and `g` otherwise is also primitive recursive.
|
Primrec.vector_head
theorem Primrec.vector_head : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec Vector.head
The theorem `Primrec.vector_head` asserts that for any type `α` that has an instance of `Primcodable` and for any natural number `n`, the function `Vector.head`, which retrieves the first element of a vector, is primitive recursive. This means that `Vector.head` can be computed using simple arithmetic operations, conditional statements, and bounded loops or recursion after encoding its input and output as natural numbers, which is the definition of a primitive recursive function.
More concisely: The theorem asserts that the function `Vector.head` on types `α` with `Primcodable` instance and natural numbers is primitive recursive.
|
Primrec.vector_get
theorem Primrec.vector_get : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec₂ Vector.get
This theorem, `Primrec.vector_get`, asserts that for any type `α` that can be coded (as indicated by `[inst : Primcodable α]`) and any natural number `n`, the function `Vector.get` is a binary primitive recursive function. In simpler terms, fetching the nth element from a vector of length `n` whose elements are of type `α` is a process that can be broken down into primitive recursive steps. `Vector.get` is a function that takes a Vector of `α` elements and a `Fin n` (a finite ordinal number less than `n`) and returns the element at that specific position in the vector.
More concisely: The function `Vector.get` on vectors of type `α` is a primitive recursive function.
|
Primrec.list_concat
theorem Primrec.list_concat : ∀ {α : Type u_1} [inst : Primcodable α], Primrec₂ fun l a => l ++ [a]
The theorem `Primrec.list_concat` states that for any type `α` that is 'Primcodable' (can be encoded as a natural number), the function that takes a list `l` and an element `a` of type `α`, and appends `a` to the end of `l` to form a new list, is a binary primitive recursive function. In other words, given a list of elements and a single element, both of `Primcodable` type `α`, the operation of appending the single element to the end of the list is a primitive recursive operation.
More concisely: The function that appends an element to the end of a list, given a list and an element of a Primcodable type, is a primitive recursive function.
|
Primrec.succ
theorem Primrec.succ : Primrec Nat.succ
The theorem `Primrec.succ` states that the successor function on natural numbers, denoted `Nat.succ`, is primitive recursive. In other words, for the function that takes a natural number and returns its successor (i.e., increases the number by one), this function can be computed by a process that is "primitive recursive". This means that the function can be computed by a procedure that involves only basic mathematical operations and recursion.
More concisely: The successor function on natural numbers is primitive recursive.
|
Primrec₂.unpaired'
theorem Primrec₂.unpaired' : ∀ {f : ℕ → ℕ → ℕ}, Nat.Primrec (Nat.unpaired f) ↔ Primrec₂ f
The theorem `Primrec₂.unpaired'` establishes a correspondence between a function being binary primitive recursive and its unpaired version being natural number primitive recursive. In other words, for any function `f` that maps two natural numbers to another natural number, `f` is a binary primitive recursive function if and only if the function obtained by applying `Nat.unpaired` to `f` is a primitive recursive function for natural numbers. Here, `Nat.unpaired f` is a function that takes a single natural number, decodes it into a pair of natural numbers using the pairing function, and applies `f` to the pair.
More concisely: A binary function is primitive recursive if and only if its unpaired version, obtained by applying `Nat.unpaired` and composing with the pairing function, is a primitive recursive function for natural numbers.
|
Primrec.comp
theorem Primrec.comp :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : β → σ} {g : α → β}, Primrec f → Primrec g → Primrec fun a => f (g a)
The theorem `Primrec.comp` states that if `f` is a primitive recursive function from type `β` to type `σ`, and `g` is a primitive recursive function from type `α` to type `β`, then the composition of `f` and `g` (given by `fun a => f (g a)`) is also a primitive recursive function. Here, the types `α, β, σ` are assumed to be primcodable, meaning that they can be encoded and decoded as natural numbers.
More concisely: If `f` is a primitive recursive function from type `β` to type `σ` and `g` is a primitive recursive function from type `α` to type `β`, then the composition `f ∘ g` defined as `x ↦ f (g x)` is a primitive recursive function.
|
Primrec₂.right
theorem Primrec₂.right :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Primrec₂ fun x b => b
The theorem `Primrec₂.right` states that for any two types `α` and `β` that have a primitive recursive encoding (`Primcodable`), the second projection function (which takes a pair `(x, b)` and returns `b`) is a binary primitive recursive function. In other words, the function that retrieves the second component of a pair is primitive recursive.
More concisely: The second projection function on pairs of primitive recursively encodable types is a primitive recursive function.
|
PrimrecRel.comp
theorem PrimrecRel.comp :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable γ] {R : β → γ → Prop} [inst_3 : (a : β) → (b : γ) → Decidable (R a b)] {f : α → β}
{g : α → γ}, PrimrecRel R → Primrec f → Primrec g → PrimrecPred fun a => R (f a) (g a)
The theorem `PrimrecRel.comp` states that for any types `α`, `β`, and `γ`, if all three are primitive encodable (as denoted by `Primcodable α`, `Primcodable β`, and `Primcodable γ`), and if we have a primitive recursive relation `R` between `β` and `γ` (with `R : β → γ → Prop`), and the relation `R` is decidable for all `a : β` and `b : γ`, then given any two functions `f : α → β` and `g : α → γ` which are both primitive recursive, the function that maps an element of type `α` to the boolean value of the relationship `R` applied to `(f a, g a)` is also primitive recursive. This implies that the composition of primitive recursive functions and relations retains the property of being primitive recursive.
More concisely: If types `α`, `β`, and `γ` are primitive encodable, `R : β → γ → Prop` is a decidable primitive recursive relation between `β` and `γ`, and `f : α → β` and `g : α → γ` are primitive recursive functions, then the function `x => Decide R (f x) (g x)` is primitive recursive.
|
Primrec.subtype_val
theorem Primrec.subtype_val :
∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p] {hp : PrimrecPred p},
Primrec Subtype.val
The theorem `Primrec.subtype_val` establishes that for any type `α` that can be encoded as a natural number (i.e., it satisfies the `Primcodable` class), any decidable predicate `p` on `α`, and under the condition that `p` is a primitive recursive predicate (`PrimrecPred p`), the function `Subtype.val` is also primitive recursive (`Primrec`). In other words, the function that retrieves the underlying element from a subtype defined by the predicate `p` is primitive recursive. This means that there exists a primitive recursive function which, given a natural number encoding of an element of the subtype, returns the natural number encoding of the underlying element of the base type `α`. The theorem asserts the computability property of the subtype extraction operation under specific settings.
More concisely: The theorem `Primrec.subtype_val` asserts that for any type `α` encodable as a natural number and decidable primitive recursive predicate `p` on `α`, the function `Subtype.val` extracting the underlying element from a subtype defined by `p` is also primitive recursive.
|
Primrec.nat_le
theorem Primrec.nat_le : PrimrecRel fun x x_1 => x ≤ x_1
The theorem `Primrec.nat_le` states that the relation of "less than or equal to" (`≤`) for two natural numbers is a primitive recursive relation. In other words, the function that takes two natural numbers and returns a boolean value indicating whether the first number is less than or equal to the second number, is primitive recursive. This function is decidable, meaning that for any two natural numbers, it can definitively determine whether the first is less than or equal to the second.
More concisely: The relation ≤ on natural numbers is a decidable, primitive recursive predicate.
|
Nat.Primrec'.comp₂
theorem Nat.Primrec'.comp₂ :
∀ (f : ℕ → ℕ → ℕ),
(Nat.Primrec' fun v => f v.head v.tail.head) →
∀ {n : ℕ} {g h : Vector ℕ n → ℕ}, Nat.Primrec' g → Nat.Primrec' h → Nat.Primrec' fun v => f (g v) (h v)
The theorem `Nat.Primrec'.comp₂` states that for any function `f` mapping two natural numbers to a natural number, if `f` composed with the head operation of a vector and the head operation of the tail of a vector is primitive recursive, then for any natural number `n` and any two functions `g` and `h` from vectors of length `n` to natural numbers that are primitive recursive, the function that maps a vector `v` to `f` applied to `g(v)` and `h(v)` is also primitive recursive. In other words, if `f` is primitive recursive when applied to the first two elements of a vector, and `g` and `h` are primitive recursive, then the composition of `f` with `g` and `h` is also primitive recursive.
More concisely: If functions `f` (mapping two natural numbers to a natural number), `g`, and `h` (each mapping vectors of length `n` to natural numbers) are primitive recursive, then the function that maps a vector `v` to `f` applied to `g(v)` and `h(v)` is also primitive recursive.
|
Primrec.to₂
theorem Primrec.to₂ :
∀ {α : Type u_1} {β : Type u_2} {σ : Type u_5} [inst : Primcodable α] [inst_1 : Primcodable β]
[inst_2 : Primcodable σ] {f : α × β → σ}, Primrec f → Primrec₂ fun a b => f (a, b)
The theorem `Primrec.to₂` states that for any types `α`, `β`, and `σ` that are encodable (denoted by `Primcodable α`, `Primcodable β`, and `Primcodable σ`), if a function `f` mapping from a pair of type `α` and `β` to `σ` is primitive recursive (expressed as `Primrec f`), then the corresponding binary function that takes two separate arguments of type `α` and `β` and applies `f` to the pair of them is also primitive recursive (expressed as `Primrec₂ fun a b => f (a, b)`). In other words, this theorem proves that if a function is primitive recursive when applied to a pair, it remains primitive recursive when its arguments are separated.
More concisely: If `f : α × β → σ` is a primitive recursive function between encodable types, then the corresponding function `g : α → β → σ` defined as `g a b := f (a, b)` is also primitive recursive.
|
Primrec.beq
theorem Primrec.beq : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : DecidableEq α], Primrec₂ BEq.beq
The theorem `Primrec.beq` asserts that for any type `α` that is both Primcodable and has Decidable Equality, the boolean equality function `BEq.beq` is a binary primitive recursive function. In other words, given two elements of type `α`, it is possible to decide their equality in a primitive recursive manner using boolean logic. This means that `BEq.beq` can be computed by a primitive recursive function, which is a fundamental concept in computability theory.
More concisely: For any Primcodable and equalitable type `α`, the boolean equality function `BEq.beq` on `α` is primitive recursive.
|
Primrec.eq
theorem Primrec.eq : ∀ {α : Type u_1} [inst : Primcodable α] [inst_1 : DecidableEq α], PrimrecRel Eq
The theorem `Primrec.eq` asserts that for any type `α` that is primcodable and has decidable equality, the equality relation `Eq` is a primitive recursive relation. In other words, it's stating that for all `α`, if `α` is a type that can be encoded in a primitive way and can decide whether two elements are equal or not, then the standard equality function from `α` to `α` to `Prop` can be determined in a primitive recursive manner. This implies that the function `decide ∘ Eq : α → α → Bool` is primitive recursive.
More concisely: For any primcodable and decidably equal type α, the standard equality relation Eq : α → α → Prop is a primitive recursive relation.
|
Primrec.unpair
theorem Primrec.unpair : Primrec Nat.unpair
This theorem states that the unpairing function for natural numbers, `Nat.unpair`, is primitive recursive. In other words, `Nat.unpair` can be computed using a finite number of steps, where each step involves only basic arithmetic operations. The function `Nat.unpair` takes a natural number and returns a pair of natural numbers such that the input number can be represented as a combination of the pair in a certain way.
More concisely: The `Nat.unpair` function, which takes a natural number and returns a pair of natural numbers representing its decomposition into a sum of two parts, is a primitive recursive function.
|
Primrec.dom_bool
theorem Primrec.dom_bool : ∀ {α : Type u_1} [inst : Primcodable α] (f : Bool → α), Primrec f
The theorem `Primrec.dom_bool` states that for any type `α`, which has a `Primcodable` instance, and for any function `f` from `Bool` to `α`, the function `f` is primitive recursive. In other words, whenever we have a function that takes a boolean value and produces an output in some type `α`, that function can be described using only the basic constructs of primitive recursion.
More concisely: For any type `α` with a `Primcodable` instance and any function `f : Bool → α`, `f` is a primitive recursive function.
|
Primrec.vector_toList_iff
theorem Primrec.vector_toList_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {n : ℕ} {f : α → Vector β n},
(Primrec fun a => (f a).toList) ↔ Primrec f
The theorem `Primrec.vector_toList_iff` states that for any types `α` and `β` that can be encoded as natural numbers (denoted by `Primcodable α` and `Primcodable β`), and any natural number `n`, a function `f` from `α` to vectors of length `n` with elements of type `β` (`α → Vector β n`) is primitive recursive if and only if the function that maps `α` to the list obtained from the vector `f(a)` (`fun a => Vector.toList (f a)`) is primitive recursive. In other words, converting the outputs of a function from vectors to lists does not change whether the function is primitive recursive.
More concisely: For types `α` and `β` encodable as natural numbers, and natural number `n`, a function `f : α → Vector β n` is primitive recursive if and only if the function `g : α → List β` defined by `g a := Vector.toList (f a)` is primitive recursive.
|
Primrec.of_graph
theorem Primrec.of_graph :
∀ {α : Type u_1} [inst : Primcodable α] {f : α → ℕ},
Primrec.PrimrecBounded f → (PrimrecRel fun a b => f a = b) → Primrec f
The theorem `Primrec.of_graph` states that for any type `α` that is primcodable, and any function `f : α → ℕ`, if the function `f` is bounded by a primitive recursive function (as denoted by `Primrec.PrimrecBounded f`) and the graph of the function `f` (expressed as the relation `(a, b) => f a = b`) is a primitive recursive relation (denoted by `PrimrecRel`), then the function `f` itself is primitive recursive (`Primrec f`). In other words, to show a function mapping from type `α` to natural numbers is primitive recursive, it suffices to demonstrate that it is bounded by a primitive recursive function and that its graph is a primitive recursive relation.
More concisely: If a type `α`'s function `f : α → ℕ` is bounded by a primitive recursive function and its graph is a primitive recursive relation, then `f` is primitive recursive.
|
Primrec.nat_iff
theorem Primrec.nat_iff : ∀ {f : ℕ → ℕ}, Primrec f ↔ Nat.Primrec f
The theorem `Primrec.nat_iff` states that for any function `f` from natural numbers to natural numbers, `f` is primitive recursive (i.e., `Primrec f`) if and only if `f` is primitive recursive as per the native definition in Lean (`Nat.Primrec f`). In other words, if `f` is primitive recursive, then it remains so when we consider its input and output as encoded natural numbers. And if `f` is primitive recursive on natural numbers, then it is also primitive recursive when we consider the encoding scheme.
More concisely: The theorem `Primrec.nat_iff` asserts that a function from natural numbers to natural numbers is primitive recursive in Lean if and only if it is primitive recursive according to the standard definition.
|
Primrec₂.ofNat_iff
theorem Primrec₂.ofNat_iff :
∀ {α : Type u_4} {β : Type u_5} {σ : Type u_6} [inst : Denumerable α] [inst_1 : Denumerable β]
[inst_2 : Primcodable σ] {f : α → β → σ},
Primrec₂ f ↔ Primrec₂ fun m n => f (Denumerable.ofNat α m) (Denumerable.ofNat β n)
This theorem `Primrec₂.ofNat_iff` states that for all types `α`, `β`, and `σ`, wherein `α` and `β` are denumerable and `σ` is primcodable, and for a binary function `f` from `α` and `β` to `σ`, the function `f` is primitive recursive if and only if the function that maps two natural numbers `m` and `n` to `f` applied to the `m`-th element of `α` and the `n`-th element of `β` is also primitive recursive. In other words, a binary function `f` is primitive recursive exactly when its corresponding function in the natural numbers domain, that uses denumerable indexing, is primitive recursive.
More concisely: A binary function between two denumerable types is primitive recursive if and only if the function that maps natural numbers to applications of the binary function to the corresponding elements in each type is primitive recursive.
|