RFC: Make `Bool.xor` a standalone definition with dedicated `simp` and `grind` support

This RFC proposes replacing Bool.xor's current definition as an abbrev of bne with a directly defined function, promoting it to the Prelude along with the other Boolean operations.

---

Proposal

Bool.xor is currently defined as a reducible abbreviation for bne:

abbrev xor : Bool → Bool → Bool := bne

Because it is a reducible abbreviation, xor is not really a separate operation at all - it is just another name for bne. Since simp lemmas and grind propagators are keyed on a term's head constant, they cannot tell the two apart: a lemma stated about xor is, as far as automation is concerned, a lemma about bne, and any fact about exclusive-or is really being expressed through the bne machinery. What that machinery unfolds to is not simple either - bne x y is !(x == y), where == is the BEq instance derived from DecidableEq, which for Bool bottoms out in Bool.decEq. I propose to make Bool.xor a definition in its own right — standalone and semireducible - with a coherent set of simp lemmas stated directly about xor and grind propagators that understand it.

Concretely, the new definition branches on the first argument:

@[inline] def Bool.xor (x y : Bool) : Bool :=
  match x with
  | false => y
  | true  => y.not

This is purely a change to the logical and elaboration-level treatment of xor; it says nothing about how xor is compiled at runtime. The key idea is that xor and bne are extensionally equal — they compute the same function — but they are not semantically equal, and for elaboration and automation that difference is exactly what matters. I have kept the body branching deliberately, since a branching definition is better suited to reduction in the kernel.

Motivation

The trouble with the abbreviation shows up in two related places.

The first is the simp normal form. Today, any lemma we want about exclusive-or has to be phrased through bne, and the normal form that simp produces for an expression involving ^^ is whatever the bne lemmas happen to give. When you are actually reasoning about xor - in bitvector code, in SAT/AIG bitblasting, or just in ordinary Boolean algebra — that is rarely the form you want. With xor as a real operation, we can give it the normal form that fits how it is used, and xor can carry the obvious Std.Commutative, Std.Associative, and Std.LawfulIdentity instances so that the usual algebraic rearrangement works directly on xor terms rather than on a bne encoding of them.

For example, both of these fail on current master and are closed by simp with this change:

example (a b : Bool) : ((a ^^ b) = a)  ↔ (b = false) := by simp
example (a b : Bool) : ((a ^^ b) = !a) ↔ (b = true)  := by simp

The second is grind. Because grind only ever sees bne, it has no dedicated understanding of exclusive-or, and cannot propagate the facts that make xor reasoning cheap: that fixing either argument turns x ^^ y into the other argument or its negation, that equal arguments make it false and distinct arguments make it true, and the converses going downward. Making Bool.xor standalone lets us register propagators for it, so grind reasons about xor congruence-closure-style instead of unfolding it away. For example, both of these fail on current master and are closed by grind with this change:

example (f : Bool → Nat) (a b : Bool) : f (a ^^ b) = 0 → a = true  → f (!b) = 0 := by grind
example (f : Bool → Nat) (a b : Bool) : f (a ^^ b) = 0 → a = false → f b    = 0 := by grind

User Experience

Users gain predictable, xor-centric normal forms when simplifying Boolean expressions, and grind becomes able to discharge goals that mix xor with equality and negation without the user having to manually rewrite through bne. For most users the change is invisible until they reach for it; for anyone whose proofs genuinely involve exclusive-or, the automation simply does more.

The honest cost is that changing a simp normal form is observable downstream. Proofs that currently rely on xor unfolding to bne, or on the present bne-shaped normal form, may need small adjustments. I think this is worth it, and it is exactly the kind of trade-off I would like feedback on before the implementation lands.

Beneficiaries

The clearest beneficiaries are projects doing Boolean, bitvector, and SAT-style reasoning, where exclusive-or is a primitive rather than an afterthought - this includes Lean's own Std.Sat AIG and BitVec bitblasting code, both of which this work already touches. More broadly, anyone proving facts about Bool benefits from xor behaving as the distinct operation people already take it to be, and from grind handling it.

Maintainability

I think this is a simplification rather than a complication. At the moment xor lemmas are either restated in terms of bne or implemented as thin wrappers around bne lemmas, which means the two operations' lemma sets are entangled even though users think of them as distinct. The entanglement also leaks the other way: a stray bne reduction during simplification can leave an awkward, hard-to-read goal that a user reasoning about xor did not ask for. Giving xor its own definition lets its lemmas live as xor lemmas, stated and proved on their own terms, and keeps the bne and xor developments cleanly separated.

Relationship to #10835

This is closely related to, but separate from, the accepted RFC #10835 (non-branching Bool implementations for not, xor, and toNat). That RFC is about the compiled runtime representation; this one is about the logical and elaboration-level treatment. The two interact in a useful direction: you can only attach a dedicated compiled implementation to a real constant, not to a reducible alias, so making Bool.xor a standalone definition is a natural prerequisite for the non-branching compilation that #10835 asks for. I see this RFC as a natural enabler for #10835, while standing on its own for the simp and grind benefits described above. With Bool.xor available as a real constant, what remains for #10835 is essentially providing the non-branching compiled implementation itself.

Alternatives considered

The most obvious lighter-touch alternative is to leave Bool.xor as an abbreviation for bne and simply improve the simp and grind story for bne instead. I do not think this works, for three reasons.

First, while xor is an abbreviation there is no separate xor to improve. simp and grind operate on terms, and the ^^ notation is erased to bne before either tactic runs, so "better lemmas for bne" and "better lemmas for xor" are the same lemmas on the same term. The lighter option cannot give xor and bne different treatment, but different treatment is exactly what is wanted: the bne/≠ shape is the right normal form when reasoning about equality, whereas the xor shape is the right one for Boolean-algebra, bitvector, and SAT reasoning. One term can only have one normal form; two distinct normal forms require two distinct constants.

Second, the same erasure blocks grind. Its propagators are keyed on the head constant, so as long as xor and bne share a head they must share propagation behaviour; there is no way to register xor-specific propagators without a distinct Bool.xor constant.

Third, the lighter option sits awkwardly with the accepted RFC #10835, which calls for xor to be compiled to non-branching code. The natural way to give xor its own compiled implementation is to attach it to a real Bool.xor constant, which a reducible alias for bne (itself routing through the branching Bool.decEq) does not provide. So a standalone definition looks less like unnecessary complexity and more like a sensible step towards that goal as well.

Implementation status

I have a working branch implementing all of the above: the standalone definition, the simp lemma set, and the grind propagators, with tests. I intend to open it as a draft PR linked to this RFC for visibility, holding it for review until the design here has had feedback.

Start with the proposed Bool.xor definition and the existing simp and grind behavior described in the RFC. Review the working branch and its tests, then compare the stated Bool, bitvector, and SAT examples. Done means the standalone definition, dedicated simp lemmas, grind propagators, and tests are in place after the design receives feedback.