English
If f is commutative on booleans and satisfies f(false,false)=false, then bitwise f is commutative: bitwise f n m = bitwise f m n for all n,m.
Русский
Если f — коммутативная операция над булевыми и выполняется f(false,false)=false, то bitwise f тоже коммутативна: bitwise f n m = bitwise f m n для всех n,m.
LaTeX
$$$ (\forall b,b',\ f(b,b')=f(b',b)) \Rightarrow \forall n,m,\ bitwise f n m = bitwise f m n $$$
Lean4
/-- If `f` is a commutative operation on bools such that `f false false = false`, then `bitwise f`
is also commutative. -/
theorem bitwise_comm {f : Bool → Bool → Bool} (hf : ∀ b b', f b b' = f b' b) (n m : ℕ) :
bitwise f n m = bitwise f m n :=
suffices bitwise f = swap (bitwise f) by conv_lhs => rw [this]
calc
bitwise f = bitwise (swap f) := congr_arg _ <| funext fun _ => funext <| hf _
_ = swap (bitwise f) := bitwise_swap
