Nat.bitwise_bit'
theorem Nat.bitwise_bit' :
∀ {f : Bool → Bool → Bool} (a : Bool) (m : ℕ) (b : Bool) (n : ℕ),
(m = 0 → a = true) →
(n = 0 → b = true) → Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)
This theorem, `Nat.bitwise_bit'`, provides an alternative form for the `bitwise_bit` function in the case where we do not necessarily assume that the bitwise operation of `false` and `false` is `false`. Instead, it is stated under the assumptions that if `m` is `0` then `a` is `true`, and if `n` is `0` then `b` is `true`. In these conditions, the theorem states that applying the bitwise operation `f` on the binary representations `Nat.bit a m` and `Nat.bit b n` is the same as appending the result of `f a b` to the result of the bitwise operation on `m` and `n`, symbolically, `Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)`.
More concisely: Under the assumptions that `m = 0` implies `a = true` and `n = 0` implies `b = true`, the bitwise operation `f` on binary representations `Nat.bit a m` and `Nat.bit b n` is equivalent to appending the result of `f a b` to the result of the bitwise operation on `m` and `n`, i.e., `Nat.bit (f a b) (Nat.bitwise f m n)`.
|
Nat.bitwise_lt
theorem Nat.bitwise_lt : ∀ {f : Bool → Bool → Bool} {x y n : ℕ}, x < 2 ^ n → y < 2 ^ n → Nat.bitwise f x y < 2 ^ n := by
sorry
The theorem `Nat.bitwise_lt` states that for any given Boolean function `f`, and any natural numbers `x`, `y`, and `n`, if `x` and `y` are both less than `2^n`, then the result of applying the `Nat.bitwise` operation with function `f` on `x` and `y` is also less than `2^n`. In other words, if `x` and `y` can both be represented within `n` bits, then the result of any bitwise operation on `x` and `y` will also fit within `n` bits.
More concisely: For any Boolean function `f`, if `x` and `y` are natural numbers less than 2^n, then `(x U<0020> y).to_nat` resulting from applying `Nat.bitwise f x y` is also less than 2^n. (Here, `U<0020>` denotes the unsigned integer representation of the bitwise operation result in Lean, and `to_nat` converts it back to a natural number.)
|
Nat.testBit_eq_inth
theorem Nat.testBit_eq_inth : ∀ (n i : ℕ), n.testBit i = n.bits.getI i
This theorem states that, for any natural numbers `n` and `i`, the `i`-th bit of `n` (obtained using the `testBit` function) is equal to the `i`-th element of the binary representation of `n` (obtained using `n.bits.getI`). Essentially, it connects bit-level operations with operations on lists of binary digits.
More concisely: For any natural number `n` and index `i`, the `i`-th bit of `n` (obtained using `testBit` function) is equivalent to the `i`-th binary digit of `n` (obtained using `n.bits.get`).
|
Nat.bitwise_zero_right
theorem Nat.bitwise_zero_right :
∀ {f : Bool → Bool → Bool} (n : ℕ), Nat.bitwise f n 0 = if f true false = true then n else 0
The theorem `Nat.bitwise_zero_right` states that for any natural number `n` and any Boolean function `f`, applying the function `Nat.bitwise` with `f`, `n`, and `0` is equivalent to checking if `f true false` equals `true`. If `f true false` does equal `true`, then `Nat.bitwise f n 0` results in `n`, otherwise it results in `0`. In short, it establishes an important property of the `Nat.bitwise` function when the second natural number in the operation is zero.
More concisely: The theorem `Nat.bitwise_zero_right` asserts that for all natural numbers `n` and Boolean functions `f`, `Nat.bitwise f n 0` equals `n` if and only if `f true false` equals `true`.
|
Nat.bitwise_comm
theorem Nat.bitwise_comm :
∀ {f : Bool → Bool → Bool},
(∀ (b b' : Bool), f b b' = f b' b) → ∀ (n m : ℕ), Nat.bitwise f n m = Nat.bitwise f m n
This theorem states that given a binary operation `f` on booleans which is commutative and has the property that `f false false = false`, then the function `Nat.bitwise f`, which applies `f` bitwise to two natural numbers `n` and `m`, is also commutative. In other words, `Nat.bitwise f n m` equals `Nat.bitwise f m n` for any two natural numbers `n` and `m` under these conditions on `f`.
More concisely: Given a commutative and idempotent boolean operation `f` with `f false false = false`, the bitwise application `Nat.bitwise f` of this operation on natural numbers is commutative.
|
Nat.bitwise_bit
theorem Nat.bitwise_bit :
∀ {f : Bool → Bool → Bool},
autoParam (f false false = false) _auto✝ →
∀ (a : Bool) (m : ℕ) (b : Bool) (n : ℕ),
Nat.bitwise f (Nat.bit a m) (Nat.bit b n) = Nat.bit (f a b) (Nat.bitwise f m n)
The theorem `Nat.bitwise_bit` states that for any boolean function `f` (with an automatically provided parameter that `f` of two `false` values equals `false`), and for any boolean values `a` and `b` and natural numbers `m` and `n`, the `bitwise` operation of `f` on the bit representation of `m` and `n` with appended bits `a` and `b` respectively, is equal to the bit representation of the `bitwise` operation of `f` on `m` and `n` with appended bit as `f` of `a` and `b`. In other words, it describes a property of the `bitwise` operation in terms of bit extension and boolean functions.
More concisely: For any boolean function `f` and natural numbers `m`, `n` with bit representations `x_m` and `x_n` respectively, and any boolean values `a` and `b`, the bitwise operation of `f` on `x_m` and `x_n` extended with bits `a` and `b` respectively, equals the bitwise operation of `f` on `x_m` and `x_n` extended with the bit `f(a, b)`.
|
Nat.xor_self
theorem Nat.xor_self : ∀ (n : ℕ), n ^^^ n = 0
This theorem states that for any natural number `n`, the exclusive OR (`^^^`) of `n` with itself is always 0. In other words, when you perform an XOR operation on a number with itself, the result is always zero, regardless of the number used. This is a property of the XOR operation and is true for all natural numbers.
More concisely: For all natural numbers n, n ^^^ n = 0.
|
Nat.append_lt
theorem Nat.append_lt : ∀ {x y n m : ℕ}, x < 2 ^ n → y < 2 ^ m → y <<< n ||| x < 2 ^ (n + m)
This theorem, `Nat.append_lt`, states that for any natural numbers `x`, `y`, `n`, and `m`, if `x` is less than 2 to the power of `n` and `y` is less than 2 to the power of `m`, then the left rotation of `y` by `n` bits or the bitwise OR of `x` is less than 2 to the power of (`n` + `m`). This is particularly used in the context of `Std.BitVec.append`, hence the name of the theorem.
More concisely: If `x` is less than 2^n and `y` is less than 2^m, then `x` < 2^(n+m) <= x OR y.
|