Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: teach bv_normalize to rewrite subtractions to additions #6890

Merged
merged 2 commits into from
Feb 1, 2025

Conversation

vlad902
Copy link
Contributor

@vlad902 vlad902 commented Jan 31, 2025

This PR teaches bv_normalize to replace subtractions on one side of an equality with an addition on the other side, this re-write eliminates a not + addition in the normalized form so it is easier on the solver.

Note that I also make a point to normalize (1 + ~~~x) to (~~~x + 1) to limit the amount of boilerplate symmetry theorems we require.

This PR teaches bv_normalize to replace subtractions on one side of an
equality with an addition on the other side, this re-write eliminates a
not + addition in the normalized form so it is easier on the solver.

Note that I also make a point to normalize (1 + ~~~x) to (~~~x + 1) to
limit the amount of boilerplate symmetry theorems we require.
@vlad902
Copy link
Contributor Author

vlad902 commented Jan 31, 2025

changelog-library

@github-actions github-actions bot added changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Jan 31, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a3f7d445932f8f183418ff53743e23ffa7f4705a --onto ad48761032c5750e51289f3885967c1b6f8edde5. (2025-01-31 17:47:14)

@vlad902 vlad902 requested a review from hargoniX February 1, 2025 08:03
@hargoniX hargoniX added this pull request to the merge queue Feb 1, 2025
Merged via the queue into leanprover:master with commit ca96ea3 Feb 1, 2025
14 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants