From 4c57f997b507d6cffd5d6984500b887aefb04b89 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 25 Sep 2024 09:39:29 +0100 Subject: [PATCH 1/6] added some shiftLeft and not theorems --- src/Init/Data/BitVec/Lemmas.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 497c06b8674d..d1e54095b18e 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -939,6 +939,11 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl ext i simp +@[simp] +theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by + ext i + simp + /-! ### cast -/ @[simp] theorem not_cast {x : BitVec w} (h : w = w') : ~~~(cast h x) = cast h (~~~x) := by @@ -1072,6 +1077,16 @@ theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) : cases h₅ : decide (i < n + m) <;> simp at * <;> omega +@[simp] +theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} (n : Nat) : + BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by + simp [← BitVec.shiftLeft_and_distrib] + +@[simp] +theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} (n : Nat) : + BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by + simp [← shiftLeft_or_distrib] + @[deprecated shiftLeft_add (since := "2024-06-02")] theorem shiftLeft_shiftLeft {w : Nat} (x : BitVec w) (n m : Nat) : (x <<< n) <<< m = x <<< (n + m) := by @@ -2363,6 +2378,11 @@ theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) : (x * y).toNat = x.toNat * y.toNat := by rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h] +@[simp] +theorem one_shiftLeft_mul {x y : BitVec w} : + 1#w <<< x.toNat * y = y <<< x.toNat := by + simp [← mul_twoPow_eq_shiftLeft, BitVec.mul_comm] + /-! ### Decidable quantifiers -/ theorem forall_zero_iff {P : BitVec 0 → Prop} : From 82aeae19e18cfd6e6b634f2536c98c3c4bf0b860 Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 25 Sep 2024 09:44:46 +0100 Subject: [PATCH 2/6] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Tobias Grosser --- 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 d1e54095b18e..c9577efdedda 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1083,7 +1083,7 @@ theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} (n : Nat) : simp [← BitVec.shiftLeft_and_distrib] @[simp] -theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} (n : Nat) : +theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} {n : Nat} : BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by simp [← shiftLeft_or_distrib] From 8a8f68ae96896bc745125411b7bc2e0ec4aecbfd Mon Sep 17 00:00:00 2001 From: Luisa Cicolini <48860705+luisacicolini@users.noreply.github.com> Date: Wed, 25 Sep 2024 09:44:52 +0100 Subject: [PATCH 3/6] Update src/Init/Data/BitVec/Lemmas.lean Co-authored-by: Tobias Grosser --- 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 c9577efdedda..e67ab52db649 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -1078,7 +1078,7 @@ theorem shiftLeft_add {w : Nat} (x : BitVec w) (n m : Nat) : simp at * <;> omega @[simp] -theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} (n : Nat) : +theorem allOnes_shiftLeft_and_shiftLeft {x : BitVec w} {n : Nat} : BitVec.allOnes w <<< n &&& x <<< n = x <<< n := by simp [← BitVec.shiftLeft_and_distrib] From 0f97b430976f1cca32dc8335cb2d44ce430c4b69 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 25 Sep 2024 09:50:06 +0100 Subject: [PATCH 4/6] dropped misplaced thm --- src/Init/Data/BitVec/Lemmas.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index d1e54095b18e..6ef4e0b443d3 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -2378,11 +2378,6 @@ theorem toNat_mul_of_lt {w} {x y : BitVec w} (h : x.toNat * y.toNat < 2^w) : (x * y).toNat = x.toNat * y.toNat := by rw [BitVec.toNat_mul, Nat.mod_eq_of_lt h] -@[simp] -theorem one_shiftLeft_mul {x y : BitVec w} : - 1#w <<< x.toNat * y = y <<< x.toNat := by - simp [← mul_twoPow_eq_shiftLeft, BitVec.mul_comm] - /-! ### Decidable quantifiers -/ theorem forall_zero_iff {P : BitVec 0 → Prop} : From 0b996a9ce96c2e864dc6ba235164daa3d79e6180 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 25 Sep 2024 10:17:27 +0100 Subject: [PATCH 5/6] addressed comment --- src/Init/Data/BitVec/Lemmas.lean | 2 +- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 5 ----- 2 files changed, 1 insertion(+), 6 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index e74d513e329b..16f752e003b6 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -939,7 +939,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl ext i simp -@[simp] +@[bv_normalize] theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by ext i simp diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index c6b9835ddd7a..d95fddc5e41d 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -141,11 +141,6 @@ theorem BitVec.mul_zero (a : BitVec w) : a * 0#w = 0#w := by theorem BitVec.zero_mul (a : BitVec w) : 0#w * a = 0#w := by simp [bv_toNat] -@[bv_normalize] -theorem BitVec.not_not (a : BitVec w) : ~~~(~~~a) = a := by - ext - simp - @[bv_normalize] theorem BitVec.shiftLeft_zero (n : BitVec w) : n <<< 0#w' = n := by ext i From 17f27e23f404a4f4d8498b80f8708438ed2718d7 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 25 Sep 2024 10:21:28 +0100 Subject: [PATCH 6/6] fixed bv_normalize --- src/Init/Data/BitVec/Lemmas.lean | 2 +- src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 16f752e003b6..e74d513e329b 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -939,7 +939,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl ext i simp -@[bv_normalize] +@[simp] theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by ext i simp diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index d95fddc5e41d..2813f36f4b2e 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -61,6 +61,8 @@ attribute [bv_normalize] BitVec.getLsbD_zero_length attribute [bv_normalize] BitVec.getLsbD_concat_zero attribute [bv_normalize] BitVec.mul_one attribute [bv_normalize] BitVec.one_mul +attribute [bv_normalize] BitVec.not_not + end Constant