feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` #5721

luisacicolini · 2024-10-15T07:29:41Z

No description provided.

leanprover-community-bot · 2024-10-15T07:50:08Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0bfe1a8c1a2e2eb6da0dad270d7b2bbdd5b97c3d --onto 225e08965d644715e8961cd205ffedf1cf7d24c2. (2024-10-15 07:50:08)
❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-10-15 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-10-15 08:44:20)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 11ae8bae42509eaca43db69ed95fbdd9570d5039 --onto 66dbad911eaaec4cd512662bd5cc67a2a16d2484. (2024-10-23 23:43:34)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 11ae8bae42509eaca43db69ed95fbdd9570d5039 --onto 09e1a05ee922bf8581ba9820f096ac1a2b1a2945. (2024-10-24 21:48:06)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8c7f7484f99b8f38a0d7c4dc7f6b48c0bed4fd7b --onto 193b6f2bec332ac0bce33e10856a96163d4be456. (2024-10-27 14:12:31)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-10-29 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-10-29 11:55:01)
✅ Mathlib branch lean-pr-testing-5721 has successfully built against this PR. (2024-10-30 02:01:56) View Log
✅ Mathlib branch lean-pr-testing-5721 has successfully built against this PR. (2024-10-30 12:14:55) View Log
✅ Mathlib branch lean-pr-testing-5721 has successfully built against this PR. (2024-10-31 02:29:16) View Log

src/Init/Data/BitVec/Lemmas.lean

alexkeizer

@luisacicolini I pushed a proof of msb_neg. I did have to use results from the Bitblast.lean file. For now, I copied the statements to Lemmas and sorried them out, but we'll have to move msb_neg et al to Bitblast.lean eventually (or another file that imports Bitblast.lean but has all the non-bitblasting lemmas that use bitblast results, which is an idea I'm starting to like more, the more we encounter this type of situation)

src/Init/Data/BitVec/Lemmas.lean

luisacicolini · 2024-10-30T11:34:13Z

Thank you very much @kim-em for reviewing this! All comments should be addressed now.

luisacicolini · 2024-10-30T11:34:17Z

awaiting-review

kim-em · 2024-10-31T01:27:58Z

src/Init/Data/BitVec/Bitblast.lean

+    getLsbD (-x) i =
+      (getLsbD x i ^^ decide (i < w ∧ ∃ j < i, getLsbD x j = true)) := by


Would

(-x).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j, j < i ∧ x.getLsbD j = true))

be okay here? This is what simp would transform the goal into.

Jup. Personally, I don't really like having so many separate decides floating around, but it is the simp normal form, so we should write it like you suggest. I just pushed the change

src/Init/Data/BitVec/Bitblast.lean

kim-em · 2024-10-31T01:29:48Z

src/Init/Data/BitVec/Bitblast.lean

+      exact ⟨w - 1 - j, by omega, h⟩
+
+theorem msb_neg {w : Nat} {x : BitVec w} :
+    (-x).msb = ((decide (x ≠ 0#w) && decide (x ≠ intMin w)) ^^ x.msb) := by


Suggested change

(-x).msb = ((decide (x ≠ 0#w) && decide (x ≠ intMin w)) ^^ x.msb) := by

(-x).msb = (((x != 0#w) && (x != intMin w)) ^^ x.msb) := by

Does this work? Seems slightly easier to just keep decide out of the statements when bool valued relations are available.

(Generally, I'm unhappy about how often we need decide in the BitVec API, but I don't have good solutions.)

It does, with a slightly amended proof I literally just pushed.

alexkeizer · 2024-10-31T01:44:37Z

src/Init/Data/BitVec/Bitblast.lean

+theorem msb_neg {w : Nat} {x : BitVec w} :
+    (-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb) := by
+  simp only [BitVec.msb, getMsbD_neg]
+  by_cases hmin : x = intMin _
+  case pos =>
+    have : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False := by
+      simp; omega
+    simp [hmin, getMsbD_intMin, this]
+  case neg =>
+    by_cases hzero : x = 0#w
+    case pos => simp [hzero]
+    case neg =>
+      have w_pos : 0 < w := by
+        cases w
+        · rw [@of_length_zero x] at hzero
+          contradiction
+        · omega
+      suffices ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true
+        by simp [show x != 0#w by simpa, show x != intMin w by simpa, this]
+      false_or_by_contra
+      rename_i getMsbD_x
+      simp only [not_exists, _root_.not_and, not_eq_true] at getMsbD_x
+      /- `getMsbD` says that all bits except the msb are `false` -/
+      cases hmsb : x.msb
+      case true =>
+        apply hmin
+        apply eq_of_getMsbD_eq
+        rintro ⟨i, hi⟩
+        simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and]
+        cases i
+        case zero => exact hmsb
+        case succ => exact getMsbD_x _ hi (by omega)
+      case false =>
+        apply hzero
+        apply eq_of_getMsbD_eq
+        rintro ⟨i, hi⟩
+        simp only [getMsbD_zero]
+        cases i
+        case zero => exact hmsb
+        case succ => exact getMsbD_x _ hi (by omega)


Suggested change

theorem msb_neg {w : Nat} {x : BitVec w} :

(-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb) := by

simp only [BitVec.msb, getMsbD_neg]

by_cases hmin : x = intMin _

case pos =>

have : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False := by

simp; omega

simp [hmin, getMsbD_intMin, this]

case neg =>

by_cases hzero : x = 0#w

case pos => simp [hzero]

case neg =>

have w_pos : 0 < w := by

cases w

· rw [@of_length_zero x] at hzero

contradiction

· omega

suffices ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true

by simp [show x != 0#w by simpa, show x != intMin w by simpa, this]

false_or_by_contra

rename_i getMsbD_x

simp only [not_exists, _root_.not_and, not_eq_true] at getMsbD_x

/- `getMsbD` says that all bits except the msb are `false` -/

cases hmsb : x.msb

case true =>

apply hmin

apply eq_of_getMsbD_eq

rintro ⟨i, hi⟩

simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and]

cases i

case zero => exact hmsb

case succ => exact getMsbD_x _ hi (by omega)

case false =>

apply hzero

apply eq_of_getMsbD_eq

rintro ⟨i, hi⟩

simp only [getMsbD_zero]

cases i

case zero => exact hmsb

case succ => exact getMsbD_x _ hi (by omega)

theorem msb_neg {w : Nat} {x : BitVec w} :

(-x).msb = ((x != 0#w && x != intMin w) ^^ x.msb) := by

simp only [BitVec.msb, getMsbD_neg]

by_cases hmin : x = intMin _

· have : (∃ j, j < w ∧ 0 < j ∧ 0 < w ∧ j = 0) ↔ False := by

simp; omega

simp [hmin, getMsbD_intMin, this]

· by_cases hzero : x = 0#w

· simp [hzero]

· have w_pos : 0 < w := by

cases w

· rw [@of_length_zero x] at hzero

contradiction

· omega

suffices ∃ j, j < w ∧ 0 < j ∧ x.getMsbD j = true

by simp [show x != 0#w by simpa, show x != intMin w by simpa, this]

false_or_by_contra

rename_i getMsbD_x

simp only [not_exists, _root_.not_and, not_eq_true] at getMsbD_x

/- `getMsbD` says that all bits except the msb are `false` -/

cases hmsb : x.msb with

| true =>

apply hmin

apply eq_of_getMsbD_eq

rintro ⟨i, hi⟩

simp only [getMsbD_intMin, w_pos, decide_True, Bool.true_and]

cases i with

| zero => exact hmsb

| succ => exact getMsbD_x _ hi (by omega)

| false =>

apply hzero

apply eq_of_getMsbD_eq

rintro ⟨i, hi⟩

simp only [getMsbD_zero]

cases i with

| zero => exact hmsb

| succ => exact getMsbD_x _ hi (by omega)

@kim-em Is the preference for cases _ with | zero => ... over case zero => ... a universal one, or just in those specific cases you pointed out before? I did a pass and noticed a few more uses of the latter

It is a mild, personal, universal preference. i.e. I always use with in every situation, but I don't particularly object to the other forms.

Let's not worry about this. Otherwise everything looks good now.

luisacicolini added 2 commits October 15, 2024 07:44

theorems draft

3a59c52

rw for consistency

de40001

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Oct 15, 2024

hargoniX reviewed Oct 15, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

if in if

41c038b

luisacicolini marked this pull request as ready for review October 16, 2024 09:28

alexkeizer reviewed Oct 17, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

kim-em added the awaiting-author Waiting for PR author to address issues label Oct 17, 2024

luisacicolini added 5 commits October 17, 2024 08:29

tmp

ef1087d

Merge branch 'master' of github.com:leanprover/lean4 into abs-neg-arith

dc357fc

tmp commit to merge

03f7e1e

Merge branch 'master' of github.com:leanprover/lean4 into abs-neg-arith

70a0355

taking a break

c8bdabd

luisacicolini marked this pull request as draft October 17, 2024 19:40

luisacicolini added 5 commits October 18, 2024 15:02

put theorems back to lemmas

cc6df3f

Merge branch 'master' of github.com:leanprover/lean4 into abs-neg-arith

bf13dc5

msb_intMin

cbc3bb8

cleaned bitblast file

cf26bbf

almost there

27bc429

tobiasgrosser reviewed Oct 19, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

tobiasgrosser reviewed Oct 19, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

alexkeizer added 6 commits October 19, 2024 16:06

prove an alternative statement of getLsbD_neg

2586124

typo

6da7f71

prove alternative statement of getMsbD_neg

34d985c

squeeze simp

74f6caa

prove msb_neg

e801d92

fill in sorry

0fc950b

alexkeizer reviewed Oct 19, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

alexkeizer reviewed Oct 19, 2024

View reviewed changes

src/Init/Data/BitVec/Lemmas.lean Outdated Show resolved Hide resolved

fixed theorems names

5e6a3ba

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2024

Update lean-toolchain for testing leanprover/lean4#5721

35b2bb4

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 30, 2024

Update lean-toolchain for testing leanprover/lean4#5721

89684d1

leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Oct 30, 2024

luisacicolini added 6 commits October 30, 2024 11:06

replaced case by dots in getLsbD_neg

efe6019

replaced syntax in cases getLsbD_neg

5dde2c7

replaced neq in msb_neg

cecaf63

suntax in induction in carry_succ_one

2cac25d

replace refine by exact

17f8a06

simpler getMSbD_neg proof

b60ba6f

github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Oct 30, 2024

luisacicolini marked this pull request as ready for review October 30, 2024 11:34

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 30, 2024

Trigger CI for leanprover/lean4#5721

2211f80

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 30, 2024

Trigger CI for leanprover/lean4#5721

2fa873c

kim-em reviewed Oct 31, 2024

View reviewed changes

change msb_neg to use bne

8c53ba8

alexkeizer reviewed Oct 31, 2024

View reviewed changes

src/Init/Data/BitVec/Bitblast.lean Outdated Show resolved Hide resolved

kim-em reviewed Oct 31, 2024

View reviewed changes

alexkeizer added 3 commits October 30, 2024 20:30

fix whitespace

4a3c48d

fix getLsbD_neg suggestion

2a802be

amend getLsbD_neg statement to be in simp-normal form

61244b0

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Oct 31, 2024

Trigger CI for leanprover/lean4#5721

8106a62

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 31, 2024

Trigger CI for leanprover/lean4#5721

3a3844a

alexkeizer reviewed Oct 31, 2024

View reviewed changes

kim-em added this pull request to the merge queue Nov 1, 2024

Merged via the queue into leanprover:master with commit 7730ddd Nov 1, 2024
14 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` #5721

feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` #5721

luisacicolini commented Oct 15, 2024

leanprover-community-bot commented Oct 15, 2024 •

edited

Loading

alexkeizer left a comment

luisacicolini commented Oct 30, 2024

luisacicolini commented Oct 30, 2024

kim-em Oct 31, 2024

alexkeizer Oct 31, 2024

kim-em Oct 31, 2024

alexkeizer Oct 31, 2024

alexkeizer Oct 31, 2024

kim-em Nov 1, 2024

kim-em Nov 1, 2024

		getLsbD (-x) i =
		(getLsbD x i ^^ decide (i < w ∧ ∃ j < i, getLsbD x j = true)) := by

	(-x).msb = ((decide (x ≠ 0#w) && decide (x ≠ intMin w)) ^^ x.msb) := by
	(-x).msb = (((x != 0#w) && (x != intMin w)) ^^ x.msb) := by

feat: add BitVec.(msb, getMsbD, getLsbD)_(neg, abs) #5721

feat: add BitVec.(msb, getMsbD, getLsbD)_(neg, abs) #5721

Conversation

luisacicolini commented Oct 15, 2024

leanprover-community-bot commented Oct 15, 2024 • edited Loading

alexkeizer left a comment

Choose a reason for hiding this comment

luisacicolini commented Oct 30, 2024

luisacicolini commented Oct 30, 2024

kim-em Oct 31, 2024

Choose a reason for hiding this comment

alexkeizer Oct 31, 2024

Choose a reason for hiding this comment

kim-em Oct 31, 2024

Choose a reason for hiding this comment

alexkeizer Oct 31, 2024

Choose a reason for hiding this comment

alexkeizer Oct 31, 2024

Choose a reason for hiding this comment

kim-em Nov 1, 2024

Choose a reason for hiding this comment

kim-em Nov 1, 2024

Choose a reason for hiding this comment

feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` #5721

feat: add `BitVec.(msb, getMsbD, getLsbD)_(neg, abs)` #5721

leanprover-community-bot commented Oct 15, 2024 •

edited

Loading