From 4a1c236e0ccb40d86482734629f8846087c0a1e2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Sun, 27 Oct 2024 00:37:23 +0200
Subject: [PATCH] feat: support BitVec.abs in bv_decide

---
 src/Init/Data/BitVec/Lemmas.lean              | 2 ++
 src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 1 +
 tests/lean/run/bv_arith.lean                  | 2 ++
 tests/lean/run/bv_decide_rewriter.lean        | 1 +
 4 files changed, 6 insertions(+)

diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean
index 9f35e7b4a381..0a8d02db90fe 100644
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -2115,6 +2115,8 @@ theorem not_neg (x : BitVec w) : ~~~(-x) = x + -1#w := by
 
 /-! ### abs -/
 
+theorem abs_eq {x : BitVec w} : x.abs = if x.msb then -x else x := by rfl
+
 @[simp, bv_toNat]
 theorem toNat_abs {x : BitVec w} : x.abs.toNat = if x.msb then 2^w - x.toNat else x.toNat := by
   simp only [BitVec.abs, neg_eq]
diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
index bef33a6e8fbb..175b2867427d 100644
--- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
+++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean
@@ -85,6 +85,7 @@ theorem BitVec.smod_umod (x y : BitVec w) :
   cases x.msb <;> cases y.msb <;> simp
 
 attribute [bv_normalize] Bool.cond_eq_if
+attribute [bv_normalize] BitVec.abs_eq
 
 end Reduce
 
diff --git a/tests/lean/run/bv_arith.lean b/tests/lean/run/bv_arith.lean
index 24374b3fd7c7..db01746eaf12 100644
--- a/tests/lean/run/bv_arith.lean
+++ b/tests/lean/run/bv_arith.lean
@@ -58,3 +58,5 @@ theorem arith_unit_13 (x y : BitVec 8) (hx : x.msb = false) (hy : y.msb = false)
 theorem arith_unit_14 (x y : BitVec 8) (hx : x.msb = true) (hy : y.msb = true) : (-((-x).umod (-y))) = x.smod y := by
   bv_decide
 
+theorem arith_unit_15 (x : BitVec 32) : BitVec.sle x (BitVec.abs x) := by
+  bv_decide
diff --git a/tests/lean/run/bv_decide_rewriter.lean b/tests/lean/run/bv_decide_rewriter.lean
index 10819fc7a3e0..92d699311fb6 100644
--- a/tests/lean/run/bv_decide_rewriter.lean
+++ b/tests/lean/run/bv_decide_rewriter.lean
@@ -80,6 +80,7 @@ example {x : BitVec 16} : 2 + (x + 10) = 12 + x := by bv_normalize
 example {x : BitVec 16} : 2 + (10 + x) = 12 + x := by bv_normalize
 example {x : BitVec 16} {b : Bool} : (if b then x else x) = x := by bv_normalize
 example {b : Bool} {x : Bool} : (bif b then x else x) = x := by bv_normalize
+example {x : BitVec 16} : x.abs = if x.msb then -x else x := by bv_normalize
 
 section