From c219303270c8db12c7f84e6ccc6e8b0b03f54216 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 4 Sep 2024 13:08:03 +1000 Subject: [PATCH] chore: remove @[simp] from some BitVec lemmas (#5249) I think it would be reasonable, but for now unnecessary, to add @[simp] to `toNat_of_zero_length` and the subsequent three lemmas. --- src/Init/Data/BitVec/Lemmas.lean | 21 +++++++++++++------ src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 2 +- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index e2551d63ec97..08be13ad1412 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -203,10 +203,19 @@ theorem eq_of_getMsbD_eq {x y : BitVec w} -- This cannot be a `@[simp]` lemma, as it would be tried at every term. theorem of_length_zero {x : BitVec 0} : x = 0#0 := by ext; simp -@[simp] theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero] +theorem toNat_zero_length (x : BitVec 0) : x.toNat = 0 := by simp [of_length_zero] theorem getLsbD_zero_length (x : BitVec 0) : x.getLsbD i = false := by simp theorem getMsbD_zero_length (x : BitVec 0) : x.getMsbD i = false := by simp -@[simp] theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero] +theorem msb_zero_length (x : BitVec 0) : x.msb = false := by simp [BitVec.msb, of_length_zero] + +theorem toNat_of_zero_length (h : w = 0) (x : BitVec w) : x.toNat = 0 := by + subst h; simp [toNat_zero_length] +theorem getLsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getLsbD i = false := by + subst h; simp [getLsbD_zero_length] +theorem getMsbD_of_zero_length (h : w = 0) (x : BitVec w) : x.getMsbD i = false := by + subst h; simp [getMsbD_zero_length] +theorem msb_of_zero_length (h : w = 0) (x : BitVec w) : x.msb = false := by + subst h; simp [msb_zero_length] theorem eq_of_toFin_eq : ∀ {x y : BitVec w}, x.toFin = y.toFin → x = y | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl @@ -285,7 +294,7 @@ theorem msb_eq_getLsbD_last (x : BitVec w) : @[bv_toNat] theorem getLsbD_last (x : BitVec w) : x.getLsbD (w-1) = decide (2 ^ (w-1) ≤ x.toNat) := by rcases w with rfl | w - · simp + · simp [toNat_of_zero_length] · simp only [getLsbD, Nat.testBit_to_div_mod, Nat.succ_sub_succ_eq_sub, Nat.sub_zero] rcases (Nat.lt_or_ge (BitVec.toNat x) (2 ^ w)) with h | h · simp [Nat.div_eq_of_lt h, h] @@ -336,7 +345,7 @@ theorem toInt_eq_toNat_cond (x : BitVec n) : rfl theorem msb_eq_false_iff_two_mul_lt (x : BitVec w) : x.msb = false ↔ 2 * x.toNat < 2^w := by - cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide] + cases w <;> simp [Nat.pow_succ, Nat.mul_comm _ 2, msb_eq_decide, toNat_of_zero_length] theorem msb_eq_true_iff_two_mul_ge (x : BitVec w) : x.msb = true ↔ 2 * x.toNat ≥ 2^w := by simp [← Bool.ne_false_iff, msb_eq_false_iff_two_mul_lt] @@ -992,7 +1001,7 @@ theorem sshiftRight_eq_of_msb_true {x : BitVec w} {s : Nat} (h : x.msb = true) : (x.sshiftRight s) = ~~~((~~~x) >>> s) := by apply BitVec.eq_of_toNat_eq rcases w with rfl | w - · simp + · simp [toNat_of_zero_length] · rw [BitVec.sshiftRight_eq, BitVec.toInt_eq_toNat_cond] have hxbound : (2 * x.toNat ≥ 2 ^ (w + 1)) := (BitVec.msb_eq_true_iff_two_mul_ge x).mp h replace hxbound : ¬ (2 * x.toNat < 2 ^ (w + 1)) := by omega @@ -1813,7 +1822,7 @@ theorem getLsbD_rotateRight {x : BitVec w} {r i : Nat} : @[simp, bv_toNat] theorem toNat_twoPow (w : Nat) (i : Nat) : (twoPow w i).toNat = 2^i % 2^w := by rcases w with rfl | w - · simp [Nat.mod_one] + · simp [Nat.mod_one, toNat_of_zero_length] · simp only [twoPow, toNat_shiftLeft, toNat_ofNat] have h1 : 1 < 2 ^ (w + 1) := Nat.one_lt_two_pow (by omega) rw [Nat.mod_eq_of_lt h1, Nat.shiftLeft_eq, Nat.one_mul] diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 6600f57cc03d..5b28185342f1 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -190,7 +190,7 @@ theorem BitVec.zero_ult' (a : BitVec w) : (BitVec.ult 0#w a) = (0#w != a) := by theorem BitVec.max_ult (a : BitVec w) : ¬ ((-1#w) < a) := by rcases w with rfl | w -· simp [bv_toNat] +· simp [bv_toNat, BitVec.toNat_of_zero_length] · simp only [BitVec.lt_def, BitVec.toNat_neg, BitVec.toNat_ofNat, Nat.not_lt] rw [Nat.mod_eq_of_lt (a := 1) (by simp)]; rw [Nat.mod_eq_of_lt]