English
If a ⊕ b ⊕ c ≠ 0 then exactly one of the three pairwise XORs dominates in a cyclic sense: b ⊕ c < a or c ⊕ a < b or a ⊕ b < c.
Русский
Если a ⊕ b ⊕ c ≠ 0, то верно одно из трёх неравенств: b ⊕ c < a, или c ⊕ a < b, или a ⊕ b < c.
LaTeX
$$$ a \oplus b \oplus c \neq 0 \Rightarrow (b \oplus c) < a \lor (c \oplus a) < b \lor (a \oplus b) < c $$$
Lean4
theorem xor_trichotomy {a b c : ℕ} (h : a ^^^ b ^^^ c ≠ 0) : b ^^^ c < a ∨ c ^^^ a < b ∨ a ^^^ b < c :=
by
set v := a ^^^ b ^^^ c with hv
have hab : a ^^^ b = c ^^^ v := by rw [Nat.xor_comm c, xor_cancel_right]
have hbc : b ^^^ c = a ^^^ v := by rw [← Nat.xor_assoc, xor_cancel_left]
have hca : c ^^^ a = b ^^^ v := by
rw [hv, Nat.xor_assoc, Nat.xor_comm a, ← Nat.xor_assoc, xor_cancel_left]
-- If `i` is the position of the most significant bit of `v`, then at least one of `a`, `b`, `c`
-- has a one bit at position `i`.
obtain ⟨i, ⟨hi, hi'⟩⟩ := exists_most_significant_bit h
have : testBit a i ∨ testBit b i ∨ testBit c i := by
contrapose! hi
simp_rw [Bool.eq_false_eq_not_eq_true] at hi ⊢
rw [testBit_xor, testBit_xor, hi.1, hi.2.1, hi.2.2]
rfl
-- If, say, `a` has a one bit at position `i`, then `a xor v` has a zero bit at position `i`, but
-- the same bits as `a` in positions greater than `j`, so `a xor v < a`.
obtain h | h | h := this
on_goal 1 => left; rw [hbc]
on_goal 2 => right; left; rw [hca]
on_goal 3 => right; right; rw [hab]
all_goals
refine lt_of_testBit i ?_ h fun j hj => ?_
· rw [testBit_xor, h, hi]
rfl
· simp only [testBit_xor, hi' _ hj, Bool.bne_false]
