chore: canonicalize constants

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]
 
@@ -361,11 +352,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
@@ -506,12 +492,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,15 +513,15 @@ 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,
           BitVec.neg_zero, Refinement.refl]
         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