[Merged by Bors] - chore: bump Std, changes for leanprover/std4#366 #8700

kim-em · 2023-11-29T07:19:30Z

Notably leanprover-community/batteries#366 changed the definition of testBit (to something equivalent) when upstreaming it, which broke a handful of proofs.

Other conflicting changes in Std, resolved for now by priming the mathlib name:

Std.BitVec.adc: the type was changed from BitVec (n + 1) to Bool × BitVec w
Nat.mul_add_mod: the type was changed from (a * b + c) % b = c % b to (b * a + c) % b = c % b

Zulip thread

This still has some breakages arising from leanprover-community/batteries#366, around testBit. Fixes welcome!

Please see also #8705, which keeps everything, but renames Nat.testBit to Nat.testBit', so for now it can exist alongside Std's Nat.testBit.

alexkeizer · 2023-11-29T13:47:19Z

~~I foresee testBit_bitwise and its corollaries being useful in the near future~~; I'll give fixing them a try

EDIT: I didn't notice the broken lemmas were about Int, rather than Nat, so I retract my statement about foreseeing their usefulness.
In any case, they have been fixed by marking Nat.testBit_bitwise as a simp lemma again (in Mathlib, not upstream), just like it was before being upstreamed.

This fixes the Int.testbit_bitwise proofs

alexkeizer · 2023-11-29T14:26:46Z

All of the previously commented out theorems should now have proper proofs

eric-wieser · 2023-11-29T14:45:35Z

Mathlib/Data/Nat/Bitwise.lean

+theorem zero_land (n : ℕ) : 0 &&& n = 0 := by simp
 #align nat.zero_land Nat.zero_land

-@[simp]
-theorem land_zero (n : ℕ) : n &&& 0 = 0 := by
-  simp only [HAnd.hAnd, AndOp.and, land, bitwise_zero_right, ite_false, Bool.and_false]
+theorem land_zero (n : ℕ) : n &&& 0 = 0 := by simp
 #align nat.land_zero Nat.land_zero

-@[simp]
-theorem zero_lor (n : ℕ) : 0 ||| n = n := by
-  simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_left, ite_true, Bool.or_true]
+theorem zero_lor (n : ℕ) : 0 ||| n = n := by simp
 #align nat.zero_lor Nat.zero_lor

-@[simp]
-theorem lor_zero (n : ℕ) : n ||| 0 = n := by
-  simp only [HOr.hOr, OrOp.or, lor, bitwise_zero_right, ite_true, Bool.or_false]
+theorem lor_zero (n : ℕ) : n ||| 0 = n := by simp
 #align nat.lor_zero Nat.lor_zero


I think these should just be removed, and the aligns changed to drop the l.

Mathlib/Data/Nat/Bitwise.lean

Mathlib/Init/Data/Nat/Bitwise.lean

Mathlib/Data/Num/Lemmas.lean

eric-wieser · 2023-11-29T14:50:36Z

Mathlib/Data/Nat/Bitwise.lean

-/-- Bitwise extensionality: Two numbers agree if they agree at every bit position. -/
-theorem eq_of_testBit_eq {n m : ℕ} (h : ∀ i, testBit n i = testBit m i) : n = m := by
-  induction' n using Nat.binaryRec with b n hn generalizing m
-  · simp only [zero_testBit] at h
-    exact (zero_of_testBit_eq_false fun i => (h i).symm).symm
-  induction' m using Nat.binaryRec with b' m
-  · simp only [zero_testBit] at h
-    exact zero_of_testBit_eq_false h
-  suffices h' : n = m by
-    rw [h', show b = b' by simpa using h 0]
-  exact hn fun i => by convert h (i + 1) using 1 <;> rw [testBit_succ]


This proof looks much nicer to me than the one (for the converse, ne_implies_bit_diff) that landed in Std4 :(.

I guess that is inevitable, since we don't have Nat.binaryRec in std yet (at least, leanprover-community/batteries#314 is still open, and I'm not aware of any alternative PRs)

Co-authored-by: Eric Wieser <[email protected]>

…munity/mathlib4 into bump_std_20231129

eric-wieser · 2023-11-30T16:25:32Z

Mathlib/Data/BitVec/Lemmas.lean


-theorem toNat_append (msbs : BitVec w) (lsbs : BitVec v) :


https://github.com/leanprover/std4/pull/366/files#r1410924581

eric-wieser · 2023-11-30T16:26:06Z

Mathlib/Data/BitVec/Lemmas.lean

@@ -60,14 +50,9 @@ lemma extractLsb_eq {w : ℕ} (hi lo : ℕ) (a : BitVec w) :

 theorem toNat_extractLsb' {i j} {x : BitVec w} :
    (extractLsb' i j x).toNat = x.toNat / 2 ^ i % (2 ^ j) := by
-  simp only [extractLsb', ofNat_eq_mod_two_pow, shiftRight_eq_div_pow]
-
-theorem getLsb_eq_testBit {i} {x : BitVec w} : getLsb x i = x.toNat.testBit i := by


Where did this go?

The RHS is now the definition of getLsb, so this is replaced by unfolding getLsb, no need for a theorem

eric-wieser · 2023-11-30T23:41:11Z

bors merge

I've updated the PR description to summarize some concerns for a follow-up.

Notably leanprover-community/batteries#366 changed the definition of `testBit` (to something equivalent) when upstreaming it, which broke a handful of proofs. Other conflicting changes in Std, resolved for now by priming the mathlib name: * `Std.BitVec.adc`: the type was changed from `BitVec (n + 1)` to `Bool × BitVec w` * `Nat.mul_add_mod`: the type was changed from `(a * b + c) % b = c % b` to `(b * a + c) % b = c % b` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Mathlib.20bump.20for.20.22Operations.20for.20bit.20representation.20of.20.2E.2E.2E.22/near/404801443) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Alex Keizer <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

kim-em · 2023-11-30T23:42:45Z

bors p=10

mathlib-bors · 2023-12-01T00:51:52Z

Pull request successfully merged into master.

Build succeeded:

Notably leanprover-community/batteries#366 changed the definition of `testBit` (to something equivalent) when upstreaming it, which broke a handful of proofs. Other conflicting changes in Std, resolved for now by priming the mathlib name: * `Std.BitVec.adc`: the type was changed from `BitVec (n + 1)` to `Bool × BitVec w` * `Nat.mul_add_mod`: the type was changed from `(a * b + c) % b = c % b` to `(b * a + c) % b = c % b` [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/348111-std4/topic/Mathlib.20bump.20for.20.22Operations.20for.20bit.20representation.20of.20.2E.2E.2E.22/near/404801443) Co-authored-by: Scott Morrison <[email protected]> Co-authored-by: Alex Keizer <[email protected]> Co-authored-by: Eric Wieser <[email protected]>

chore: bump Std, changes for leanprover-community/batteries#366

766c33e

kim-em added help-wanted The author needs attention to resolve issues awaiting-review labels Nov 29, 2023

kim-em added 8 commits November 29, 2023 18:26

revert

9db8667

.

6240309

fix a bit

db5e363

blech

bfc4612

one more

82a3392

comment out broken and unused results

068ccf3

chore: bump Std

c43641c

merge

18e1a0c

kim-em mentioned this pull request Nov 29, 2023

chore: bump Std to include leanprover/std4#366 (alternative to #8700) #8705

Closed

kim-em added 2 commits November 29, 2023 21:10

remove redundant simp lemmas

8b31141

cleanup

2fd0cb4

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 29, 2023

alexkeizer added 3 commits November 29, 2023 13:52

fix: make Nat.testBit_bitwise a simp-lemma again.

5cad514

This fixes the Int.testbit_bitwise proofs

fix castNum_testBit

1a433ef

fix testBit_eq_inth

da0024a

eric-wieser reviewed Nov 29, 2023

View reviewed changes

Mathlib/Data/Nat/Bitwise.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 29, 2023

View reviewed changes

Mathlib/Init/Data/Nat/Bitwise.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Nov 29, 2023

View reviewed changes

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

eric-wieser reviewed Nov 29, 2023

View reviewed changes

Merge branch 'master' into bump_std_20231129

d0245fb

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 29, 2023

eric-wieser and others added 3 commits November 30, 2023 13:33

fixes

85c799e

golf

f4100cf

Apply suggestions from code review

7b6f1a3

Co-authored-by: Eric Wieser <[email protected]>

eric-wieser added 5 commits November 30, 2023 13:47

golf

fcbe2e5

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

a936ad1

…munity/mathlib4 into bump_std_20231129

fix whitespace

c3b7df4

fix name conflict

3e71922

more efficient

e90cfb7

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 30, 2023

restore lemma

8c7c2d9

alexkeizer mentioned this pull request Nov 30, 2023

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

Closed

1 task

Merge remote-tracking branch 'origin/master' into bump_std_20231129

e8952a9

leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 30, 2023

fix breakage in BitVec lemmas

3765c7e

eric-wieser reviewed Nov 30, 2023

View reviewed changes

remove simp from ofNat_toNat'

c731f15

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

mathlib-bors bot changed the title ~~chore: bump Std, changes for leanprover/std4#366~~ [Merged by Bors] - chore: bump Std, changes for leanprover/std4#366 Dec 1, 2023

mathlib-bors bot closed this Dec 1, 2023

mathlib-bors bot deleted the bump_std_20231129 branch December 1, 2023 00:51

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - chore: bump Std, changes for leanprover/std4#366 #8700

[Merged by Bors] - chore: bump Std, changes for leanprover/std4#366 #8700

kim-em commented Nov 29, 2023 •

edited by eric-wieser

Loading

alexkeizer commented Nov 29, 2023 •

edited

Loading

alexkeizer commented Nov 29, 2023

eric-wieser Nov 29, 2023

eric-wieser Nov 29, 2023

alexkeizer Nov 29, 2023

eric-wieser Nov 30, 2023

eric-wieser Nov 30, 2023

alexkeizer Nov 30, 2023 •

edited

Loading

eric-wieser commented Nov 30, 2023

kim-em commented Nov 30, 2023

mathlib-bors bot commented Dec 1, 2023

[Merged by Bors] - chore: bump Std, changes for leanprover/std4#366 #8700

[Merged by Bors] - chore: bump Std, changes for leanprover/std4#366 #8700

Conversation

kim-em commented Nov 29, 2023 • edited by eric-wieser Loading

alexkeizer commented Nov 29, 2023 • edited Loading

alexkeizer commented Nov 29, 2023

eric-wieser Nov 29, 2023

Choose a reason for hiding this comment

eric-wieser Nov 29, 2023

Choose a reason for hiding this comment

alexkeizer Nov 29, 2023

Choose a reason for hiding this comment

eric-wieser Nov 30, 2023

Choose a reason for hiding this comment

eric-wieser Nov 30, 2023

Choose a reason for hiding this comment

alexkeizer Nov 30, 2023 • edited Loading

Choose a reason for hiding this comment

eric-wieser commented Nov 30, 2023

kim-em commented Nov 30, 2023

mathlib-bors bot commented Dec 1, 2023

kim-em commented Nov 29, 2023 •

edited by eric-wieser

Loading

alexkeizer commented Nov 29, 2023 •

edited

Loading

alexkeizer Nov 30, 2023 •

edited

Loading