From a6cb5036baec3c751460424c7b371c5e26ace7a2 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 16 Dec 2024 17:51:33 +0000 Subject: [PATCH 1/9] feat: upstream Nat.div_pos --- src/Init/Data/Nat/Div/Lemmas.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Data/Nat/Div/Lemmas.lean b/src/Init/Data/Nat/Div/Lemmas.lean index 538a92568913..c37f07f2589e 100644 --- a/src/Init/Data/Nat/Div/Lemmas.lean +++ b/src/Init/Data/Nat/Div/Lemmas.lean @@ -49,4 +49,9 @@ theorem lt_div_mul_self (h : 0 < k) (w : k ≤ x) : x - k < x / k * k := by have : x % k < k := mod_lt x h omega +theorem div_pos (hba : b ≤ a) (hb : 0 < b) : 0 < a / b := by + cases b + · contradiction + · simp [Nat.pos_iff_ne_zero, div_eq_zero_iff_lt, hba] + end Nat From 20a71fcf8dfa0849e7eb7be59a04353a11ff8bea Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 16 Dec 2024 17:52:51 +0000 Subject: [PATCH 2/9] feat: `BitVec.{toFin, toInt}_umod` --- src/Init/Data/BitVec/Lemmas.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 0b6596bf4388..2e51032b1560 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2570,6 +2570,10 @@ theorem umod_def {x y : BitVec n} : have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt simp [umod, bv_toNat, Nat.mod_eq_of_lt h] +@[simp] +theorem toFin_umod {x y : BitVec w} : + (x % y).toFin = x.toFin % y.toFin := rfl + @[simp, bv_toNat] theorem toNat_umod {x y : BitVec n} : (x % y).toNat = x.toNat % y.toNat := rfl @@ -2601,6 +2605,14 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by rcases hy with rfl | rfl <;> rfl +theorem toInt_umod_eq_bmod {x y : BitVec w} : + (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by + simp [toInt_eq_toNat_bmod] + +theorem toInt_umod_of_msb {x y : BitVec w} (h : x.msb = false) : + (x % y).toInt = x.toInt % y.toNat := by + simp [toInt_eq_msb_cond, h] + /-! ### smtUDiv -/ theorem smtUDiv_eq (x y : BitVec w) : smtUDiv x y = if y = 0#w then allOnes w else x / y := by From 03373e77550dad274d8388c052644e7d607feb81 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 16 Dec 2024 17:53:13 +0000 Subject: [PATCH 3/9] feat: BitVec.msb_umod --- src/Init/Data/BitVec/Lemmas.lean | 37 ++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 2e51032b1560..cfdee3c64c17 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -10,6 +10,7 @@ import Init.Data.BitVec.Basic import Init.Data.Fin.Lemmas import Init.Data.Nat.Lemmas import Init.Data.Nat.Mod +import Init.Data.Nat.Div.Lemmas import Init.Data.Int.Bitwise.Lemmas import Init.Data.Int.Pow @@ -2605,6 +2606,42 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by rcases hy with rfl | rfl <;> rfl +@[simp] +theorem msb_umod {x y : BitVec w} : + (x % y).msb = (x.msb && (x < y || y == 0#w)) := by + rw [msb_eq_decide, toNat_umod] + cases msb_x : x.msb + · suffices x.toNat % y.toNat < 2 ^ (w - 1) by simpa + calc + x.toNat % y.toNat ≤ x.toNat := by apply Nat.mod_le + _ < 2 ^ (w - 1) := by simpa [msb_eq_decide] using msb_x + . by_cases hy : y = 0 + · simp_all [msb_eq_decide] + · suffices 2 ^ (w - 1) ≤ x.toNat % y.toNat ↔ x < y by simp_all + by_cases x_lt_y : x < y + . simp_all [Nat.mod_eq_of_lt x_lt_y, msb_eq_decide] + · suffices x.toNat % y.toNat < 2 ^ (w - 1) by + simpa [x_lt_y] + have y_le_x : y.toNat ≤ x.toNat := by + simpa using x_lt_y + replace hy : y.toNat ≠ 0 := + neq_iff_toNat_neq.mpr hy + by_cases msb_y : y.toNat < 2 ^ (w - 1) + · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega) + omega + · rcases w with _|w + · contradiction + simp only [Nat.add_one_sub_one] + replace msb_y : 2 ^ w ≤ y.toNat := by + simpa using msb_y + have : y.toNat ≤ y.toNat * (x.toNat / y.toNat) := by + apply Nat.le_mul_of_pos_right + apply Nat.div_pos y_le_x + omega + have : x.toNat % y.toNat ≤ x.toNat - y.toNat := by + rw [Nat.mod_eq_sub]; omega + omega + theorem toInt_umod_eq_bmod {x y : BitVec w} : (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by simp [toInt_eq_toNat_bmod] From d16ff31a8d5a910f796b1bc6bbf2c3b0526b7857 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 16 Dec 2024 18:02:06 +0000 Subject: [PATCH 4/9] feat: umod_eq_of_lt --- src/Init/Data/BitVec/Lemmas.lean | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index cfdee3c64c17..2ab4afed2a56 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -99,6 +99,12 @@ theorem ofFin_eq_ofNat : @BitVec.ofFin w (Fin.mk x lt) = BitVec.ofNat w x := by theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl +/-- Prove nonequality of bitvectors in terms of nat operations. -/ +theorem neq_iff_toNat_neq {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by + constructor + · rintro h rfl; apply h rfl + · intro h h_eq; apply h <| eq_of_toNat_eq h_eq + @[simp] theorem val_toFin (x : BitVec w) : x.toFin.val = x.toNat := rfl @[bv_toNat] theorem toNat_eq {x y : BitVec n} : x = y ↔ x.toNat = y.toNat := @@ -2606,6 +2612,11 @@ theorem umod_eq_and {x y : BitVec 1} : x % y = x &&& (~~~y) := by rcases hy with rfl | rfl <;> rfl +theorem umod_eq_of_lt {x y : BitVec w} (h : x < y) : + x % y = x := by + apply eq_of_toNat_eq + simp [Nat.mod_eq_of_lt h] + @[simp] theorem msb_umod {x y : BitVec w} : (x % y).msb = (x.msb && (x < y || y == 0#w)) := by From 7542a6634ec5aeda0a69b70ca43651f8a5d3c531 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Mon, 16 Dec 2024 18:07:41 +0000 Subject: [PATCH 5/9] rename `neq` -> `ne` --- src/Init/Data/BitVec/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 2ab4afed2a56..69690fbd434e 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -100,7 +100,7 @@ theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl /-- Prove nonequality of bitvectors in terms of nat operations. -/ -theorem neq_iff_toNat_neq {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by +theorem ne_iff_toNat_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by constructor · rintro h rfl; apply h rfl · intro h h_eq; apply h <| eq_of_toNat_eq h_eq @@ -2636,7 +2636,7 @@ theorem msb_umod {x y : BitVec w} : have y_le_x : y.toNat ≤ x.toNat := by simpa using x_lt_y replace hy : y.toNat ≠ 0 := - neq_iff_toNat_neq.mpr hy + ne_iff_toNat_ne.mpr hy by_cases msb_y : y.toNat < 2 ^ (w - 1) · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega) omega From 2313b3cd9cf1937436410371685110dda5c08513 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 18 Dec 2024 13:22:04 +0000 Subject: [PATCH 6/9] Move toFin after toNat --- src/Init/Data/BitVec/Lemmas.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 69690fbd434e..8afe714c6843 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2577,14 +2577,14 @@ theorem umod_def {x y : BitVec n} : have h : x.toNat % y.toNat < 2 ^ n := Nat.lt_of_le_of_lt (Nat.mod_le _ _) x.isLt simp [umod, bv_toNat, Nat.mod_eq_of_lt h] -@[simp] -theorem toFin_umod {x y : BitVec w} : - (x % y).toFin = x.toFin % y.toFin := rfl - @[simp, bv_toNat] theorem toNat_umod {x y : BitVec n} : (x % y).toNat = x.toNat % y.toNat := rfl +@[simp] +theorem toFin_umod {x y : BitVec w} : + (x % y).toFin = x.toFin % y.toFin := rfl + @[simp] theorem umod_zero {x : BitVec n} : x % 0#n = x := by simp [umod_def] From 01213667f6e1e20cc1d0cfe6eb2f75816ecf0b2c Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Wed, 18 Dec 2024 13:23:11 +0000 Subject: [PATCH 7/9] toInt_umod_eq_bmod -> toInt_umod --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 8afe714c6843..71644b3324e9 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2653,7 +2653,7 @@ theorem msb_umod {x y : BitVec w} : rw [Nat.mod_eq_sub]; omega omega -theorem toInt_umod_eq_bmod {x y : BitVec w} : +theorem toInt_umod {x y : BitVec w} : (x % y).toInt = (x.toNat % y.toNat : Int).bmod (2 ^ w) := by simp [toInt_eq_toNat_bmod] From b8c014c03e413eae1d2bc1b16985fa5fd25f927b Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 10 Jan 2025 12:33:41 +0000 Subject: [PATCH 8/9] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Kim Morrison --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 71644b3324e9..2b49055defd0 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -100,7 +100,7 @@ theorem eq_of_toNat_eq {n} : ∀ {x y : BitVec n}, x.toNat = y.toNat → x = y | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl /-- Prove nonequality of bitvectors in terms of nat operations. -/ -theorem ne_iff_toNat_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by +theorem toNat_ne_iff_ne {n} {x y : BitVec n} : x.toNat ≠ y.toNat ↔ x ≠ y := by constructor · rintro h rfl; apply h rfl · intro h h_eq; apply h <| eq_of_toNat_eq h_eq From d2894eabb492bcbd52294080cc3ae207056fa814 Mon Sep 17 00:00:00 2001 From: Alex Keizer Date: Fri, 10 Jan 2025 14:06:13 +0000 Subject: [PATCH 9/9] fix: toNat_ne_iff_ne rename --- src/Init/Data/BitVec/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index acb61c79fdc9..377ab5cc885f 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2755,7 +2755,7 @@ theorem msb_umod {x y : BitVec w} : have y_le_x : y.toNat ≤ x.toNat := by simpa using x_lt_y replace hy : y.toNat ≠ 0 := - ne_iff_toNat_ne.mpr hy + toNat_ne_iff_ne.mpr hy by_cases msb_y : y.toNat < 2 ^ (w - 1) · have : x.toNat % y.toNat < y.toNat := Nat.mod_lt _ (by omega) omega