Nat.shiftLeft_eq'
theorem Nat.shiftLeft_eq' : ∀ (m n : ℕ), m.shiftLeft n = m <<< n
This theorem, `Nat.shiftLeft_eq'`, states that for all natural numbers `m` and `n`, the operation of shifting `m` to the left by `n` places is equivalent to the bitwise shift operation `m <<< n`. In other words, the `shiftLeft` function on natural numbers is equivalent to the `<<<` operation as defined in Lean's standard library.
More concisely: For all natural numbers m and n, m shifted left by n places equals m bitwise left-shifted by n.
|
Nat.bit_val
theorem Nat.bit_val : ∀ (b : Bool) (n : ℕ), Nat.bit b n = 2 * n + bif b then 1 else 0
The theorem `Nat.bit_val` states that for any boolean `b` and natural number `n`, the value of the function `Nat.bit` applied with arguments `b` and `n` is equivalent to twice the value of `n` plus either 1 if `b` is true or 0 if `b` is false. Essentially, this function appends the boolean `b` as a binary digit to the binary representation of `n`, where `true` corresponds to `1` and `false` corresponds to `0`, and this theorem gives the numeric value of the resulting binary number.
More concisely: For any natural number `n` and boolean `b`, `Nat.bit b n` equals 2*{n} + IEEE.bool_to_int b, where IEEE.bool_to_int is the Lean function mapping boolean values to integers (0 for false and 1 for true).
|
Nat.bodd_succ
theorem Nat.bodd_succ : ∀ (n : ℕ), n.succ.bodd = !n.bodd
The theorem `Nat.bodd_succ` states that for every natural number `n`, the boolean value indicating whether or not the successor of `n` (i.e., `n+1`) is odd is the negation of the boolean value indicating whether `n` is odd. In other words, if `n` is odd, then `n+1` is not, and vice versa.
More concisely: For every natural number `n`, the oddness of `n` and `n+1` are opposite.
|
Nat.binaryRec.proof_4
theorem Nat.binaryRec.proof_4 : ∀ {C : ℕ → Sort u_1} (n : ℕ), n = 0 → C n = C 0
This theorem states that for any natural number `n` and any function `C` from natural numbers to some sort `u_1`, if `n` is equal to zero, then the value of `C` at `n` is the same as the value of `C` at zero. In other words, for a given function `C`, the theorem asserts that the function's value at zero remains the same regardless if we input `0` directly or another number `n` that is equivalent to `0`.
More concisely: For any function `C` from natural numbers to some sort `u_1`, `C(0) = C(n)` whenever `n` is equal to zero.
|
Nat.bodd_add_div2
theorem Nat.bodd_add_div2 : ∀ (n : ℕ), (bif n.bodd then 1 else 0) + 2 * n.div2 = n
The theorem `Nat.bodd_add_div2` states that for any natural number `n`, if `n` is odd (determined by `Nat.bodd n`), then adding `1` to twice the greatest integer smaller than `n/2` (`2 * Nat.div2 n`) gives `n` itself. If `n` is not odd (i.e., even), then adding `0` to twice of `⌊n/2⌋` still gives `n`. Essentially, this theorem is expressing an integer as the sum of an odd/even indicator (1 or 0) and twice a rounded-down half.
More concisely: For any natural number `n`, `n = Nat.bodd n * 2 * Nat.div2 n + Nat.abs (Nat.sub n (2 * Nat.div2 n))`.
|
Nat.zero_bits
theorem Nat.zero_bits : Nat.bits 0 = []
The theorem `Nat.zero_bits` states that when the function `Nat.bits` is applied to the natural number 0, it returns an empty list. This corresponds to the binary representation of 0, which does not have any bits.
More concisely: The theorem asserts that the binary representation of natural number 0 is the empty list. (or equivalently, Nat.bits 0 = [] in Lean)
|
Nat.div2_bit
theorem Nat.div2_bit : ∀ (b : Bool) (n : ℕ), (Nat.bit b n).div2 = n
This theorem states that for any boolean `b` and natural number `n`, the result of dividing by 2 (using the `Nat.div2` function which takes the floor of `n/2`) the natural number formed by appending the boolean `b` as a binary digit to `n` (using the `Nat.bit` function) is equal to the original number `n`. In other words, appending a binary digit to a number and then halving effectively removes the appended digit.
More concisely: For any natural number `n` and boolean `b`, `Nat.div2 (Nat.bit0 (Nat.succ n) b) = n`. (Here, `Nat.bit0` is used instead of `Nat.bit` to append the bit at the least significant position.)
|
Nat.bit_decomp
theorem Nat.bit_decomp : ∀ (n : ℕ), Nat.bit n.bodd n.div2 = n
The theorem `Nat.bit_decomp` states that for any natural number `n`, if you take the binary representation of `n`, determine if it's odd or even using the `Nat.bodd` function to get the last digit, divide `n` by 2 using the `Nat.div2` function to get the remaining digits, and then concatenate the last digit and the remaining digits using the `Nat.bit` function, you will get back the original number `n`. In other words, it verifies the correctness of the decomposition of a natural number into its binary representation.
More concisely: For any natural number `n`, the binary representation of `n` obtained by concatenating the last digit of its binary representation (determined by `Nat.bodd`) with the remaining digits (obtained by dividing `n` by 2 using `Nat.div2`) equals `n`.
|
Nat.binaryRec_eq'
theorem Nat.binaryRec_eq' :
∀ {C : ℕ → Sort u_1} {z : C 0} {f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)} (b : Bool) (n : ℕ),
f false 0 z = z ∨ (n = 0 → b = true) → Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)
The theorem `Nat.binaryRec_eq'` in Lean 4 is essentially an improvement of `binaryRec_eq` allowing for a more flexible condition when appending `false` to `0`. It states that for any predicate `C` mapping natural numbers to a certain type, a base case `z` for `0`, a function `f` that applies to a boolean, a natural number, and an instance of `C n` to generate an instance of `C (Nat.bit b n)`, a boolean `b`, and a natural number `n`, if `f false 0 z` equals `z` or `n` equals zero implies `b` equals `true`, then applying `Nat.binaryRec` on the bit representation of the number `n` with base case `z` and function `f`, is equivalent to applying function `f` on `b`, `n`, and the recursive application of `Nat.binaryRec` on `n`.
More concisely: If for a predicate `C` and natural numbers `z` and `n`, `f` satisfies `f false 0 z = z` when `n = 0` and `b = true` if `n = 0` or `n = 0` and `f b (Nat.bit b n) = C (Nat.bit b n)`, then `f b n = C (Nat.binaryRec (Nat.bit b) n z)`.
|
Nat.testBit_bit_succ
theorem Nat.testBit_bit_succ : ∀ (m : ℕ) (b : Bool) (n : ℕ), (Nat.bit b n).testBit m.succ = n.testBit m
This theorem states that for any natural numbers `m` and `n`, and any Boolean `b`, testing the `(m+1)`-th least significant bit of the number obtained by appending the digit `b` to the binary representation of `n`, is the same as testing the `m`-th least significant bit of `n` itself. This property reflects how binary numbers are constructed: adding a new least significant bit shifts the positions of all the other bits.
More concisely: For all natural numbers m, n, and Boolean values b, the (m+1)th least significant bit of the binary representation of n with the digit b appended is equivalent to the mth least significant bit of n.
|
Nat.bitCasesOn_bit
theorem Nat.bitCasesOn_bit :
∀ {C : ℕ → Sort u} (H : (b : Bool) → (n : ℕ) → C (Nat.bit b n)) (b : Bool) (n : ℕ),
(Nat.bit b n).bitCasesOn H = H b n
The theorem `Nat.bitCasesOn_bit` asserts that for any predicate `C` which is a function from natural numbers to some arbitrary type, and for any function `H` which maps a boolean `b` and a natural number `n` to an instance of `C(Nat.bit b n)`, and for any boolean `b` and natural number `n`, applying the `Nat.bitCasesOn` function to `Nat.bit b n` and `H` will always yield the same result as directly applying `H` to `b` and `n`. Essentially, it states that `Nat.bitCasesOn` correctly decomposes any natural number formed by appending a binary digit to another number.
More concisely: For any predicate `C` and function `H`, the evaluation of `H (b, Nat.bit b n)` equals the application of `Nat.bitCasesOn` to `Nat.bit b n` and `H`.
|
Nat.bit1_val
theorem Nat.bit1_val : ∀ (n : ℕ), bit1 n = 2 * n + 1
The theorem `Nat.bit1_val` states that for any natural number `n`, the `bit1` function applied to `n` equals `2 * n + 1`. The `bit1` function here is defined as adding 1 to the double of a given number. Thus, this theorem is simply characterizing the action of the `bit1` function in terms of multiplication and addition on natural numbers.
More concisely: For any natural number `n`, `bit1 (2 * n) = 2 * n + 1`. In Lean, this is expressed as the theorem `Nat.bit1_val : ∀ n : Nat, Bit1 (2 * n) = 2 * n + 1`.
|
Nat.mod_two_of_bodd
theorem Nat.mod_two_of_bodd : ∀ (n : ℕ), n % 2 = bif n.bodd then 1 else 0
This theorem states that for any natural number `n`, the remainder when `n` is divided by 2 is determined by whether `n` is odd or not. Specifically, if `n` is odd (as indicated by the function `Nat.bodd n` returning `true`), then `n` modulo 2 is 1. Otherwise, if `n` is even (i.e., `Nat.bodd n` returns `false`), then `n` modulo 2 is 0. This is essentially the definition of odd and even numbers in terms of division by 2.
More concisely: For any natural number `n`, `n` modulo 2 is 1 if `n` is odd, and 0 if `n` is even.
|
Nat.binaryRec.proof_5
theorem Nat.binaryRec.proof_5 :
∀ {C : ℕ → Sort u_1} (n : ℕ), Nat.bit n.bodd n.div2 = n → C n = C (Nat.bit n.bodd n.div2)
This theorem asserts that for every natural number `n` and for every function `C` from natural numbers to a type, if `n` can be represented as a binary number by appending the binary digit equivalent of whether `n` is odd (`Nat.bodd n`) to the binary representation of the floor division of `n` by 2 (`Nat.div2 n`), then the value of `C` at `n` is the same as the value of `C` at the binary number representation of `n`. In other words, the function `C` is invariant under the operation of binary representation of numbers.
More concisely: For every function `C` and all natural numbers `n`, if `n` is represented in binary as the concatenation of the binary representation of `Nat.div2 n` and the binary digit representing the oddness of `n` (i.e., `Nat.bodd n`), then `C(n) = C(binary_representation_of_n)`.
|
Nat.boddDiv2_eq
theorem Nat.boddDiv2_eq : ∀ (n : ℕ), n.boddDiv2 = (n.bodd, n.div2)
The theorem `Nat.boddDiv2_eq` states that for any natural number `n`, the function `Nat.boddDiv2` on `n` returns a pair: the first element of the pair is the result of the function `Nat.bodd` on `n` (which checks if `n` is odd), and the second element is the result of the function `Nat.div2` on `n` (which calculates the greatest integer less than or equal to `n/2`). In other words, the `Nat.boddDiv2` function simultaneously calculates and returns whether a number is odd and its integer division by 2.
More concisely: For any natural number `n`, the function `Nat.boddDiv2` returns a pair `(Nat.bodd n, Nat.div2 n)`.
|
Nat.shiftLeft'_false
theorem Nat.shiftLeft'_false : ∀ {m : ℕ} (n : ℕ), Nat.shiftLeft' false m n = m <<< n
The theorem `Nat.shiftLeft'_false` states that for any given natural numbers `m` and `n`, the function `Nat.shiftLeft'` with `false` as the first argument, `m` as the second argument, and `n` as the third argument, is equivalent to the left bitwise shift of `m` by `n` places. In other words, shifting `m` left `n` times while adding a `false` bit (i.e., a zero bit) each time as the least significant bit results in the same value as performing a bitwise left shift of `m` by `n` places.
More concisely: For all natural numbers m and n, the function Nat.shiftLeft' (false) m n equals the bitwise left shift of m by n places.
|
Nat.div2_val
theorem Nat.div2_val : ∀ (n : ℕ), n.div2 = n / 2
This theorem states that for every natural number `n`, the value of the function `Nat.div2 n` is equal to the floor of `n/2`. In other words, `Nat.div2 n` gives the greatest integer that is less than or equal to `n/2`. This theorem provides a formal proof in Lean 4 that this function indeed behaves as expected based on its definition.
More concisely: For every natural number `n`, `Nat.div2 n` equals the floor of `n/2`.
|
Nat.bodd_bit
theorem Nat.bodd_bit : ∀ (b : Bool) (n : ℕ), (Nat.bit b n).bodd = b
This theorem, `Nat.bodd_bit`, states that for any Boolean value `b` and any natural number `n`, the result of computing the binary oddness (`Nat.bodd`) of the number obtained by appending `b` as the least significant bit to the binary representation of `n` (`Nat.bit b n`) is equal to `b` itself. In other words, the least significant bit of a binary number determines its oddness: if the bit is `1` (true), the number is odd; if the bit is `0` (false), the number is even.
More concisely: For any Boolean value $b$ and natural number $n$, the binary oddness of $n$ with its least significant bit set to $b$ equals $b$.
|
Nat.bits_append_bit
theorem Nat.bits_append_bit : ∀ (n : ℕ) (b : Bool), (n = 0 → b = true) → (Nat.bit b n).bits = b :: n.bits
The theorem `Nat.bits_append_bit` states that for any natural number `n` and any boolean `b`, if `n` is zero implies `b` is true, then the binary representation of the natural number obtained by appending `b` to `n` (using the `Nat.bit` function) is equal to the list that has `b` as the head followed by the binary representation of `n` (using the `Nat.bits` function). In other words, it asserts that the `Nat.bits` function correctly reflects the addition of a binary digit to a natural number using the `Nat.bit` function, assuming that when the natural number is zero, the added digit is one.
More concisely: For any natural number `n` and boolean `b`, if `n = 0` implies `b = true`, then `Nat.bit (Nat.succ n) b` equals the cons of `b` with the list `Nat.bits n`.
|
Nat.bodd_add
theorem Nat.bodd_add : ∀ (m n : ℕ), (m + n).bodd = xor m.bodd n.bodd
The theorem `Nat.bodd_add` states that for all natural numbers `m` and `n`, the parity (whether it is odd or even) of the sum `m + n` is the Boolean exclusive or (xor) of the parities of `m` and `n`. In other words, the sum of two numbers is odd if and only if exactly one of them is odd.
More concisely: The parity of the sum of natural numbers is the XOR of their individual parities.
|
Nat.bit0_val
theorem Nat.bit0_val : ∀ (n : ℕ), bit0 n = 2 * n
The theorem `Nat.bit0_val` states that for all natural numbers `n`, applying the function `bit0` to `n` is equivalent to multiplying `n` by 2. The `bit0` function, given a numerical input, simply adds the input to itself, thereby effectively doubling its value.
More concisely: For all natural numbers n, bit0(n) = 2 * n.
|
Nat.binaryRec_zero
theorem Nat.binaryRec_zero :
∀ {C : ℕ → Sort u} (z : C 0) (f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)), Nat.binaryRec z f 0 = z
The theorem `Nat.binaryRec_zero` states that for any type function `C` from natural numbers to some arbitrary sort `u`, and for any inputs `z` of type `C 0` and `f` of type `(b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)`, the result of applying the binary recursion function `Nat.binaryRec` to `z`, `f`, and `0` is equal to `z`. Essentially, this is saying that the base case of this binary recursion, when the input natural number is zero, is exactly the value `z`.
More concisely: For any function `C : ℕ → Sort u` and values `z : C 0` and `f : ∀ (b : Bool), ℕ → C → C`, `Nat.binaryRec z f 0 = z`.
|
Nat.binaryRec_eq
theorem Nat.binaryRec_eq :
∀ {C : ℕ → Sort u} {z : C 0} {f : (b : Bool) → (n : ℕ) → C n → C (Nat.bit b n)},
f false 0 z = z → ∀ (b : Bool) (n : ℕ), Nat.binaryRec z f (Nat.bit b n) = f b n (Nat.binaryRec z f n)
The theorem `Nat.binaryRec_eq` states that for any predicate `C` over natural numbers, given an instance `z` of `C 0` and a function `f` that constructs an instance of `C (Nat.bit b n)` from `b` (a boolean), `n` (a natural number), and an instance of `C n`, if `f false 0 z` equals `z`, then for any boolean `b` and natural number `n`, applying the binary recursion of `C` to the binary number formed by appending `b` to `n` equals applying `f` to `b`, `n`, and the result of the binary recursion of `C` on `n`. This theorem essentially provides a condition under which the binary recursion function behaves as expected with respect to the function `f`.
More concisely: If for all natural numbers `n` and booleans `b`, if `C 0` holds for some instance `z` and `C (Nat.bit b (Nat.succ n)) = f b (Nat.bit b n) (C n)`, then `C (Nat.bit b (Nat.succ (Nat.succ n))) = f b (Nat.succ n) (C (Nat.bit b (Nat.succ n)))`.
|
Nat.bodd_mul
theorem Nat.bodd_mul : ∀ (m n : ℕ), (m * n).bodd = (m.bodd && n.bodd)
The theorem `Nat.bodd_mul` states that for any two natural numbers `m` and `n`, the binary oddity (being odd or even) of their product `m * n` is equivalent to the logical conjunction (AND) of the binary oddities of `m` and `n` individually. In other words, the product of two natural numbers is odd if and only if both numbers are odd.
More concisely: The theorem `Nat.bodd_mul` asserts that for all natural numbers m and n, m * n is odd if and only if both m and n are odd.
|