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.

Sign up for GitHub

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

[Merged by Bors] - feat: show that BitVec is a commutative ring #8711

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: show that BitVec is a commutative ring #8711

Changes from 1 commit
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
9e28e30
feat: show that `BitVec` is a commutative ring
alexkeizer Nov 29, 2023
333b404
add toFin_injective
alexkeizer Nov 29, 2023
70fe10c
reverse direction of `ofFin_foo_ofFin`
alexkeizer Nov 29, 2023
d0f31ee
WIP
alexkeizer Nov 29, 2023
3748021
rename lemma to reflect to changed order
alexkeizer Nov 29, 2023
10bf420
reorder Injectivivity proofs
alexkeizer Nov 29, 2023
bbc3adc
refactor distributivity lemmas
alexkeizer Nov 29, 2023
86003cd
remove extraneous arguments
alexkeizer Nov 29, 2023
d815ab7
add `ofFin_zero`/`_one`
alexkeizer Nov 29, 2023
e7b44ad
add `toFin_zero`/`_one`
alexkeizer Nov 29, 2023
365b86a
refactor `SMul`, `Pow` and `Cast` instances
alexkeizer Nov 29, 2023
f219560
move instances to Defs file, use theorems by name
alexkeizer Nov 29, 2023
2a760f4
Remove some simp lemmas
tobiasgrosser Nov 30, 2023
9b53ed9
Update Mathlib/Data/Bitvec/Lemmas.lean
tobiasgrosser Nov 30, 2023
4db1611
tidy
eric-wieser Nov 30, 2023
698608e
Fix proofs
alexkeizer Dec 1, 2023
772eba5
Fix more proofs
alexkeizer Dec 1, 2023
ee150e9
WIP: use `ofInt` as `IntCast` instance
alexkeizer Dec 1, 2023
57a52e1
finish `ofFin_intCast` proof
alexkeizer Dec 1, 2023
ee86242
WIP: fix `ofFin_intCast`
alexkeizer Dec 11, 2023
8367843
Update Mathlib/Data/BitVec/Lemmas.lean
tobiasgrosser Dec 11, 2023
61c9b26
Reduce PR to CommSemiring
alexkeizer Dec 15, 2023
5871779
Formatting
alexkeizer Dec 15, 2023
4e381cf
Update Mathlib/Data/BitVec/Lemmas.lean
tobiasgrosser Dec 15, 2023
98a9e96
Add comment
tobiasgrosser Dec 15, 2023
b8c92cb
Drop unused lemma
tobiasgrosser Dec 15, 2023
affc6d4
Update Mathlib/Data/BitVec/Lemmas.lean
alexkeizer Dec 15, 2023
a09afb8
linarith
tobiasgrosser Dec 15, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Mathlib/Data/BitVec/Lemmas.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -203,6 +203,8 @@ end
### `IntCast`
-/

-- Either of these follows trivially fromt he other. Which one to
-- prove is not yet clear.
alexkeizer marked this conversation as resolved.
Show resolved Hide resolved
proof_wanted ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = z

proof_wanted toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z
Expand Down
Loading