English
Let bitwise be a binary Boolean operation. For every integers m, n and natural k, the k-th bit of bitwise f applied to m and n equals applying f to the k-th bits of m and n respectively.
Русский
Пусть побитовая операция bitwise f является бинарной операцией над булевыми значениями. Для любых целых чисел m, n и натурального k выполняется равенство: k-й бит результата bitwise f m n равен f(k-й бит m, k-й бит n).
LaTeX
$$$$\forall f:\,\Bool\to\Bool\to\Bool,\; \forall m,n\in\mathbb{Z},\; \forall k\in\mathbb{N},\; \mathrm{testBit}(\mathrm{bitwise}\, f\, m\, n)\ k = f(\mathrm{testBit}\, m\ k)(\mathrm{testBit}\, n\ k).$$$$
Lean4
@[simp]
theorem testBit_bitwise (f : Bool → Bool → Bool) (m n k) : testBit (bitwise f m n) k = f (testBit m k) (testBit n k) :=
by
cases m <;> cases n <;> simp only [testBit, bitwise, natBitwise]
· by_cases h : f false false <;> simp [h]
· by_cases h : f false true <;> simp [h]
· by_cases h : f true false <;> simp [h]
· by_cases h : f true true <;> simp [h]
