feat: ~~~(-x) bv_decide (#5670)

Co-authored-by: Siddharth <siddu.druid@gmail.com>

src/Init/Data/BitVec/Lemmas.lean

@@ -961,6 +961,15 @@ theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
   ext i
   simp
 
+theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
+  constructor
+  · intro h
+    rw [← h]
+    simp
+  · intro h
+    rw [h]
+    simp
+
 @[simp] theorem getMsb_not {x : BitVec w} :
     (~~~x).getMsbD i = (decide (i < w) && !(x.getMsbD i)) := by
   simp only [getMsbD]
@@ -2024,7 +2033,7 @@ theorem negOne_eq_allOnes : -1#w = allOnes w := by
     have r : (2^w - 1) < 2^w := by omega
     simp [Nat.mod_eq_of_lt q, Nat.mod_eq_of_lt r]
 
-theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1 := by
+theorem neg_eq_not_add (x : BitVec w) : -x = ~~~x + 1#w := by
   apply eq_of_toNat_eq
   simp only [toNat_neg, ofNat_eq_ofNat, toNat_add, toNat_not, toNat_ofNat, Nat.add_mod_mod]
   congr
@@ -2070,6 +2079,22 @@ theorem smod_zero {x : BitVec n} : x.smod 0#n = x := by
   · simp
   · by_cases h : x = 0#n <;> simp [h]
 
+theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
+  rcases w with _ | w
+  · apply Subsingleton.elim
+  · rw [BitVec.not_eq_comm]
+    apply BitVec.eq_of_toNat_eq
+    simp only [BitVec.toNat_neg, BitVec.toNat_not, BitVec.toNat_add, BitVec.toNat_ofNat,
+      Nat.add_mod_mod]
+    by_cases hx : x.toNat = 0
+    · simp [hx]
+    · rw [show (_ - 1 % _) = _ by rw [Nat.mod_eq_of_lt (by omega)],
+        show _ + (_ - 1) = (x.toNat - 1) + 2^(w + 1) by omega,
+        Nat.add_mod_right,
+        show (x.toNat - 1) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)],
+        show (_ - x.toNat) % _ = _ by rw [Nat.mod_eq_of_lt (by omega)]]
+      omega
+
 /-! ### abs -/
 
 @[simp, bv_toNat]

src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize.lean

@@ -65,6 +65,69 @@ builtin_simproc [bv_normalize] maxUlt (BitVec.ult (_ : BitVec _) (_ : BitVec _))
   else
     return .continue
 
+-- A specialised version of BitVec.neg_eq_not_add so it doesn't trigger on -constant
+builtin_simproc [bv_normalize] neg_eq_not_add (-(_ : BitVec _)) := fun e => do
+  let_expr Neg.neg typ _ val := e | return .continue
+  let_expr BitVec widthExpr := typ | return .continue
+  let some w ← getNatValue? widthExpr | return .continue
+  match ← getBitVecValue? val with
+  | some _ => return .continue
+  | none =>
+    let proof := mkApp2 (mkConst ``BitVec.neg_eq_not_add) (toExpr w) val
+    let expr ← mkAppM ``HAdd.hAdd #[← mkAppM ``Complement.complement #[val], (toExpr 1#w)]
+    return .visit { expr := expr, proof? := some proof }
+
+builtin_simproc [bv_normalize] bv_add_const ((_ : BitVec _) + ((_ : BitVec _) + (_ : BitVec _))) :=
+  fun e => do
+    let_expr HAdd.hAdd _ _ _ _ exp1 rhs := e | return .continue
+    let_expr HAdd.hAdd _ _ _ _ exp2 exp3 := rhs | return .continue
+    let some ⟨w, exp1Val⟩ ←  getBitVecValue? exp1 | return .continue
+    let proofBuilder thm := mkApp4 (mkConst thm) (toExpr w) exp1 exp2 exp3
+    match ← getBitVecValue? exp2 with
+    | some ⟨w', exp2Val⟩ =>
+      if h : w = w' then
+        let newLhs := exp1Val + h ▸ exp2Val
+        let expr ← mkAppM ``HAdd.hAdd #[toExpr newLhs, exp3]
+        let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_left
+        return .visit { expr := expr, proof? := some proof }
+      else
+        return .continue
+    | none =>
+      let some ⟨w', exp3Val⟩ ← getBitVecValue? exp3 | return .continue
+      if h : w = w' then
+        let newLhs := exp1Val + h ▸ exp3Val
+        let expr ← mkAppM ``HAdd.hAdd #[toExpr newLhs, exp2]
+        let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_right
+        return .visit { expr := expr, proof? := some proof }
+      else
+        return .continue
+
+builtin_simproc [bv_normalize] bv_add_const' (((_ : BitVec _) + (_ : BitVec _)) + (_ : BitVec _)) :=
+  fun e => do
+    let_expr HAdd.hAdd _ _ _ _ lhs exp3 := e | return .continue
+    let_expr HAdd.hAdd _ _ _ _ exp1 exp2 := lhs | return .continue
+    let some ⟨w, exp3Val⟩ ←  getBitVecValue? exp3 | return .continue
+    let proofBuilder thm := mkApp4 (mkConst thm) (toExpr w) exp1 exp2 exp3
+    match ← getBitVecValue? exp1 with
+    | some ⟨w', exp1Val⟩ =>
+      if h : w = w' then
+        let newLhs := exp3Val + h ▸ exp1Val
+        -- TODO
+        let expr ← mkAppM ``HAdd.hAdd #[toExpr newLhs, exp2]
+        let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_left'
+        return .visit { expr := expr, proof? := some proof }
+      else
+        return .continue
+    | none =>
+      let some ⟨w', exp2Val⟩ ← getBitVecValue? exp2 | return .continue
+      if h : w = w' then
+        let newLhs := exp3Val + h ▸ exp2Val
+        let expr ← mkAppM ``HAdd.hAdd #[toExpr newLhs, exp1]
+        let proof := proofBuilder ``Std.Tactic.BVDecide.Normalize.BitVec.add_const_right'
+        return .visit { expr := expr, proof? := some proof }
+      else
+        return .continue
+
 /--
 A pass in the normalization pipeline. Takes the current goal and produces a refined one or closes
 the goal fully, indicated by returning `none`.

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -5,6 +5,7 @@ Authors: Henrik Böving
 -/
 prelude
 import Init.Data.BitVec.Bitblast
+import Init.Data.AC
 import Std.Tactic.BVDecide.Normalize.Bool
 import Std.Tactic.BVDecide.Normalize.Canonicalize
 
@@ -18,7 +19,6 @@ namespace Normalize
 
 section Reduce
 
-attribute [bv_normalize] BitVec.neg_eq_not_add
 attribute [bv_normalize] BitVec.sub_toAdd
 
 @[bv_normalize]
@@ -109,23 +109,57 @@ theorem BitVec.not_add (a : BitVec w) : ~~~a + a = (-1#w) := by
 
 @[bv_normalize]
 theorem BitVec.add_neg (a : BitVec w) : a + (~~~a + 1#w) = 0#w := by
-  rw [← BitVec.ofNat_eq_ofNat]
   rw [← BitVec.neg_eq_not_add]
   rw [← BitVec.sub_toAdd]
   rw [BitVec.sub_self]
 
+@[bv_normalize]
+theorem BitVec.add_neg' (a : BitVec w) : a + (1#w + ~~~a) = 0#w := by
+  rw [BitVec.add_comm 1#w (~~~a)]
+  rw [BitVec.add_neg]
+
 @[bv_normalize]
 theorem BitVec.neg_add (a : BitVec w) : (~~~a + 1#w) + a = 0#w := by
-  rw [← BitVec.ofNat_eq_ofNat]
   rw [← BitVec.neg_eq_not_add]
   rw [BitVec.add_comm]
   rw [← BitVec.sub_toAdd]
   rw [BitVec.sub_self]
 
+@[bv_normalize]
+theorem BitVec.neg_add' (a : BitVec w) : (1#w + ~~~a) + a = 0#w := by
+  rw [BitVec.add_comm 1#w (~~~a)]
+  rw [BitVec.neg_add]
+
+@[bv_normalize]
+theorem BitVec.not_neg (x : BitVec w) : ~~~(~~~x + 1#w) = x + -1#w := by
+  rw [← BitVec.neg_eq_not_add x]
+  rw [_root_.BitVec.not_neg]
+
+@[bv_normalize]
+theorem BitVec.not_neg' (x : BitVec w) : ~~~(1#w + ~~~x) = x + -1#w := by
+  rw [BitVec.add_comm 1#w (~~~x)]
+  rw [BitVec.not_neg]
+
+@[bv_normalize]
+theorem BitVec.not_neg'' (x : BitVec w) : ~~~(x + 1#w) = ~~~x + -1#w := by
+  rw [← BitVec.not_not (b := x)]
+  rw [BitVec.not_neg]
+  simp
+
+@[bv_normalize]
+theorem BitVec.not_neg''' (x : BitVec w) : ~~~(1#w + x) = ~~~x + -1#w := by
+  rw [BitVec.add_comm 1#w x]
+  rw [BitVec.not_neg'']
+
 @[bv_normalize]
 theorem BitVec.add_same (a : BitVec w) : a + a = a * 2#w := by
   rw [BitVec.mul_two]
 
+theorem BitVec.add_const_left (a b c : BitVec w) : a + (b + c) = (a + b) + c := by ac_rfl
+theorem BitVec.add_const_right (a b c : BitVec w) : a + (b + c) = (a + c) + b := by ac_rfl
+theorem BitVec.add_const_left' (a b c : BitVec w) : (a + b) + c = (a + c) + b := by ac_rfl
+theorem BitVec.add_const_right' (a b c : BitVec w) : (a + b) + c = (b + c) + a := by ac_rfl
+
 @[bv_normalize]
 theorem BitVec.zero_sshiftRight : BitVec.sshiftRight 0#w a = 0#w := by
   ext

tests/lean/run/5664.lean

@@ -0,0 +1,10 @@
+import Std.Tactic.BVDecide
+
+set_option bv.ac_nf false in
+example
+  (a k n : BitVec 32) :
+  n < -1 - k →
+    ((¬a + k + 1 - a ≤ a + k - a ∧ ¬a + k + 1 + n - a ≤ a + k - a) ∧
+        ¬a - (a + k + 1) ≤ a + k + 1 + n - (a + k + 1)) ∧
+      ¬a + k - (a + k + 1) ≤ a + k + 1 + n - (a + k + 1) := by
+  bv_decide

tests/lean/run/bv_decide_rewriter.lean

@@ -73,5 +73,14 @@ example {x : BitVec 16} {i} {h} : BitVec.ofBool (x[i]'h) = x.extractLsb' i 1 :=
 example {x : BitVec 16} {i} {h} : x[i] = x.getLsbD i := by bv_normalize
 example {x y : BitVec 1} : x + y = x ^^^ y := by bv_normalize
 example {x y : BitVec 1} : x * y = x &&& y := by bv_normalize
-example {x y : BitVec 16} : x / 0 = 0 := by bv_normalize
-example {x y : BitVec 16} : x % 0 = x := by bv_normalize
+example {x : BitVec 16} : x / 0 = 0 := by bv_normalize
+example {x : BitVec 16} : x % 0 = x := by bv_normalize
+example {x : BitVec 16} : ~~~(-x) = x + (-1#16) := by bv_normalize
+example {x : BitVec 16} : ~~~(~~~x + 1#16) = x + (-1#16) := by bv_normalize
+example {x : BitVec 16} : ~~~(x + 1#16) = ~~~x + (-1#16) := by bv_normalize
+example {x : BitVec 16} : ~~~(1#16 + ~~~x) = x + (-1#16) := by bv_normalize
+example {x : BitVec 16} : ~~~(1#16 + x) = ~~~x + (-1#16) := by bv_normalize
+example {x : BitVec 16} : (10 + x) + 2 = 12 + x := by bv_normalize
+example {x : BitVec 16} : (x + 10) + 2 = 12 + x := by bv_normalize
+example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
+example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize