English
An alternative form of bitwise bit: for all f, a, m, b, n, with assumptions m = 0 → a = true and n = 0 → b = true, bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n).
Русский
Алтернативная формула битовой операции: для всех f, a, m, b, n, при условии m = 0 → a = true и n = 0 → b = true, выполняется bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n).
LaTeX
$$$$ \\forall f\\ a\\ m\\ b\\ n:\\ \\bigl(m = 0 \\to a = \\text{true}\\bigr) \\to \\bigl(n = 0 \\to b = \\text{true}\\bigr) \\Rightarrow \\mathrm{bitwise}\\; f\\ (\\mathrm{bit}\\ a\\ m) (\\mathrm{bit}\\ b\\ n) = \\mathrm{bit}\\ (f\\ a\\ b) (\\mathrm{bitwise}\\; f\\ m\\ n) $$$$
Lean4
/-- An alternative for `bitwise_bit` which replaces the `f false false = false` assumption
with assumptions that neither `bit a m` nor `bit b n` are `0`
(albeit, phrased as the implications `m = 0 → a = true` and `n = 0 → b = true`) -/
theorem bitwise_bit' {f : Bool → Bool → Bool} (a : Bool) (m : Nat) (b : Bool) (n : Nat) (ham : m = 0 → a = true)
(hbn : n = 0 → b = true) : bitwise f (bit a m) (bit b n) = bit (f a b) (bitwise f m n) :=
by
conv_lhs => unfold bitwise
rw [← bit_ne_zero_iff] at ham hbn
simp only [ham, hbn, bit_mod_two_eq_one_iff, Bool.decide_coe, ← div2_val, div2_bit, ite_false]
conv_rhs => simp only [bit, two_mul, Bool.cond_eq_ite]
