From 00fcd55a3aa2dd5fefa392677336ec6136ece14c Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 29 May 2024 19:13:39 +0100
Subject: [PATCH 01/18] chore: canonicalize constants in alive output

This will make subsequent patches for enabling reductions smaller,
as these canonicalization for some reason is not needed in that
case.
---
 SSA/Projects/InstCombine/AliveStatements.lean | 129 ++++++++----------
 SSA/Projects/InstCombine/Tactic.lean          |   3 +
 SSA/Projects/InstCombine/Test.lean            |  54 ++++++++
 3 files changed, 111 insertions(+), 75 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
index 6334f0e68..2391156b1 100644
--- a/SSA/Projects/InstCombine/AliveStatements.lean
+++ b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -17,7 +17,7 @@ set_option linter.unreachableTactic false
 
 theorem bitvec_AddSub_1043 :
     ∀ (e e_1 e_2 : LLVM.IntW w),
-      LLVM.add (LLVM.add (LLVM.xor (LLVM.and e_2 e_1) e_1) (LLVM.const? ↑1)) e ⊑ LLVM.sub e (LLVM.or e_2 (LLVM.not e_1)) := by
+      LLVM.add (LLVM.add (LLVM.xor (LLVM.and e_2 e_1) e_1) (LLVM.const? 1)) e ⊑ LLVM.sub e (LLVM.or e_2 (LLVM.not e_1)) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -33,7 +33,7 @@ theorem bitvec_AddSub_1152 :
   all_goals sorry
 
 theorem bitvec_AddSub_1156 :
-    ∀ (e : LLVM.IntW w), LLVM.add e e ⊑ LLVM.shl e (LLVM.const? ↑1) := by
+    ∀ (e : LLVM.IntW w), LLVM.add e e ⊑ LLVM.shl e (LLVM.const? 1) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -66,8 +66,7 @@ theorem bitvec_AddSub_1176 :
   all_goals sorry
 
 theorem bitvec_AddSub_1202 :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.add (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e ⊑ LLVM.sub (LLVM.sub e (LLVM.const? ↑1)) e_1 := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.add (LLVM.xor e_1 (LLVM.const? (-1))) e ⊑ LLVM.sub (LLVM.sub e (LLVM.const? 1)) e_1 := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -115,7 +114,7 @@ theorem bitvec_AddSub_1556 :
   all_goals sorry
 
 theorem bitvec_AddSub_1560 :
-    ∀ (e : LLVM.IntW w), LLVM.sub (LLVM.const? (Int.negSucc 0)) e ⊑ LLVM.xor e (LLVM.const? (Int.negSucc 0)) := by
+    ∀ (e : LLVM.IntW w), LLVM.sub (LLVM.const? (-1)) e ⊑ LLVM.xor e (LLVM.const? (-1)) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -123,8 +122,7 @@ theorem bitvec_AddSub_1560 :
   all_goals sorry
 
 theorem bitvec_AddSub_1564 :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.sub e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) ⊑ LLVM.add e (LLVM.add e_1 (LLVM.const? ↑1)) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.sub e_1 (LLVM.xor e (LLVM.const? (-1))) ⊑ LLVM.add e (LLVM.add e_1 (LLVM.const? 1)) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -242,8 +240,8 @@ theorem bitvec_AndOrXor_887_2 :
 
 theorem bitvec_AndOrXor_1230__A__B___A__B :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) (LLVM.xor e (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.xor (LLVM.or e_1 e) (LLVM.const? (Int.negSucc 0)) := by
+      LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1))) ⊑
+        LLVM.xor (LLVM.or e_1 e) (LLVM.const? (-1)) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -251,8 +249,7 @@ theorem bitvec_AndOrXor_1230__A__B___A__B :
   all_goals sorry
 
 theorem bitvec_AndOrXor_1241_AB__AB__AB :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.and (LLVM.or e_1 e) (LLVM.xor (LLVM.and e_1 e) (LLVM.const? (Int.negSucc 0))) ⊑ LLVM.xor e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.or e_1 e) (LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1))) ⊑ LLVM.xor e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -260,8 +257,7 @@ theorem bitvec_AndOrXor_1241_AB__AB__AB :
   all_goals sorry
 
 theorem bitvec_AndOrXor_1247_AB__AB__AB :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.and (LLVM.xor (LLVM.and e_1 e) (LLVM.const? (Int.negSucc 0))) (LLVM.or e_1 e) ⊑ LLVM.xor e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1))) (LLVM.or e_1 e) ⊑ LLVM.xor e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -269,7 +265,7 @@ theorem bitvec_AndOrXor_1247_AB__AB__AB :
   all_goals sorry
 
 theorem bitvec_AndOrXor_1253_A__AB___A__B :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.xor e_1 e) e_1 ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.xor e_1 e) e_1 ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -277,7 +273,7 @@ theorem bitvec_AndOrXor_1253_A__AB___A__B :
   all_goals sorry
 
 theorem bitvec_AndOrXor_1280_ABA___AB :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) e_1 ⊑ LLVM.and e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e) e_1 ⊑ LLVM.and e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -287,7 +283,7 @@ theorem bitvec_AndOrXor_1280_ABA___AB :
 theorem bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C :
     ∀ (e e_1 e_2 : LLVM.IntW w),
       LLVM.and (LLVM.xor e_2 e_1) (LLVM.xor (LLVM.xor e_1 e) e_2) ⊑
-        LLVM.and (LLVM.xor e_2 e_1) (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+        LLVM.and (LLVM.xor e_2 e_1) (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -295,8 +291,7 @@ theorem bitvec_AndOrXor_1288_A__B__B__C__A___A__B__C :
   all_goals sorry
 
 theorem bitvec_AndOrXor_1294_A__B__A__B___A__B :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.and (LLVM.or e_1 e) (LLVM.xor (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) ⊑ LLVM.and e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.and (LLVM.or e_1 e) (LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.and e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -315,7 +310,7 @@ theorem bitvec_AndOrXor_1683_1 :
 
 theorem bitvec_AndOrXor_1683_2 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or (LLVM.icmp LLVM.IntPredicate.uge e_1 e) (LLVM.icmp LLVM.IntPredicate.ne e_1 e) ⊑ LLVM.const? ↑1 := by
+      LLVM.or (LLVM.icmp LLVM.IntPredicate.uge e_1 e) (LLVM.icmp LLVM.IntPredicate.ne e_1 e) ⊑ LLVM.const? 1 := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -325,7 +320,7 @@ theorem bitvec_AndOrXor_1683_2 :
 theorem bitvec_AndOrXor_1704 :
     ∀ (e e_1 : LLVM.IntW w),
       LLVM.or (LLVM.icmp LLVM.IntPredicate.eq e_1 (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.ult e e_1) ⊑
-        LLVM.icmp LLVM.IntPredicate.uge (LLVM.add e_1 (LLVM.const? (Int.negSucc 0))) e := by
+        LLVM.icmp LLVM.IntPredicate.uge (LLVM.add e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -335,7 +330,7 @@ theorem bitvec_AndOrXor_1704 :
 theorem bitvec_AndOrXor_1705 :
     ∀ (e e_1 : LLVM.IntW w),
       LLVM.or (LLVM.icmp LLVM.IntPredicate.eq e_1 (LLVM.const? 0)) (LLVM.icmp LLVM.IntPredicate.ugt e_1 e) ⊑
-        LLVM.icmp LLVM.IntPredicate.uge (LLVM.add e_1 (LLVM.const? (Int.negSucc 0))) e := by
+        LLVM.icmp LLVM.IntPredicate.uge (LLVM.add e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -361,7 +356,7 @@ theorem bitvec_AndOrXor_2063__X__C1__C2____X__C2__C1__C2 :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2113___A__B__A___A__B :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.or (LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) e_1 ⊑ LLVM.or e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.or (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) e_1 ⊑ LLVM.or e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -370,8 +365,7 @@ theorem bitvec_AndOrXor_2113___A__B__A___A__B :
 
 theorem bitvec_AndOrXor_2118___A__B__A___A__B :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or (LLVM.and e_1 e) (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e := by
+      LLVM.or (LLVM.and e_1 e) (LLVM.xor e_1 (LLVM.const? (-1))) ⊑ LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -379,8 +373,7 @@ theorem bitvec_AndOrXor_2118___A__B__A___A__B :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2123___A__B__A__B___A__B :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or (LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0)))) (LLVM.xor e_1 e) ⊑ LLVM.xor e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.or (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.xor e_1 e) ⊑ LLVM.xor e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -389,9 +382,7 @@ theorem bitvec_AndOrXor_2123___A__B__A__B___A__B :
 
 theorem bitvec_AndOrXor_2188 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or (LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))))
-          (LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) ⊑
-        LLVM.xor e_1 e := by
+      LLVM.or (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -416,8 +407,8 @@ theorem bitvec_AndOrXor_2243__B__C__A__B___B__A__C :
 
 theorem bitvec_AndOrXor_2247__A__B__A__B :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) (LLVM.xor e (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.xor (LLVM.and e_1 e) (LLVM.const? (Int.negSucc 0)) := by
+      LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1))) ⊑
+        LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1)) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -434,8 +425,7 @@ theorem bitvec_AndOrXor_2263 :
 
 theorem bitvec_AndOrXor_2264 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or e_1 (LLVM.xor (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) ⊑
-        LLVM.or e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.or e_1 (LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -452,8 +442,7 @@ theorem bitvec_AndOrXor_2265 :
 
 theorem bitvec_AndOrXor_2284 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or e_1 (LLVM.xor (LLVM.or e_1 e) (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.or e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.or e_1 (LLVM.xor (LLVM.or e_1 e) (LLVM.const? (-1))) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -462,8 +451,7 @@ theorem bitvec_AndOrXor_2284 :
 
 theorem bitvec_AndOrXor_2285 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or e_1 (LLVM.xor (LLVM.xor e_1 e) (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.or e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.or e_1 (LLVM.xor (LLVM.xor e_1 e) (LLVM.const? (-1))) ⊑ LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -472,8 +460,7 @@ theorem bitvec_AndOrXor_2285 :
 
 theorem bitvec_AndOrXor_2297 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.or (LLVM.and e_1 e) (LLVM.xor (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) ⊑
-        LLVM.xor (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e := by
+      LLVM.or (LLVM.and e_1 e) (LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor (LLVM.xor e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -490,8 +477,8 @@ theorem bitvec_AndOrXor_2367 :
 
 theorem bitvec_AndOrXor_2416 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) (LLVM.const? (Int.negSucc 0)) ⊑
-        LLVM.or e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.xor (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) (LLVM.const? (-1)) ⊑
+        LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -500,8 +487,8 @@ theorem bitvec_AndOrXor_2416 :
 
 theorem bitvec_AndOrXor_2417 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) (LLVM.const? (Int.negSucc 0)) ⊑
-        LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.xor (LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e) (LLVM.const? (-1)) ⊑
+        LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -510,8 +497,8 @@ theorem bitvec_AndOrXor_2417 :
 
 theorem bitvec_AndOrXor_2429 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.and e_1 e) (LLVM.const? (Int.negSucc 0)) ⊑
-        LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1)) ⊑
+        LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -520,8 +507,8 @@ theorem bitvec_AndOrXor_2429 :
 
 theorem bitvec_AndOrXor_2430 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.or e_1 e) (LLVM.const? (Int.negSucc 0)) ⊑
-        LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+      LLVM.xor (LLVM.or e_1 e) (LLVM.const? (-1)) ⊑
+        LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -529,8 +516,7 @@ theorem bitvec_AndOrXor_2430 :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2443 :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.ashr (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) (LLVM.const? (Int.negSucc 0)) ⊑ LLVM.ashr e_1 e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.ashr (LLVM.xor e_1 (LLVM.const? (-1))) e) (LLVM.const? (-1)) ⊑ LLVM.ashr e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -539,7 +525,7 @@ theorem bitvec_AndOrXor_2443 :
 
 theorem bitvec_AndOrXor_2453 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.icmp LLVM.IntPredicate.slt e_1 e) (LLVM.const? (Int.negSucc 0)) ⊑ LLVM.icmp LLVM.IntPredicate.sge e_1 e := by
+      LLVM.xor (LLVM.icmp LLVM.IntPredicate.slt e_1 e) (LLVM.const? (-1)) ⊑ LLVM.icmp LLVM.IntPredicate.sge e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -547,8 +533,7 @@ theorem bitvec_AndOrXor_2453 :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2475 :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.sub e_1 e) (LLVM.const? (Int.negSucc 0)) ⊑ LLVM.add e (LLVM.sub (LLVM.const? (Int.negSucc 0)) e_1) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.sub e_1 e) (LLVM.const? (-1)) ⊑ LLVM.add e (LLVM.sub (LLVM.const? (-1)) e_1) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -556,8 +541,7 @@ theorem bitvec_AndOrXor_2475 :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2486 :
-    ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.add e_1 e) (LLVM.const? (Int.negSucc 0)) ⊑ LLVM.sub (LLVM.sub (LLVM.const? (Int.negSucc 0)) e) e_1 := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.add e_1 e) (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.sub (LLVM.const? (-1)) e) e_1 := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -565,7 +549,7 @@ theorem bitvec_AndOrXor_2486 :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2581__BAB___A__B :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.or e_1 e) e ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.or e_1 e) e ⊑ LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1))) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -573,7 +557,7 @@ theorem bitvec_AndOrXor_2581__BAB___A__B :
   all_goals sorry
 
 theorem bitvec_AndOrXor_2587__BAA___B__A :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.and e_1 e) e ⊑ LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.xor (LLVM.and e_1 e) e ⊑ LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -590,9 +574,7 @@ theorem bitvec_AndOrXor_2595 :
 
 theorem bitvec_AndOrXor_2607 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.or e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))))
-          (LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) ⊑
-        LLVM.xor e_1 e := by
+      LLVM.xor (LLVM.or e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑ LLVM.xor e_1 e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -601,8 +583,7 @@ theorem bitvec_AndOrXor_2607 :
 
 theorem bitvec_AndOrXor_2617 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0))))
-          (LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e) ⊑
+      LLVM.xor (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e) ⊑
         LLVM.xor e_1 e := by
   simp_alive_undef
   simp_alive_ops
@@ -612,7 +593,7 @@ theorem bitvec_AndOrXor_2617 :
 
 theorem bitvec_AndOrXor_2627 :
     ∀ (e e_1 e_2 : LLVM.IntW w),
-      LLVM.xor (LLVM.xor e_2 e_1) (LLVM.or e_2 e) ⊑ LLVM.xor (LLVM.and (LLVM.xor e_2 (LLVM.const? (Int.negSucc 0))) e) e_1 := by
+      LLVM.xor (LLVM.xor e_2 e_1) (LLVM.or e_2 e) ⊑ LLVM.xor (LLVM.and (LLVM.xor e_2 (LLVM.const? (-1))) e) e_1 := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -629,8 +610,8 @@ theorem bitvec_AndOrXor_2647 :
 
 theorem bitvec_AndOrXor_2658 :
     ∀ (e e_1 : LLVM.IntW w),
-      LLVM.xor (LLVM.and e_1 (LLVM.xor e (LLVM.const? (Int.negSucc 0)))) (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.xor (LLVM.and e_1 e) (LLVM.const? (Int.negSucc 0)) := by
+      LLVM.xor (LLVM.and e_1 (LLVM.xor e (LLVM.const? (-1)))) (LLVM.xor e_1 (LLVM.const? (-1))) ⊑
+        LLVM.xor (LLVM.and e_1 e) (LLVM.const? (-1)) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -648,7 +629,7 @@ theorem bitvec_AndOrXor_2663 :
   all_goals sorry
 
 theorem bitvec_152 :
-    ∀ (e : LLVM.IntW w), LLVM.mul e (LLVM.const? (Int.negSucc 0)) ⊑ LLVM.sub (LLVM.const? 0) e := by
+    ∀ (e : LLVM.IntW w), LLVM.mul e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -712,7 +693,7 @@ theorem bitvec_283 :
   all_goals sorry
 
 theorem bitvec_290__292 :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.mul (LLVM.shl (LLVM.const? ↑1) e_1) e ⊑ LLVM.shl e e_1 := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.mul (LLVM.shl (LLVM.const? 1) e_1) e ⊑ LLVM.shl e e_1 := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -736,7 +717,7 @@ theorem bitvec_820' :
   all_goals sorry
 
 theorem bitvec_1030 :
-    ∀ (e : LLVM.IntW w), LLVM.sdiv e (LLVM.const? (Int.negSucc 0)) ⊑ LLVM.sub (LLVM.const? 0) e := by
+    ∀ (e : LLVM.IntW w), LLVM.sdiv e (LLVM.const? (-1)) ⊑ LLVM.sub (LLVM.const? 0) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -745,8 +726,7 @@ theorem bitvec_1030 :
 
 theorem bitvec_Select_858 :
     ∀ (e e_1 : LLVM.IntW 1),
-      LLVM.select e_1 (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e ⊑
-        LLVM.and (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e := by
+      LLVM.select e_1 (LLVM.xor e_1 (LLVM.const? (-1))) e ⊑ LLVM.and (LLVM.xor e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -755,8 +735,7 @@ theorem bitvec_Select_858 :
 
 theorem bitvec_Select_859' :
     ∀ (e e_1 : LLVM.IntW 1),
-      LLVM.select e_1 e (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) ⊑
-        LLVM.or (LLVM.xor e_1 (LLVM.const? (Int.negSucc 0))) e := by
+      LLVM.select e_1 e (LLVM.xor e_1 (LLVM.const? (-1))) ⊑ LLVM.or (LLVM.xor e_1 (LLVM.const? (-1))) e := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -764,7 +743,7 @@ theorem bitvec_Select_859' :
   all_goals sorry
 
 theorem bitvec_select_1100 :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.select (LLVM.const? ↑1) e_1 e ⊑ e_1 := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.select (LLVM.const? 1) e_1 e ⊑ e_1 := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -780,7 +759,7 @@ theorem bitvec_Select_1105 :
   all_goals sorry
 
 theorem bitvec_InstCombineShift__239 :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.lshr (LLVM.shl e_1 e) e ⊑ LLVM.and e_1 (LLVM.lshr (LLVM.const? (Int.negSucc 0)) e) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.lshr (LLVM.shl e_1 e) e ⊑ LLVM.and e_1 (LLVM.lshr (LLVM.const? (-1)) e) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -788,7 +767,7 @@ theorem bitvec_InstCombineShift__239 :
   all_goals sorry
 
 theorem bitvec_InstCombineShift__279 :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.shl (LLVM.lshr e_1 e) e ⊑ LLVM.and e_1 (LLVM.shl (LLVM.const? (Int.negSucc 0)) e) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.shl (LLVM.lshr e_1 e) e ⊑ LLVM.and e_1 (LLVM.shl (LLVM.const? (-1)) e) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
@@ -832,7 +811,7 @@ theorem bitvec_InstCombineShift__497''' :
   all_goals sorry
 
 theorem bitvec_InstCombineShift__582 :
-    ∀ (e e_1 : LLVM.IntW w), LLVM.lshr (LLVM.shl e_1 e) e ⊑ LLVM.and e_1 (LLVM.lshr (LLVM.const? (Int.negSucc 0)) e) := by
+    ∀ (e e_1 : LLVM.IntW w), LLVM.lshr (LLVM.shl e_1 e) e ⊑ LLVM.and e_1 (LLVM.lshr (LLVM.const? (-1)) e) := by
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
diff --git a/SSA/Projects/InstCombine/Tactic.lean b/SSA/Projects/InstCombine/Tactic.lean
index bdc93176a..cba8e427e 100644
--- a/SSA/Projects/InstCombine/Tactic.lean
+++ b/SSA/Projects/InstCombine/Tactic.lean
@@ -68,6 +68,9 @@ macro "simp_alive_ssa" : tactic =>
         simp (config := {failIfUnchanged := false}) only [
             InstCombine.Op.denote, HVector.getN, HVector.get
           ]
+
+        -- Fold integers into their canonical form.
+        simp (config := {failIfUnchanged := false }) only [Nat.cast_ofNat, Nat.cast_one, Int.reduceNegSucc, Int.reduceNeg]
       )
   )
 
diff --git a/SSA/Projects/InstCombine/Test.lean b/SSA/Projects/InstCombine/Test.lean
index d2e7d5c41..6b7ad26fb 100644
--- a/SSA/Projects/InstCombine/Test.lean
+++ b/SSA/Projects/InstCombine/Test.lean
@@ -560,3 +560,57 @@ def two_ne_macro_noreduce_proof (w : Nat) :
   simp_alive_meta
   simp_alive_ssa
   apply two_ne_stmt
+
+set_option ssa.alive_icom_reduce true in
+def constant_macro (w : Nat) :=
+  [alive_icom (w)|{
+  ^bb0():
+    %0 = "llvm.mlir.constant" () { value = 2 : _ } : () -> (_)
+    %1 = "llvm.mlir.constant" () { value = 1 : _ } : () -> (_)
+    %2 = "llvm.mlir.constant" () { value = 0 : _ } : () -> (_)
+    %3 = "llvm.mlir.constant" () { value = -1 : _ } : () -> (_)
+    %4 = "llvm.mlir.constant" () { value = -2 : _ } : () -> (_)
+    %5 = "llvm.add" (%0, %1) : (_, _) -> (_)
+    %6 = "llvm.add" (%5, %2) : (_, _) -> (_)
+    %7 = "llvm.add" (%6, %3) : (_, _) -> (_)
+    %8 = "llvm.add" (%7, %4) : (_, _) -> (_)
+    "llvm.return" (%8) : (_) -> ()
+  }]
+
+set_option ssa.alive_icom_reduce false in
+def constant_macro_noreduce (w : Nat) :=
+  [alive_icom (w)|{
+  ^bb0():
+    %0 = "llvm.mlir.constant" () { value = 2 : _ } : () -> (_)
+    %1 = "llvm.mlir.constant" () { value = 1 : _ } : () -> (_)
+    %2 = "llvm.mlir.constant" () { value = 0 : _ } : () -> (_)
+    %3 = "llvm.mlir.constant" () { value = -1 : _ } : () -> (_)
+    %4 = "llvm.mlir.constant" () { value = -2 : _ } : () -> (_)
+    %5 = "llvm.add" (%0, %1) : (_, _) -> (_)
+    %6 = "llvm.add" (%5, %2) : (_, _) -> (_)
+    %7 = "llvm.add" (%6, %3) : (_, _) -> (_)
+    %8 = "llvm.add" (%7, %4) : (_, _) -> (_)
+    "llvm.return" (%8) : (_) -> ()
+  }]
+
+def constant_stmt :
+    @BitVec.Refinement (BitVec w)
+      (LLVM.add (LLVM.add (LLVM.add (LLVM.add (LLVM.const? 2) (LLVM.const? 1))
+        (LLVM.const? 0)) (LLVM.const? (-1))) (LLVM.const? (-2)))
+      (LLVM.add (LLVM.add (LLVM.add (LLVM.add (LLVM.const? 2) (LLVM.const? 1))
+        (LLVM.const? 0)) (LLVM.const? (-1))) (LLVM.const? (-2))) := by
+  simp
+
+def constant_macro_proof (w : Nat) :
+    constant_macro w ⊑ constant_macro w := by
+  unfold constant_macro
+  simp_alive_meta
+  simp_alive_ssa
+  apply constant_stmt
+
+def constant_macro_noreduce_proof (w : Nat) :
+    constant_macro_noreduce w ⊑ constant_macro_noreduce w := by
+  unfold constant_macro_noreduce
+  simp_alive_meta
+  simp_alive_ssa
+  apply constant_stmt

From 4ec25157a2f91b9b64e26fc143610bed02afc8c4 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 29 May 2024 21:24:11 +0100
Subject: [PATCH 02/18] chore: canonicalize constants in alive output

---
 SSA/Projects/InstCombine/ForLean.lean    |  5 ++--
 SSA/Projects/InstCombine/ForStd.lean     | 30 ++++++++++++++++++++++++
 SSA/Projects/InstCombine/TacticAuto.lean |  5 +++-
 3 files changed, 37 insertions(+), 3 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 26abf657e..bfb8c432d 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -120,8 +120,9 @@ theorem Nat.one_mod_two_pow_succ_eq {n : Nat} : 1 % 2 ^ n.succ = 1 := by
 
 @[simp]
 lemma ofInt_ofNat (w n : Nat) :
-    BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w n :=
-  rfl
+    BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w n := by rfl
+
+lemma ofInt_ofNat' : BitVec.ofInt w (OfNat.ofNat (α := ℤ) x ) = x#w := rfl
 
 -- @[simp]
 def msb_one (h : 1 < w) : BitVec.msb (1#w) = false := by
diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index c1a09a039..244bcb9e0 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -131,4 +131,34 @@ theorem bitvec_minus_one : BitVec.ofInt w (Int.negSucc 0) = (-1 : _root_.BitVec
     rw [zeroBitwidth]
     simp
 
+theorem bitvec_minus_one' : BitVec.ofInt w (-1) = (-1 : _root_.BitVec w) := by
+  simp
+  by_cases zeroBitwidth : 0 < w
+  case pos =>
+    apply BitVec.eq_of_toInt_eq
+    simp
+    unfold BitVec.toInt
+    simp
+    have xx : 1 % 2 ^ w = 1 := by
+      rw [Nat.mod_eq_of_lt]
+      simp [Nat.pow_one]
+      omega
+    simp [xx]
+    split
+    · rename_i h
+      rw [Nat.mod_eq_of_lt] at h
+      · have xxx : 2 * (2 ^ w - 1) = 2 * 2 ^ w - 2 * 1 := by omega
+        rw [xxx] at h
+        simp at h
+        omega
+      · omega
+    · simp only [Int.bmod, Int.reduceNeg, Int.natCast_pred_of_pos _ (Nat.two_pow_pos w),
+        Int.neg_emod]
+      omega
+  case neg =>
+    simp_all
+    rw [zeroBitwidth]
+    simp
+
+
   end BitVec
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index 362099c6a..77cfd88e1 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -62,7 +62,10 @@ macro "simp_alive_ops" : tactic =>
   `(tactic|
       (
         simp (config := {failIfUnchanged := false}) only [
-            simp_llvm, BitVec.bitvec_minus_one, pure_bind
+            simp_llvm, BitVec.bitvec_minus_one,
+            BitVec.bitvec_minus_one',
+            (BitVec.ofInt_ofNat'),
+            pure_bind
           ]
       )
   )

From 2291c64d0731c34cd6e87d22062eea644cea7d3e Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 29 May 2024 22:09:13 +0100
Subject: [PATCH 03/18] chore: makeit build

---
 .../AliveHandwrittenLargeExamples.lean        | 28 +++++++++----------
 SSA/Projects/InstCombine/ForLean.lean         | 15 +++-------
 2 files changed, 17 insertions(+), 26 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 455abfe41..765fc9f51 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -233,9 +233,8 @@ def alive_simplifyMulDivRem805' (w : Nat) :
   split_ifs with c
   simp
   by_cases w_0 : w = 0; subst w_0; simp [BitVec.eq_nil a]
-  by_cases h : BitVec.ofInt w 3 >ᵤ BitVec.ofInt w 1 + a
+  by_cases h : 3#w >ᵤ 1#w + a
   · simp [h]
-    rw [ofInt_eq_ofNat, ofInt_eq_ofNat] at h
     by_cases a_0 : a = 0; subst a_0; simp at c
     by_cases a_1 : a = 1; subst a_1; rw [sdiv_one_one]
     rw [BitVec.toNat_eq] at a_0 a_1
@@ -254,9 +253,6 @@ def alive_simplifyMulDivRem805' (w : Nat) :
     by_cases a_allones : a = allOnes w
     · have x := sdiv_one_allOnes w_gt_1
       rw [a_allones]
-      have rr : 1#w = BitVec.ofInt w 1 := by rfl
-
-      simp [rr] at x
       simp [x]
     ·
       rw [Nat.add_mod_of_add_mod_lt] at h
@@ -281,13 +277,11 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       simp only [ofNat_eq_ofNat, toNat_ofNat, Nat.zero_mod, toNat_ofInt, Nat.cast_pow,
         Nat.cast_ofNat, toNat_neg] at c
       norm_cast at c
-      simp only [Int.toNat_natCast] at c
       apply c.elim
       by_cases w_1 : w = 1; subst w_1; simp at h
       have w_gt_1 : 1 < w := by omega;
       simp only [BitVec.ult_toNat, toNat_add, toNat_ofInt, decide_eq_false_iff_not] at h
       norm_cast at h
-      simp only [Int.toNat_natCast] at h
       simp only [
         Nat.mod_eq_of_lt (@Nat.pow_le_pow_of_le 2 2 w (by omega) (by omega)),
         Nat.mod_eq_of_lt, ofNat_eq_ofNat, toNat_ofNat, Nat.add_mod_mod,
@@ -301,12 +295,21 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       norm_cast at h
       simp only [Int.toNat_natCast, toNat_allOnes, Nat.mod_add_mod] at h
       by_cases w_1 : w = 1; subst w_1; simp at h
-      rw [Nat.add_sub_of_le (by omega), Nat.mod_self, nonpos_iff_eq_zero] at h
-      rw [Nat.mod_eq_of_lt] at h
-      simp at h
+      simp only [BitVec.toNat_ofNat] at h
       have et : _ := @Nat.pow_le_pow_of_le 2 2 w (by simp) (by omega)
+      rw [Nat.mod_eq_of_lt (by omega)] at h
+      have xx : 1 % (2^w) = 1 := by
+        rw [Nat.mod_eq_of_lt]
+        omega
+      rw [xx] at h
+      ring_nf at h
+      rw [Nat.add_comm] at h
+      rw [Nat.sub_add_cancel] at h
+      rw [Nat.mod_self] at h
+      simp at h
       omega
     rw [one_sdiv a_ne_zero a_ne_one a_ne_allOnes]
+    rfl
 
 /--info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805'' depends on axioms:
 [propext, Classical.choice, Quot.sound] -/
@@ -361,11 +364,6 @@ def alive_simplifyMulDivRem290 (w : Nat) :
   by_cases h : w ≤ BitVec.toNat B <;> simp [h]
   apply BitVec.eq_of_toNat_eq
   simp [bv_toNat]
-  norm_cast
-  have : (1 % 2^w) = 1 := by
-    apply Nat.mod_eq_of_lt
-    apply Nat.one_lt_pow <;> omega
-  simp [this]
   ring_nf
 
 /-- info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem290' depends on
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index bfb8c432d..584e649a6 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -90,10 +90,10 @@ def toInt_zero_eq (w : Nat) : BitVec.toInt 0#w = 0 := by
  simp [BitVec.toInt]
 def toNat_zero_eq (w : Nat) : BitVec.toNat 0#w = 0 := rfl
 
-def msb_ofInt_one (h : 1 < w): BitVec.msb (BitVec.ofInt w 1) = false := by
+def msb_ofInt_one (h : 1 < w): BitVec.msb (1#w) = false := by
   simp only [BitVec.msb_eq_decide, decide_eq_false_iff_not, not_le, toNat_ofInt]
   norm_cast
-  simp only [Int.toNat_natCast]
+  simp only [BitVec.toNat_ofNat]
   rw [Nat.mod_eq_of_lt] <;> simp <;> omega
 
 @[simp]
@@ -126,7 +126,6 @@ lemma ofInt_ofNat' : BitVec.ofInt w (OfNat.ofNat (α := ℤ) x ) = x#w := rfl
 
 -- @[simp]
 def msb_one (h : 1 < w) : BitVec.msb (1#w) = false := by
-  rw [← ofInt_ofNat]
   simp [msb_ofInt_one h]
 
 -- @[simp]
@@ -161,9 +160,7 @@ def sdiv_one_allOnes {w : Nat} (h : 1 < w) :
   simp only [msb_ofInt_one h, neg_eq, @msb_allOnes w (by omega)]
   simp only [neg_allOnes]
   simp only [udiv_one_eq_self]
-  rw [BitVec.msb_one]
   simp only [negOne_eq_allOnes]
-  exact h
 
 theorem width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
   obtain ⟨a, ha⟩ := a
@@ -260,7 +257,7 @@ lemma gt_one_of_neq_0_neq_1 (a : BitVec w) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a >
 
 def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
     (hao : a ≠ allOnes w) :
-    BitVec.sdiv (BitVec.ofInt w 1) a = BitVec.ofInt w 0 := by
+    BitVec.sdiv (1#w) a = BitVec.ofInt w 0 := by
   rcases w with ⟨rfl | ⟨rfl | w⟩⟩
   case zero => simp [BitVec.eq_nil a]
   case succ w' =>
@@ -300,22 +297,18 @@ def sdiv_one_one' (h : 1 < w) : BitVec.sdiv 1#w 1#w = 1#w := by
   apply BitVec.eq_of_toNat_eq
   simp [hone]
 
-def sdiv_one_one : BitVec.sdiv (BitVec.ofInt w 1) 1 = 1 := by
+def sdiv_one_one : BitVec.sdiv 1#w 1 = 1 := by
   by_cases w_0 : w = 0; subst w_0; rfl
   by_cases w_1 : w = 1; subst w_1; rfl
   unfold BitVec.sdiv
   unfold BitVec.udiv
   simp
   rw [msb_one (by omega)]
-  rw [msb_ofInt_one (by omega)]
   simp
   have ki' : (1) % (2) ^ w = 1 := by
     rw [Nat.mod_eq_of_lt]
     simp
     omega
-  have ki : (1:Int) % (2: Int) ^ w = 1 := by
-    norm_cast
-  simp only [ki]
   simp only [ki']
   simp
   have one : 1 = 1#w := by

From 62c37a886f6e9859a2003a707ac331d021a68a34 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Wed, 29 May 2024 22:14:41 +0100
Subject: [PATCH 04/18] chore: makeit build

---
 .../InstCombine/AliveHandwrittenLargeExamples.lean        | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 765fc9f51..204a97f96 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -299,13 +299,9 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       have et : _ := @Nat.pow_le_pow_of_le 2 2 w (by simp) (by omega)
       rw [Nat.mod_eq_of_lt (by omega)] at h
       have xx : 1 % (2^w) = 1 := by
-        rw [Nat.mod_eq_of_lt]
-        omega
+        rw [Nat.mod_eq_of_lt (by omega)]
       rw [xx] at h
-      ring_nf at h
-      rw [Nat.add_comm] at h
-      rw [Nat.sub_add_cancel] at h
-      rw [Nat.mod_self] at h
+      rw [Nat.add_comm, Nat.sub_add_cancel, Nat.mod_self] at h
       simp at h
       omega
     rw [one_sdiv a_ne_zero a_ne_one a_ne_allOnes]

From c5a44362af3549b00a49275c9c19207f6e3090f7 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 05:15:53 +0100
Subject: [PATCH 05/18] chore: canonicalize constants in alive output

---
 SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 204a97f96..051459be4 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -298,9 +298,7 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       simp only [BitVec.toNat_ofNat] at h
       have et : _ := @Nat.pow_le_pow_of_le 2 2 w (by simp) (by omega)
       rw [Nat.mod_eq_of_lt (by omega)] at h
-      have xx : 1 % (2^w) = 1 := by
-        rw [Nat.mod_eq_of_lt (by omega)]
-      rw [xx] at h
+      rw [@Nat.mod_eq_of_lt 1 (2^w) (by omega)] at h
       rw [Nat.add_comm, Nat.sub_add_cancel, Nat.mod_self] at h
       simp at h
       omega

From 3f4a41104b9aa8ab1725c1fdc4fe15ea522c98d8 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 05:19:37 +0100
Subject: [PATCH 06/18] chore: canonicalize constants in alive output

---
 .../InstCombine/AliveHandwrittenLargeExamples.lean         | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 051459be4..8962eb11b 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -297,10 +297,9 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       by_cases w_1 : w = 1; subst w_1; simp at h
       simp only [BitVec.toNat_ofNat] at h
       have et : _ := @Nat.pow_le_pow_of_le 2 2 w (by simp) (by omega)
-      rw [Nat.mod_eq_of_lt (by omega)] at h
-      rw [@Nat.mod_eq_of_lt 1 (2^w) (by omega)] at h
-      rw [Nat.add_comm, Nat.sub_add_cancel, Nat.mod_self] at h
-      simp at h
+      rw [Nat.mod_eq_of_lt (by omega), @Nat.mod_eq_of_lt 1 (2^w) (by omega),
+        Nat.add_comm, Nat.sub_add_cancel, Nat.mod_self] at h
+      norm_num at h
       omega
     rw [one_sdiv a_ne_zero a_ne_one a_ne_allOnes]
     rfl

From c88feed70e3c264311fdd8762a0eb9e423bafdd7 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 05:22:04 +0100
Subject: [PATCH 07/18] chore: canonicalize constants in alive output

---
 SSA/Projects/InstCombine/ForLean.lean | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 584e649a6..49ff4580f 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -90,7 +90,7 @@ def toInt_zero_eq (w : Nat) : BitVec.toInt 0#w = 0 := by
  simp [BitVec.toInt]
 def toNat_zero_eq (w : Nat) : BitVec.toNat 0#w = 0 := rfl
 
-def msb_ofInt_one (h : 1 < w): BitVec.msb (1#w) = false := by
+def msb_ofInt_one (h : 1 < w): BitVec.msb 1#w = false := by
   simp only [BitVec.msb_eq_decide, decide_eq_false_iff_not, not_le, toNat_ofInt]
   norm_cast
   simp only [BitVec.toNat_ofNat]
@@ -120,7 +120,8 @@ theorem Nat.one_mod_two_pow_succ_eq {n : Nat} : 1 % 2 ^ n.succ = 1 := by
 
 @[simp]
 lemma ofInt_ofNat (w n : Nat) :
-    BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w n := by rfl
+    BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w n :=
+  rfl
 
 lemma ofInt_ofNat' : BitVec.ofInt w (OfNat.ofNat (α := ℤ) x ) = x#w := rfl
 

From dcabde681f58c7686ca37dca36664e29807737e2 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 05:24:43 +0100
Subject: [PATCH 08/18] chore: canonicalize constants in alive output

---
 SSA/Projects/InstCombine/ForLean.lean |  2 +-
 SSA/Projects/InstCombine/ForStd.lean  | 31 ++-------------------------
 2 files changed, 3 insertions(+), 30 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 49ff4580f..cd400f1c2 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -258,7 +258,7 @@ lemma gt_one_of_neq_0_neq_1 (a : BitVec w) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a >
 
 def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
     (hao : a ≠ allOnes w) :
-    BitVec.sdiv (1#w) a = BitVec.ofInt w 0 := by
+    BitVec.sdiv 1#w a = BitVec.ofInt w 0 := by
   rcases w with ⟨rfl | ⟨rfl | w⟩⟩
   case zero => simp [BitVec.eq_nil a]
   case succ w' =>
diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index 244bcb9e0..d7c29bac4 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -131,34 +131,7 @@ theorem bitvec_minus_one : BitVec.ofInt w (Int.negSucc 0) = (-1 : _root_.BitVec
     rw [zeroBitwidth]
     simp
 
-theorem bitvec_minus_one' : BitVec.ofInt w (-1) = (-1 : _root_.BitVec w) := by
-  simp
-  by_cases zeroBitwidth : 0 < w
-  case pos =>
-    apply BitVec.eq_of_toInt_eq
-    simp
-    unfold BitVec.toInt
-    simp
-    have xx : 1 % 2 ^ w = 1 := by
-      rw [Nat.mod_eq_of_lt]
-      simp [Nat.pow_one]
-      omega
-    simp [xx]
-    split
-    · rename_i h
-      rw [Nat.mod_eq_of_lt] at h
-      · have xxx : 2 * (2 ^ w - 1) = 2 * 2 ^ w - 2 * 1 := by omega
-        rw [xxx] at h
-        simp at h
-        omega
-      · omega
-    · simp only [Int.bmod, Int.reduceNeg, Int.natCast_pred_of_pos _ (Nat.two_pow_pos w),
-        Int.neg_emod]
-      omega
-  case neg =>
-    simp_all
-    rw [zeroBitwidth]
-    simp
-
+theorem bitvec_minus_one' : BitVec.ofInt w (-1) = (-1 : BitVec w) := by
+  simp [bitvec_minus_one]
 
   end BitVec

From 706a3d7593620a7c328a7a8bc391f79feddc531c Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 05:36:48 +0100
Subject: [PATCH 09/18] chore: canonicalize constants in alive output

---
 SSA/Projects/InstCombine/ForStd.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index d7c29bac4..e3b97e666 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -132,6 +132,8 @@ theorem bitvec_minus_one : BitVec.ofInt w (Int.negSucc 0) = (-1 : _root_.BitVec
     simp
 
 theorem bitvec_minus_one' : BitVec.ofInt w (-1) = (-1 : BitVec w) := by
-  simp [bitvec_minus_one]
+  have x : -1 = Int.negSucc 0 := by simp
+  simp [x, bitvec_minus_one]
+
 
   end BitVec

From 4506ad9c68c7e9a10a16bedbea34406e137e6ad7 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 05:42:14 +0100
Subject: [PATCH 10/18] chore: canonicalize constants in alive output

---
 SSA/Projects/InstCombine/ForStd.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index e3b97e666..a23bb50c7 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -133,7 +133,9 @@ theorem bitvec_minus_one : BitVec.ofInt w (Int.negSucc 0) = (-1 : _root_.BitVec
 
 theorem bitvec_minus_one' : BitVec.ofInt w (-1) = (-1 : BitVec w) := by
   have x : -1 = Int.negSucc 0 := by simp
-  simp [x, bitvec_minus_one]
+  rw [x, bitvec_minus_one]
+
+
 
 
   end BitVec

From ae18006cd2ead7a0a7688f0c17a9e27c635ae449 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 12:13:19 +0100
Subject: [PATCH 11/18] Address comments

---
 .../AliveHandwrittenLargeExamples.lean        |  4 +--
 SSA/Projects/InstCombine/ForLean.lean         | 30 ++-----------------
 2 files changed, 5 insertions(+), 29 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 8962eb11b..b53f2cada 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -176,7 +176,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
                 simp [h1]
                 rw [Nat.mod_eq_of_lt (by omega)]
               subst h1
-              simp [BitVec.sdiv_one_one']
+              simp [BitVec.sdiv_one_one]
             · have hcases : (1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') ∨
                   1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') + 1) := by
                 omega
@@ -236,7 +236,7 @@ def alive_simplifyMulDivRem805' (w : Nat) :
   by_cases h : 3#w >ᵤ 1#w + a
   · simp [h]
     by_cases a_0 : a = 0; subst a_0; simp at c
-    by_cases a_1 : a = 1; subst a_1; rw [sdiv_one_one]
+    by_cases a_1 : a = 1; subst a_1; simp [sdiv_one_one]
     rw [BitVec.toNat_eq] at a_0 a_1
     simp at a_0 a_1
     by_cases w_1 : w = 1; subst w_1; omega
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index cd400f1c2..f0a5140e3 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -285,7 +285,9 @@ def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
         apply BitVec.udiv_one_eq_zero
         apply BitVec.gt_one_of_neq_0_neq_1 <;> assumption
 
-def sdiv_one_one' (h : 1 < w) : BitVec.sdiv 1#w 1#w = 1#w := by
+def sdiv_one_one : BitVec.sdiv 1#w 1#w = 1#w := by
+  by_cases w_0 : w = 0; subst w_0; rfl
+  by_cases w_1 : w = 1; subst w_1; rfl
   unfold BitVec.sdiv
   unfold BitVec.udiv
   simp only [toNat_ofNat, neg_eq, toNat_neg]
@@ -298,32 +300,6 @@ def sdiv_one_one' (h : 1 < w) : BitVec.sdiv 1#w 1#w = 1#w := by
   apply BitVec.eq_of_toNat_eq
   simp [hone]
 
-def sdiv_one_one : BitVec.sdiv 1#w 1 = 1 := by
-  by_cases w_0 : w = 0; subst w_0; rfl
-  by_cases w_1 : w = 1; subst w_1; rfl
-  unfold BitVec.sdiv
-  unfold BitVec.udiv
-  simp
-  rw [msb_one (by omega)]
-  simp
-  have ki' : (1) % (2) ^ w = 1 := by
-    rw [Nat.mod_eq_of_lt]
-    simp
-    omega
-  simp only [ki']
-  simp
-  have one : 1 = 1#w := by
-    simp
-  simp only [← one]
-  unfold BitVec.ofNatLt
-  simp
-  unfold BitVec.ofNat
-  unfold Fin.ofNat'
-  simp
-  rw [Nat.mod_eq_of_lt]
-  simp
-  omega
-
 def ofInt_eq_ofNat {a: Nat} :
     BitVec.ofInt w (@OfNat.ofNat ℤ a _) = BitVec.ofNat w a := by
   rfl

From d9f73fc09c671663645d7ce630ce7f0fa2cd460c Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 12:15:14 +0100
Subject: [PATCH 12/18] chore: nuke newlines

---
 SSA/Projects/InstCombine/ForStd.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForStd.lean b/SSA/Projects/InstCombine/ForStd.lean
index a23bb50c7..883e492b2 100644
--- a/SSA/Projects/InstCombine/ForStd.lean
+++ b/SSA/Projects/InstCombine/ForStd.lean
@@ -135,7 +135,4 @@ theorem bitvec_minus_one' : BitVec.ofInt w (-1) = (-1 : BitVec w) := by
   have x : -1 = Int.negSucc 0 := by simp
   rw [x, bitvec_minus_one]
 
-
-
-
   end BitVec

From eb43774035a356212e9718d3a55ba86dc5c4f177 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 12:31:28 +0100
Subject: [PATCH 13/18] WIP

---
 SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 2 ++
 SSA/Projects/InstCombine/TacticAuto.lean                    | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index b53f2cada..650a61044 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -232,6 +232,8 @@ def alive_simplifyMulDivRem805' (w : Nat) :
   simp
   split_ifs with c
   simp
+  -- TODO: This one does not work: simp [(BitVec.ofInt_ofNat)]
+  simp [(BitVec.ofInt_ofNat')]
   by_cases w_0 : w = 0; subst w_0; simp [BitVec.eq_nil a]
   by_cases h : 3#w >ᵤ 1#w + a
   · simp [h]
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
index 77cfd88e1..5595a03e3 100644
--- a/SSA/Projects/InstCombine/TacticAuto.lean
+++ b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -64,7 +64,7 @@ macro "simp_alive_ops" : tactic =>
         simp (config := {failIfUnchanged := false}) only [
             simp_llvm, BitVec.bitvec_minus_one,
             BitVec.bitvec_minus_one',
-            (BitVec.ofInt_ofNat'),
+            (BitVec.ofInt_ofNat),
             pure_bind
           ]
       )

From dc3dcfa15a8e0cf1eb10a8fc25c87c71a8f9657d Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 16:06:32 +0100
Subject: [PATCH 14/18] WIP

---
 SSA/Projects/InstCombine/ForLean.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 26abf657e..2b1d537d5 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -120,7 +120,7 @@ theorem Nat.one_mod_two_pow_succ_eq {n : Nat} : 1 % 2 ^ n.succ = 1 := by
 
 @[simp]
 lemma ofInt_ofNat (w n : Nat) :
-    BitVec.ofInt w (OfNat.ofNat n) = BitVec.ofNat w n :=
+    BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w n :=
   rfl
 
 -- @[simp]

From 120859b92cebbee7d807b47a75e61749d5070d9a Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 18:24:38 +0100
Subject: [PATCH 15/18] test

---
 .../AliveHandwrittenLargeExamples.lean        | 36 +++++--------
 SSA/Projects/InstCombine/ForLean.lean         | 51 ++++---------------
 2 files changed, 23 insertions(+), 64 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 455abfe41..32bfa0ecb 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -133,8 +133,6 @@ def alive_simplifyMulDivRem805 (w : Nat) :
       rw [LLVM.sdiv?_denom_zero_eq_none]
       apply Refinement.none_left
     case neg =>
-      rw [BitVec.ofInt_one_eq_ofNat_one]
-      rw [BitVec.ofInt_eq_ofNat_mod']
       rw [BitVec.ult_toNat]
       rw [BitVec.toNat_ofNat]
       cases w'
@@ -176,7 +174,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
                 simp [h1]
                 rw [Nat.mod_eq_of_lt (by omega)]
               subst h1
-              simp [BitVec.sdiv_one_one']
+              simp [BitVec.sdiv_one_one]
             · have hcases : (1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') ∨
                   1 + BitVec.toNat x = 2 ^ Nat.succ (Nat.succ w'') + 1) := by
                 omega
@@ -194,7 +192,6 @@ def alive_simplifyMulDivRem805 (w : Nat) :
         case h_3 c hugt =>
           clear c
           simp at hugt
-          simp only [ofInt_zero_eq]
           unfold LLVM.sdiv? -- TODO: delete this; write theorem to unfold sdiv?
           split <;> simp
           case inr hsdiv =>
@@ -233,11 +230,10 @@ def alive_simplifyMulDivRem805' (w : Nat) :
   split_ifs with c
   simp
   by_cases w_0 : w = 0; subst w_0; simp [BitVec.eq_nil a]
-  by_cases h : BitVec.ofInt w 3 >ᵤ BitVec.ofInt w 1 + a
+  by_cases h : 3#w >ᵤ 1#w + a
   · simp [h]
-    rw [ofInt_eq_ofNat, ofInt_eq_ofNat] at h
     by_cases a_0 : a = 0; subst a_0; simp at c
-    by_cases a_1 : a = 1; subst a_1; rw [sdiv_one_one]
+    by_cases a_1 : a = 1; subst a_1; simp [sdiv_one_one];
     rw [BitVec.toNat_eq] at a_0 a_1
     simp at a_0 a_1
     by_cases w_1 : w = 1; subst w_1; omega
@@ -254,12 +250,8 @@ def alive_simplifyMulDivRem805' (w : Nat) :
     by_cases a_allones : a = allOnes w
     · have x := sdiv_one_allOnes w_gt_1
       rw [a_allones]
-      have rr : 1#w = BitVec.ofInt w 1 := by rfl
-
-      simp [rr] at x
       simp [x]
-    ·
-      rw [Nat.add_mod_of_add_mod_lt] at h
+    · rw [Nat.add_mod_of_add_mod_lt] at h
       simp [el_one] at h
       omega
       simp [el_one]
@@ -281,13 +273,11 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       simp only [ofNat_eq_ofNat, toNat_ofNat, Nat.zero_mod, toNat_ofInt, Nat.cast_pow,
         Nat.cast_ofNat, toNat_neg] at c
       norm_cast at c
-      simp only [Int.toNat_natCast] at c
       apply c.elim
       by_cases w_1 : w = 1; subst w_1; simp at h
       have w_gt_1 : 1 < w := by omega;
       simp only [BitVec.ult_toNat, toNat_add, toNat_ofInt, decide_eq_false_iff_not] at h
       norm_cast at h
-      simp only [Int.toNat_natCast] at h
       simp only [
         Nat.mod_eq_of_lt (@Nat.pow_le_pow_of_le 2 2 w (by omega) (by omega)),
         Nat.mod_eq_of_lt, ofNat_eq_ofNat, toNat_ofNat, Nat.add_mod_mod,
@@ -301,10 +291,11 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       norm_cast at h
       simp only [Int.toNat_natCast, toNat_allOnes, Nat.mod_add_mod] at h
       by_cases w_1 : w = 1; subst w_1; simp at h
-      rw [Nat.add_sub_of_le (by omega), Nat.mod_self, nonpos_iff_eq_zero] at h
-      rw [Nat.mod_eq_of_lt] at h
-      simp at h
       have et : _ := @Nat.pow_le_pow_of_le 2 2 w (by simp) (by omega)
+      simp only [BitVec.toNat_ofNat] at h
+      rw [Nat.mod_eq_of_lt (by omega), @Nat.mod_eq_of_lt 1 (2^w) (by omega),
+        Nat.add_comm, Nat.sub_add_cancel, Nat.mod_self] at h
+      norm_num at h
       omega
     rw [one_sdiv a_ne_zero a_ne_one a_ne_allOnes]
 
@@ -365,7 +356,6 @@ def alive_simplifyMulDivRem290 (w : Nat) :
   have : (1 % 2^w) = 1 := by
     apply Nat.mod_eq_of_lt
     apply Nat.one_lt_pow <;> omega
-  simp [this]
   ring_nf
 
 /-- info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem290' depends on
@@ -506,12 +496,12 @@ def alive_simplifySelect764 (w : Nat) :
   simp_alive_undef
   intros A
   rcases A with rfl | A  <;> simp [Option.bind, Bind.bind]
-  by_cases zero_sgt_A : BitVec.ofInt w 0 >ₛ A
+  by_cases zero_sgt_A : 0#w >ₛ A
   · simp [zero_sgt_A]
   · simp only [zero_sgt_A, ofBool_false, ofNat_eq_ofNat, sub_sub_cancel]
-    by_cases neg_A_sgt_zero : -A >ₛ BitVec.ofInt w 0
+    by_cases neg_A_sgt_zero : -A >ₛ 0#w
     · simp [neg_A_sgt_zero, zero_sub_eq_neg]
-      by_cases A_sgt_zero : A >ₛ BitVec.ofInt w 0
+      by_cases A_sgt_zero : A >ₛ 0#w
       simp only [A_sgt_zero, ofBool_true, ofNat_eq_ofNat, Refinement.some_some]
       · by_cases A_eq_zero : A = 0
         simp only [A_eq_zero, ofNat_eq_ofNat, BitVec.neg_zero]
@@ -527,7 +517,7 @@ def alive_simplifySelect764 (w : Nat) :
         simp [neg_A_sgt_zero] at A_sgt_zero
       simp [A_sgt_zero]
     · simp [neg_A_sgt_zero, zero_sub_eq_neg]
-      by_cases A_sgt_zero : A >ₛ BitVec.ofInt w 0
+      by_cases A_sgt_zero : A >ₛ 0#w
       · simp [A_sgt_zero]
       · by_cases A_eq_zero : A = 0
         simp only [A_eq_zero, ofNat_eq_ofNat, ofInt_zero_eq, sgt_same, ofBool_false,
@@ -535,7 +525,7 @@ def alive_simplifySelect764 (w : Nat) :
         by_cases A_eq_intMin : A = intMin w
         · simp [A_eq_intMin, BitVec.ofInt_zero_eq, sgt_same, intMin_not_gt_zero,
             intMin_eq_neg_intMin]
-        · have neg_not_sgt_zero : ¬(-A >ₛ BitVec.ofInt w 0) = true → (A >ₛ BitVec.ofInt w 0) = true
+        · have neg_not_sgt_zero : ¬(-A >ₛ 0#w) = true → (A >ₛ 0#w) = true
             := (sgt_zero_eq_not_neg_sgt_zero A A_eq_intMin A_eq_zero).mpr
           apply neg_not_sgt_zero at neg_A_sgt_zero
           simp only at neg_A_sgt_zero
diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 2b1d537d5..8d9d03c4e 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -90,10 +90,10 @@ def toInt_zero_eq (w : Nat) : BitVec.toInt 0#w = 0 := by
  simp [BitVec.toInt]
 def toNat_zero_eq (w : Nat) : BitVec.toNat 0#w = 0 := rfl
 
-def msb_ofInt_one (h : 1 < w): BitVec.msb (BitVec.ofInt w 1) = false := by
+def msb_ofInt_one (h : 1 < w): BitVec.msb 1#w = false := by
   simp only [BitVec.msb_eq_decide, decide_eq_false_iff_not, not_le, toNat_ofInt]
   norm_cast
-  simp only [Int.toNat_natCast]
+  simp only [toNat_ofNat]
   rw [Nat.mod_eq_of_lt] <;> simp <;> omega
 
 @[simp]
@@ -125,6 +125,7 @@ lemma ofInt_ofNat (w n : Nat) :
 
 -- @[simp]
 def msb_one (h : 1 < w) : BitVec.msb (1#w) = false := by
+
   rw [← ofInt_ofNat]
   simp [msb_ofInt_one h]
 
@@ -160,9 +161,7 @@ def sdiv_one_allOnes {w : Nat} (h : 1 < w) :
   simp only [msb_ofInt_one h, neg_eq, @msb_allOnes w (by omega)]
   simp only [neg_allOnes]
   simp only [udiv_one_eq_self]
-  rw [BitVec.msb_one]
   simp only [negOne_eq_allOnes]
-  exact h
 
 theorem width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
   obtain ⟨a, ha⟩ := a
@@ -259,7 +258,7 @@ lemma gt_one_of_neq_0_neq_1 (a : BitVec w) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a >
 
 def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
     (hao : a ≠ allOnes w) :
-    BitVec.sdiv (BitVec.ofInt w 1) a = BitVec.ofInt w 0 := by
+    BitVec.sdiv (1#w) a = 0#w := by
   rcases w with ⟨rfl | ⟨rfl | w⟩⟩
   case zero => simp [BitVec.eq_nil a]
   case succ w' =>
@@ -272,8 +271,7 @@ def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
       unfold BitVec.sdiv
       simp [udiv_one_eq_self, msb_one, ofInt_one_eq_ofNat_one]
       by_cases h : BitVec.msb a <;> simp [h]
-      · simp [BitVec.ofInt_zero_eq]
-        simp only [neg_eq_iff_eq_neg, BitVec.neg_zero]
+      · simp only [neg_eq_iff_eq_neg, BitVec.neg_zero]
         apply BitVec.udiv_one_eq_zero
         apply BitVec.gt_one_of_neq_0_neq_1
         · rw [neg_neq_iff_neq_neg]
@@ -282,11 +280,12 @@ def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
         · rw [neg_neq_iff_neq_neg]
           rw [← negOne_eq_allOnes] at hao
           assumption
-      · simp [BitVec.ofInt_zero_eq]
-        apply BitVec.udiv_one_eq_zero
+      · apply BitVec.udiv_one_eq_zero
         apply BitVec.gt_one_of_neq_0_neq_1 <;> assumption
 
-def sdiv_one_one' (h : 1 < w) : BitVec.sdiv 1#w 1#w = 1#w := by
+def sdiv_one_one : BitVec.sdiv 1#w 1#w = 1#w := by
+  by_cases w_0 : w = 0; subst w_0; rfl
+  by_cases w_1 : w = 1; subst w_1; rfl
   unfold BitVec.sdiv
   unfold BitVec.udiv
   simp only [toNat_ofNat, neg_eq, toNat_neg]
@@ -299,36 +298,6 @@ def sdiv_one_one' (h : 1 < w) : BitVec.sdiv 1#w 1#w = 1#w := by
   apply BitVec.eq_of_toNat_eq
   simp [hone]
 
-def sdiv_one_one : BitVec.sdiv (BitVec.ofInt w 1) 1 = 1 := by
-  by_cases w_0 : w = 0; subst w_0; rfl
-  by_cases w_1 : w = 1; subst w_1; rfl
-  unfold BitVec.sdiv
-  unfold BitVec.udiv
-  simp
-  rw [msb_one (by omega)]
-  rw [msb_ofInt_one (by omega)]
-  simp
-  have ki' : (1) % (2) ^ w = 1 := by
-    rw [Nat.mod_eq_of_lt]
-    simp
-    omega
-  have ki : (1:Int) % (2: Int) ^ w = 1 := by
-    norm_cast
-  simp only [ki]
-  simp only [ki']
-  simp
-  have one : 1 = 1#w := by
-    simp
-  simp only [← one]
-  unfold BitVec.ofNatLt
-  simp
-  unfold BitVec.ofNat
-  unfold Fin.ofNat'
-  simp
-  rw [Nat.mod_eq_of_lt]
-  simp
-  omega
-
 def ofInt_eq_ofNat {a: Nat} :
     BitVec.ofInt w (@OfNat.ofNat ℤ a _) = BitVec.ofNat w a := by
   rfl
@@ -498,7 +467,7 @@ theorem toInt_ne (x y : BitVec n) : x ≠ y ↔ x.toInt ≠ y.toInt := by
   rw [Ne, toInt_eq]
 
 theorem sgt_zero_eq_not_neg_sgt_zero (A : BitVec w) (h_ne_intMin : A ≠ intMin w) (h_ne_zero : A ≠ 0):
-    (A >ₛ BitVec.ofInt w 0) ↔ ¬ ((-A) >ₛ BitVec.ofInt w 0) := by
+    (A >ₛ 0#w) ↔ ¬ ((-A) >ₛ 0#w) := by
   by_cases w0 : w = 0
   · subst w0
     simp [BitVec.eq_nil A] at h_ne_zero

From 726eab5748091099d5fd3bee5e539008522c1d92 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 18:27:02 +0100
Subject: [PATCH 16/18] Fix more

---
 SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 5c95eaf97..9225fd954 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -229,17 +229,11 @@ def alive_simplifyMulDivRem805' (w : Nat) :
   simp
   split_ifs with c
   simp
-  -- TODO: This one does not work: simp [(BitVec.ofInt_ofNat)]
-  simp [(BitVec.ofInt_ofNat')]
   by_cases w_0 : w = 0; subst w_0; simp [BitVec.eq_nil a]
   by_cases h : 3#w >ᵤ 1#w + a
   · simp [h]
     by_cases a_0 : a = 0; subst a_0; simp at c
-<<<<<<< HEAD
     by_cases a_1 : a = 1; subst a_1; simp [sdiv_one_one]
-=======
-    by_cases a_1 : a = 1; subst a_1; simp [sdiv_one_one];
->>>>>>> further_fixes
     rw [BitVec.toNat_eq] at a_0 a_1
     simp at a_0 a_1
     by_cases w_1 : w = 1; subst w_1; omega

From eaa1950805ccb20191689775c11da482099b8169 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 18:27:56 +0100
Subject: [PATCH 17/18] Fix more

---
 SSA/Projects/InstCombine/ForLean.lean | 12 ------------
 1 file changed, 12 deletions(-)

diff --git a/SSA/Projects/InstCombine/ForLean.lean b/SSA/Projects/InstCombine/ForLean.lean
index 99d53eb74..696b80669 100644
--- a/SSA/Projects/InstCombine/ForLean.lean
+++ b/SSA/Projects/InstCombine/ForLean.lean
@@ -93,11 +93,7 @@ def toNat_zero_eq (w : Nat) : BitVec.toNat 0#w = 0 := rfl
 def msb_ofInt_one (h : 1 < w): BitVec.msb 1#w = false := by
   simp only [BitVec.msb_eq_decide, decide_eq_false_iff_not, not_le, toNat_ofInt]
   norm_cast
-<<<<<<< HEAD
-  simp only [BitVec.toNat_ofNat]
-=======
   simp only [toNat_ofNat]
->>>>>>> further_fixes
   rw [Nat.mod_eq_of_lt] <;> simp <;> omega
 
 @[simp]
@@ -131,11 +127,7 @@ lemma ofInt_ofNat' : BitVec.ofInt w (OfNat.ofNat (α := ℤ) x ) = x#w := rfl
 
 -- @[simp]
 def msb_one (h : 1 < w) : BitVec.msb (1#w) = false := by
-<<<<<<< HEAD
-=======
-
   rw [← ofInt_ofNat]
->>>>>>> further_fixes
   simp [msb_ofInt_one h]
 
 -- @[simp]
@@ -267,11 +259,7 @@ lemma gt_one_of_neq_0_neq_1 (a : BitVec w) (ha0 : a ≠ 0) (ha1 : a ≠ 1) : a >
 
 def one_sdiv { w : Nat} {a : BitVec w} (ha0 : a ≠ 0) (ha1 : a ≠ 1)
     (hao : a ≠ allOnes w) :
-<<<<<<< HEAD
-    BitVec.sdiv 1#w a = BitVec.ofInt w 0 := by
-=======
     BitVec.sdiv (1#w) a = 0#w := by
->>>>>>> further_fixes
   rcases w with ⟨rfl | ⟨rfl | w⟩⟩
   case zero => simp [BitVec.eq_nil a]
   case succ w' =>

From 47ef8ed7d1c237cd54286dca6979fbab2024f0d9 Mon Sep 17 00:00:00 2001
From: Tobias Grosser <tobias@grosser.es>
Date: Thu, 30 May 2024 18:44:10 +0100
Subject: [PATCH 18/18] WIP

---
 SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
index 9225fd954..a81d2d433 100644
--- a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
+++ b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -298,7 +298,6 @@ def alive_simplifyMulDivRem805' (w : Nat) :
       norm_num at h
       omega
     rw [one_sdiv a_ne_zero a_ne_one a_ne_allOnes]
-    rfl
 
 /--info: 'AliveHandwritten.MulDivRem.alive_simplifyMulDivRem805'' depends on axioms:
 [propext, Classical.choice, Quot.sound] -/