chore: eliminate redundant BitVec.msb_one (#518)

opencompl · Aug 9, 2024 · 08ebc44 · 08ebc44
1 parent 078d9d6
commit 08ebc44
Showing 1 changed file with 3 additions and 7 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -74,7 +74,8 @@ def toInt_zero_eq (w : Nat) : BitVec.toInt 0#w = 0 := by
  simp [BitVec.toInt]
 def toNat_zero_eq (w : Nat) : BitVec.toNat 0#w = 0 := rfl
 
-def msb_ofInt_one (h : 1 < w): BitVec.msb 1#w = false := by
+@[simp]
+def msb_one (h : 1 < w) : BitVec.msb 1#w = false := by
   simp only [BitVec.msb_eq_decide, decide_eq_false_iff_not, not_le, toNat_ofInt,
     toNat_ofNat]
   rw [Nat.mod_eq_of_lt] <;> simp <;> omega
@@ -104,11 +105,6 @@ lemma ofInt_ofNat (w n : Nat) :
     BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w n :=
   rfl
 
--- @[simp]
-def msb_one (h : 1 < w) : BitVec.msb (1#w) = false := by
-  rw [← ofInt_ofNat]
-  simp [msb_ofInt_one h]
-
 -- @[simp]
 def neg_allOnes {w : Nat} : -(allOnes w) = (1#w) := by
   simp [bv_toNat]
@@ -133,7 +129,7 @@ theorem udiv_one_eq_self (w : Nat) (x : BitVec w) : BitVec.udiv x (1#w)  = x :=
 def sdiv_one_allOnes {w : Nat} (h : 1 < w) :
     BitVec.sdiv (1#w) (BitVec.allOnes w) = BitVec.allOnes w := by
   simp only [BitVec.sdiv]
-  simp only [msb_ofInt_one h, neg_eq, @msb_allOnes w (by omega)]
+  simp only [msb_one h, neg_eq, @msb_allOnes w (by omega)]
   simp only [neg_allOnes]
   simp only [udiv_one_eq_self]
   simp only [negOne_eq_allOnes]