feat: BitVec.zero_sub (#658)

Co-authored-by: emmau678 <[email protected]> Co-authored-by: Tobias Grosser <[email protected]>
opencompl · Sep 26, 2024 · 831c747 · 831c747
1 parent 1b9ebb8
commit 831c747
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -621,6 +621,10 @@ theorem allOnes_shiftLeft_or_shiftLeft {x : BitVec w} (n : Nat) :
     BitVec.allOnes w <<< n ||| x <<< n = BitVec.allOnes w <<< n := by
   simp [← BitVec.shiftLeft_or_distrib]
 
+@[simp]
+theorem zero_sub {x : BitVec w} : 0#w - x = - x := by
+    simp [bv_toNat]
+
 end BitVec
 
 namespace Bool