[Merged by Bors] - refactor: replace Bitvec with Std.BitVec by mhk119 · Pull Request #5920 · leanprover-community/mathlib4

mhk119 · 2023-07-15T03:02:54Z

re-adding definitions and theorems about bitvectors that mathlib has for Bitvec to the new Std.BitVec type, and getting rid of the former.

In std, the choice was made to define ult (unsigned less than) and related comparisons as Bool-valued, where the corresponding defs for Bitvec in mathlib are Prop-valued. Std does not have definitions for the respective greater-equal or greater-than comparisons, so we add those here, but we choose to be consistent with std and make them Bool-valued as well, breaking with the old API.

depends on: [Merged by Bors] - feat: prove an upper bound on bitwise operations #8598

EDIT (alexkeizer):
Since opening this PR, substantial parts of the proposed refactor have been upstreamed to std.
This PR has thus changed its goal from:

Redefine BitVec w as Fin (2^w) instead of Vector Bool w because the Fin representation is computationally more efficient and allows users to reuse existing theorems on Fin or Nat easily.

Co-authored-by: Scott Morrison <scott@tqft.net>

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

…mathlib4 into bitvectors

Mathlib/Data/Bitvec/Lemmas.lean

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser · 2023-11-29T12:22:13Z

bors merge

This looks good to go now; thanks for splitting out all the other smaller PRs to make this a manageable size!

re-adding definitions and theorems about bitvectors that mathlib has for `Bitvec` to the new `Std.BitVec` type, and getting rid of the former. In std, the choice was made to define ult (unsigned less than) and related comparisons as `Bool`-valued, where the corresponding defs for `Bitvec` in mathlib are `Prop`-valued. Std does not have definitions for the respective greater-equal or greater-than comparisons, so we add those here, but we choose to be consistent with std and make them `Bool`-valued as well, breaking with the old API. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Alex Keizer <alex@keizer.dev> Co-authored-by: Harun Khan <harun19@stanford.edu>

mathlib-bors · 2023-11-29T12:53:13Z

Pull request successfully merged into master.

Build succeeded:

alexkeizer · 2023-11-29T13:42:07Z

Yay, we finally made it! Thanks everyone for helping out along the way!

tobiasgrosser · 2023-11-29T14:10:55Z

Thank you all, indeed!

mhk119 · 2023-11-30T01:02:58Z

Thanks everyone for your hard work! This is amazing.

This matches the name of `Std.BitVec`. Performing the rename was deliberately left out of #5920, to avoid creating a break in the git history.

linesthatinterlace · 2023-12-01T10:22:03Z

Congratulations!

These were factored out of #5920 as they seem generally useful.

These are generally useful and split out of #5920. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

re-adding definitions and theorems about bitvectors that mathlib has for `Bitvec` to the new `Std.BitVec` type, and getting rid of the former. In std, the choice was made to define ult (unsigned less than) and related comparisons as `Bool`-valued, where the corresponding defs for `Bitvec` in mathlib are `Prop`-valued. Std does not have definitions for the respective greater-equal or greater-than comparisons, so we add those here, but we choose to be consistent with std and make them `Bool`-valued as well, breaking with the old API. Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Alex Keizer <alex@keizer.dev> Co-authored-by: Harun Khan <harun19@stanford.edu>

mhk119 and others added 30 commits June 11, 2023 20:23

doc(Data/Nat/Bitblast): initial commit

1ccf17f

fixed linting issues

4ed06e5

fixed intro

055749d

Update Mathlib/Data/Nat/Bitblast.lean

4868ef5

Co-authored-by: Scott Morrison <scott@tqft.net>

Update Mathlib/Data/Nat/Bitblast.lean

869e882

Co-authored-by: Scott Morrison <scott@tqft.net>

Update Mathlib/Data/Nat/Bitblast.lean

bcaea2d

Co-authored-by: Scott Morrison <scott@tqft.net>

Update Mathlib/Data/Nat/Bitblast.lean

1d8a3be

Co-authored-by: Scott Morrison <scott@tqft.net>

fixed docstrings

fbdc3a2

re-ordered things and resolved Bool namespace

c140963

deleted bitblast.lean

a7515c9

merged recent work into bitwise.lean

b211ed2

Update Mathlib/Data/Nat/Bitwise.lean

068e96b

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

d3b5b04

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

4a506c5

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

e9cf563

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

7f85934

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

cb5a252

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

fd82137

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

3fb9204

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

0b2d9e8

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

78ca18b

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

eaf1d28

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

ec57592

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Update Mathlib/Data/Nat/Bitwise.lean

2c2d8ec

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

fixed some errors due to naming

4508848

moved some lemmas into other files

835e7aa

moved two_pow_succ

74b3eb1

Merge branch 'master' into bitvectors

2516600

changed definition of toNat

ef71db1

Merge branch 'bitvectors' of https://github.com/leanprover-community/…

1dfd73f

…mathlib4 into bitvectors

tobiasgrosser added 2 commits November 25, 2023 23:21

Shorten proof

037b756

Shorten even further

22c534b

eric-wieser reviewed Nov 25, 2023

View reviewed changes

Mathlib/Data/Bitvec/Lemmas.lean Outdated Show resolved Hide resolved

Proof golf toNat_injective

6401e71

eric-wieser reviewed Nov 26, 2023

View reviewed changes

Mathlib/Data/Bitvec/Lemmas.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 26, 2023

View reviewed changes

Mathlib/Data/Bitvec/Lemmas.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 26, 2023

View reviewed changes

Mathlib/Data/Bitvec/Lemmas.lean Show resolved Hide resolved

tobiasgrosser and others added 5 commits November 26, 2023 14:23

Update Mathlib/Data/Bitvec/Lemmas.lean

9f95785

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Mathlib/Data/Bitvec/Lemmas.lean

7c10df8

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Whitespace

0bdb762

Fix noaligns

fee5ddc

Explicit args

1ce69cc

github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Nov 29, 2023

mathlib-bors bot changed the title ~~refactor: replace Bitvec with Std.BitVec~~ [Merged by Bors] - refactor: replace Bitvec with Std.BitVec Nov 29, 2023

mathlib-bors bot closed this Nov 29, 2023

mathlib-bors bot deleted the Bitvecnew branch November 29, 2023 12:53

eric-wieser mentioned this pull request Nov 30, 2023

[Merged by Bors] - chore: rename Data.Bitvec to Data.BitVec #8710

Closed

mathlib-bors bot pushed a commit that referenced this pull request Nov 30, 2023

chore: rename Data.Bitvec to Data.BitVec (#8710)

7816795

This matches the name of `Std.BitVec`. Performing the rename was deliberately left out of #5920, to avoid creating a break in the git history.

grunweg pushed a commit that referenced this pull request Dec 15, 2023

feat: theorems about power of twos (#8547)

5c32dea

These were factored out of #5920 as they seem generally useful.

awueth pushed a commit that referenced this pull request Dec 19, 2023

feat: theorems about power of twos (#8547)

44cebda

These were factored out of #5920 as they seem generally useful.

awueth pushed a commit that referenced this pull request Dec 19, 2023

feat: add two power-of-two theorems to bitwise (#8558)

91d855f

These are generally useful and split out of #5920. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor: replace Bitvec with Std.BitVec#5920

[Merged by Bors] - refactor: replace Bitvec with Std.BitVec#5920
mhk119 wants to merge 209 commits intomasterfrom
Bitvecnew

mhk119 commented Jul 15, 2023 •

edited by eric-wieser

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented Nov 29, 2023

Uh oh!

mathlib-bors bot commented Nov 29, 2023

Uh oh!

alexkeizer commented Nov 29, 2023

Uh oh!

tobiasgrosser commented Nov 29, 2023

Uh oh!

mhk119 commented Nov 30, 2023

Uh oh!

linesthatinterlace commented Dec 1, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

Conversation

mhk119 commented Jul 15, 2023 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser commented Nov 29, 2023

Uh oh!

mathlib-bors bot commented Nov 29, 2023

Uh oh!

alexkeizer commented Nov 29, 2023

Uh oh!

tobiasgrosser commented Nov 29, 2023

Uh oh!

mhk119 commented Nov 30, 2023

Uh oh!

linesthatinterlace commented Dec 1, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

8 participants

mhk119 commented Jul 15, 2023 •

edited by eric-wieser

Loading