feat: make Bool.xor a standalone definition#13995
Draft
linesthatinterlace wants to merge 5 commits into
Draft
Conversation
Previously `Bool.xor` was an `abbrev` for `bne`. Make it a semireducible def with its own simp lemma set (early lemmas in SimpLemmas, the rest in Bool). Move the `^^` notation and definition to Prelude, and fix the `or` recommended_spelling target. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Use the `xor_*` lemmas (`xor_false`, `xor_left_inj`, `xor_assoc`, …) where proofs previously relied on `xor` being defeq to `bne`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
xor is now opaque; dedicated grind propagators will replace the unfold. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Make `Bool.xor` `@[inline]` and define it with a direct `match`, trim its docstring, and drop the now-redundant re-exports. Round out the xor/bne simp normal forms: `@[simp]` on `xor_eq_false_iff` and new `eq_not_self_*`/`eq_not_*_self` lemmas, with matching `bool_simp` coverage. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Add `propagateBoolXorUp`/`propagateBoolXorDown` so `grind` reasons about `Bool.xor` directly on the Bool equivalence graph, rather than relying on it being unfolded to `bne`. Propagates truth values from either argument, and the `a ≡ b ⟹ false` / `a ≠ b ⟹ true` equivalence facts in both directions, with supporting lemmas in `Init.Grind.Lemmas`. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Contributor
Author
|
Opening this as a draft for visibility alongside RFC #13994. I'd like to hold it for review until the RFC has had feedback, since the design decision — in particular the change to the |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR makes
Bool.xora standalone definition instead of a reducible abbreviation forbne, so thatsimpandgrindtreat exclusive-or as an operation in its own right rather than unfolding it away. It adds dedicatedxorsimplemmas andgrindpropagators, giving predictable xor-shaped normal forms and lettinggrindclose goals involving^^that previously needed manual rewriting throughbne.Bool.xoris now defined by a branchingmatchon its first argument, with the definition and^^notation living inInit.PreludeandInit.Notation. Thexorlemmas inInit.Data.Boolare restated directly in terms ofxorrather than asbnewrappers; newsimpnormal-form lemmas andStd.Commutative,Std.Associative, andStd.LawfulIdentityinstances are added; andgrindpropagators forBool.xorare registered, with supporting lemmas inInit.Grind.Lemmas. TheBitVecbitblasting andStd.SatAIG code is adapted to the new normal forms.This implements RFC #13994.
AI disclosure: the
grindpropagators (propagateBoolXorUp/propagateBoolXorDowninLean.Meta.Tactic.Grind.Propagate) and their supporting lemmas inInit.Grind.Lemmaswere authored by Claude (Claude Code) and reviewed by me; theBool.xordefinition change and thesimplemma set are my own work.