English
The bitwise operation of a and not b corresponds to the ldiff operator: (a ∧ ¬b) = ldiff(a,b).
Русский
Побитовая разность определяется как a ∧ ¬b, что совпадает с оператором ldiff: (a ∧ ¬b) = ldiff(a,b).
LaTeX
$$$$ (a \land \lnot b) = \mathrm{ldiff}(a,b) \quad \text{for } a,b \in \{0,1\}. $$$$
Lean4
theorem bitwise_diff : (bitwise fun a b => a && not b) = ldiff :=
by
funext m n
rcases m with m | m <;> rcases n with n | n <;>
try { rfl
} <;>
simp only [bitwise, natBitwise, Bool.not_false, cond_false, cond_true, Nat.ldiff, Bool.and_true, negSucc.injEq,
Bool.and_false, Bool.not_true, ldiff]
· congr
simp
· congr
simp
· rw [Nat.bitwise_swap, Function.swap]
congr
funext x y
cases x <;> cases y <;>
rfl
-- Porting note: Was `bitwise_tac` in mathlib
