From b71ca39faf021167846baad232addd5e2e9a5f4c Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Sat, 28 Sep 2024 15:08:33 +0100
Subject: [PATCH] feat: start experimenting with 'abs' in bv_decide (#665)

---
 SSA/Projects/InstCombine/ForLean.lean        | 23 ++++++++++++++++++++
 SSA/Projects/InstCombine/HackersDelight.lean |  6 +++--
 SSA/Projects/InstCombine/TacticAuto.lean     |  5 ++++-
 3 files changed, 31 insertions(+), 3 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 8b2e9d980..3d39c8064 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -89,6 +89,29 @@ end Nat
 
 namespace BitVec
 
+@[simp]
+theorem replicate_one {w : Nat} : BitVec.replicate w 1#1 = cast (by simp) (allOnes w) := by
+  ext i
+  simp
+  omega
+
+@[simp]
+theorem replicate_zero {w : Nat} : BitVec.replicate w 0#1 = cast (by simp) (0#w) := by
+  ext i
+  simp
+
+theorem abs_eq_add_xor {x : BitVec w} :
+    have y : BitVec w := BitVec.cast (by simp) (BitVec.replicate w (BitVec.ofBool x.msb))
+    x.abs = (x + y) ^^^ y := by
+  simp only [BitVec.abs, neg_eq]
+  by_cases h: x.msb
+  · simp [h, ← allOnes_sub_eq_not]
+  · simp [h]
+
+theorem abs_eq_if {x : BitVec w} :
+    x.abs = if x.msb then -x else x := by
+  simp only [BitVec.abs, neg_eq]
+
 @[simp, bv_toNat]
 lemma toNat_shiftLeft' (A B : BitVec w) :
     BitVec.toNat (A <<< B) = (BitVec.toNat A) * 2 ^ BitVec.toNat B % 2 ^w := by
diff --git a/SSA/Projects/InstCombine/HackersDelight.lean b/SSA/Projects/InstCombine/HackersDelight.lean
index 435c2f7e4..bedea625e 100644
--- a/SSA/Projects/InstCombine/HackersDelight.lean
+++ b/SSA/Projects/InstCombine/HackersDelight.lean
@@ -1,6 +1,8 @@
 import SSA.Projects.InstCombine.ForMathlib
 import SSA.Projects.InstCombine.ForStd
 import SSA.Projects.InstCombine.TacticAuto
+import Std.Tactic.BVDecide
+
 
 set_option linter.unusedTactic false
 set_option linter.unreachableTactic false
@@ -9,7 +11,7 @@ namespace HackersDelight
 
 namespace Ch2Basics
 
-variable {x y z : BitVec w}
+variable {x y z : BitVec 32}
 
 /- 2–3 Inequalities among Logical and Arithmetic Expressions -/
 
@@ -62,7 +64,7 @@ theorem neq_iff_neg_sub_abs :
 
 theorem lt_iff_sub_xor_xor_and_sub_xor :
     (x <ₛ y) ↔ ((x - y) ^^^ ((x ^^^ y) &&& ((x - y) ^^^ x))).msb := by
-  -- try alive_auto -- this leads to a heartbeat timeout
+  try alive_auto
   all_goals sorry
 
 theorem slt_iff_and_not_or_not_xor_and_sub :
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index 0658e03fd..35a8cb701 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -155,7 +155,10 @@ macro "bv_auto": tactic =>
               simp (config := {failIfUnchanged := false}) only [(BitVec.two_mul), ←BitVec.negOne_eq_allOnes]
               bv_automata
             )
-          | bv_decide
+          |
+            simp (config := {failIfUnchanged := false}) only [BitVec.abs_eq_if]
+            try split
+            all_goals bv_decide
           | bv_distrib
       )
    )