Upstreaming bit, div2, bodd and establishing binary recursion.#1737
Open
linesthatinterlace wants to merge 17 commits intoleanprover-community:mainfrom
Open
Upstreaming bit, div2, bodd and establishing binary recursion.#1737linesthatinterlace wants to merge 17 commits intoleanprover-community:mainfrom
bit, div2, bodd and establishing binary recursion.#1737linesthatinterlace wants to merge 17 commits intoleanprover-community:mainfrom
Conversation
github-actions
bot
added
the
awaiting-review
Add bit arithmetic lemmas (bit_false, bit_true, bit_add, bit_add_bit), complete the leastBits/ofLeastBits section with simp lemmas, inverse proofs, injectivity, and the connection between bits and leastBits via bits_eq_leastBits_elim. Remove grind attributes from bodd_val, div2_val, bit_val to prevent grind from escaping into arithmetic. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Rename bits → bitsList, ofBits → ofBitsList, leastBits → leastBitsList, ofLeastBits → ofLeastBitsList to avoid clashes with existing Nat.ofBits. Add testBit lemmas for bitsList/ofBitsList, getElem_bitsList, bitsList_eq_ofFn_testBit. Sketch toBitVec, toLeastBitVec, ofBitVec, ofLeastBitVec definitions. Remove grind attributes from _val lemmas. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Change binaryElim's bit callback from Nat → α → α to Bool → α → α, since only n.bodd is ever used. This simplifies all binaryElim-based definitions. Add binaryElim_bit/binaryElim_bit_apply showing binaryElim 0 1 bit = id. Remove BitVec sketches for now. Tidy docstrings. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
fgdorais
reviewed
Mar 27, 2026
AlexeyMilovanov
left a comment
AlexeyMilovanov
left a comment
There was a problem hiding this comment.
The CI is currently failing, but I verified locally that these suggestions fix it. I think it's just the strict simpNF linter catching these 6 lemmas. With @[simp] removed here, both lake build and lake lint pass perfectly
…ies into binary_rewrite
Co-authored-by: Alexey Milovanov <almas239@gmail.com>
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Mar 30, 2026
Collaborator
|
I think we could use this opportunity to change |
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 1, 2026
Contributor
Author
|
I would be fine with changing |
Contributor
Author
|
(I note by the way that we don't have the following inductive definitions. I am not proposing to add them and it isn't clear they would be suitable in batteries! However, I could certainly imagine Nat.Odd and Nat.Even existing.) |
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 1, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 1, 2026
mathlib-nightly-testing bot
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Apr 2, 2026
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
3 participants
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 aims to produce a cleanly structured characterisation of
bodd,div2andbit, and use them to define a form of binary induction that is clean and easy to work with.