Prove by case splitting

opencompl · Sep 28, 2024 · d92c4c0 · d92c4c0
1 parent 3b45a88
commit d92c4c0
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 7 deletions.
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
@@ -108,10 +108,9 @@ theorem abs_eq_add_xor {x : BitVec w} :
   · simp [h, ← allOnes_sub_eq_not]
   · simp [h]
 
-theorem abs_eq_add_xor' {x : BitVec w} :
-    have y : BitVec w := BitVec.sshiftRight x (w - 1)
-    x.abs = (x + y) ^^^ y := by
-  sorry
+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) :

diff --git a/SSA/Projects/InstCombine/HackersDelight.lean b/SSA/Projects/InstCombine/HackersDelight.lean
@@ -64,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
@@ -156,8 +156,9 @@ macro "bv_auto": tactic =>
               bv_automata
             )
           |
-            simp (config := {failIfUnchanged := false}) only [BitVec.abs_eq_add_xor']
-            bv_decide
+            simp (config := {failIfUnchanged := false}) only [BitVec.abs_eq_if]
+            try split
+            all_goals bv_decide
           | bv_distrib
       )
    )