chore: make proof more robust

opencompl · Apr 29, 2024 · 3c60de9 · 3c60de9
1 parent 7180e9b
commit 3c60de9
Showing 1 changed file with 4 additions and 7 deletions.
diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -1204,9 +1204,7 @@ def trsa' {A B : BitVec w} (h : BitVec.toNat B < w):
     simp
     omega
   ·
-    rw [Nat.mod_eq_of_lt]
-    rw [Nat.mod_eq_of_lt]
-    rw [Nat.mod_eq_of_lt]
+    repeat (rw [Nat.mod_eq_of_lt])
     ring_nf
     simp [sn]
     simp at h
@@ -1216,8 +1214,7 @@ def trsa' {A B : BitVec w} (h : BitVec.toNat B < w):
     ring_nf
     simp [sn]
     simp at h
-    simp only [h]
-    simp
+    simp [h]
   · simp
     ring_nf
 
@@ -1237,8 +1234,8 @@ def alive_simplifyMulDivRem290 (w : Nat) :
   simp_alive_undef
   simp_alive_ops
   intros A B
-  rcases A with none | A  <;> simp [Option.bind, Bind.bind] <;>
-  rcases B with none | B  <;> simp [Option.bind, Bind.bind] <;>
+  rcases A with none | A  <;> (try (simp [Option.bind, Bind.bind]; done)) <;>
+  rcases B with none | B  <;> (try (simp [Option.bind, Bind.bind]; done)) <;>
   by_cases h : w ≤ BitVec.toNat B <;> simp [h]
   rw [trsa]
   omega