From 08ebc449d894acc138f1697eae7ead5190b49685 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Fri, 9 Aug 2024 05:10:03 +0100 Subject: [PATCH] chore: eliminate redundant BitVec.msb_one (#518) --- SSA/Projects/InstCombine/ForLean.lean | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean index 32cf8f6d9..a0ce6b637 100644 --- 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]