feat: make xor semireducible

[fgdorais]

Stemmed from the discussion at #464.

Making xor semireducible makes it so that xor and bne can have distinct simp normal forms. For example, with the changes in this PR xor (!x) (!y && x) = true simplifies to ¬(x = false ↔ y = false ∧ x = true) instead of ¬(!x) = (!y && x).

[joehendrix]

I'm supportive of making this distinction between bne and xor, but neither normal form looks great to me.

What's the intuition behind why the new normal form is good?

[fgdorais]

To clarify the example, this simp only applies when xor is used in a propositional context (i.e. _ = true). The same applies for and, or, not. These don't trigger when used in a Bool expression. For example, xor (!x) (!y) = z simps to xor x y = z but not further.

The problem with bne is that generic bne rules trigger, so bne always simplifies to Ne if there is a LawfulBEq instance available. That makes total sense for most uses of bne but it doesn't make much sense for xor.

This is related to some core issues like leanprover/lean4#2038

[joehendrix]

How about we also add a Xor instance for Bool so the ^^^ notation works?

[fgdorais]

Core defines notations && and || for and and or. An ^^^ instance would be unusual, I'd rather have a ^^ notation for xor.

[joehendrix]

Thanks for the reference to SimpLemmas. I tried out removing the simp attributes, but that affects other code negatively.

I may be overthinking, but perhaps we should define the 3-character operations over Bool and make a distinction in the simp normal forms for the 2-character and 3-character connectives (e.g., && vs &&&):

The two character connectives are logical operations and can reduce to propositional reasoning. These should be preferred in defining predicates (e.g. for List.filter).

The three character connectives are data operations and will never reduce to Prop connectives. These should be preferred in code for building Boolean circuits or otherwise encoding logic.

[fgdorais]

Another way would be to use Bool.asProp instead of _ = true for the coercion Bool to Prop. lean4#2060

[fgdorais]

@joehendrix Gentle ping! If you find some time to come back to this PR, I have a current project that needs this.

[joehendrix]

@fgdorais Sorry for the silence. I think with all the upstreaming going on, there's a lot of risk with creating conflicts with the next version.

The other thing I'm a bit concerned with this is that the existing xor simp rules are essentially doing double duty as bne simp rules with Bool.

I'm working on an overhaul of the Bool/Prop normal forms with the focus on ensuring Lean Init, Std, and Mathlib all share the same Boolean normal forms. The files that I plan to move from Std to Lean Init are here while the current test code is here.

I should have a draft PR to Lean 4 within a day or two. Once that's in; then I think xor could potentially become semi-reducible since bne will not being relying on xor simp rules.

[fgdorais]

moved to core