chore: bash the proof a bit

opencompl · Apr 29, 2024 · 6b28ed9 · 6b28ed9
1 parent 36c1185
commit 6b28ed9
Showing 1 changed file with 6 additions and 8 deletions.
diff --git a/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean b/SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean
@@ -97,17 +97,15 @@ def alive_simplifyAndOrXor2515 (w : Nat) :
   simp_alive_ssa
   simp_alive_undef
   intros c1 c2 c3 x
-  rcases c1 with none | c1 <;>
-  rcases c2 with none | c2 <;>
-  rcases c3 with none | c3 <;>
-  rcases x with none | x <;>
-  simp only [LLVM.xor?_eq, xor_eq, Option.bind_eq_bind, Option.none_bind, Option.bind_none,
-    Option.some_bind, Refinement.refl]
+  rcases c1 with none | c1 <;> try simp
+  rcases c2 with none | c2 <;> try simp
+  rcases c3 with none | c3 <;> try simp
+  rcases x with none | x <;> try simp
   rw [←Option.bind_eq_bind]
   simp_alive_ops
-  by_cases h : w ≤ BitVec.toNat c2 <;>
+  by_cases h : BitVec.toNat c2 ≥ w <;>
   simp only [ge_iff_le, h, ↓reduceIte, Option.bind_eq_bind, Option.none_bind, Option.bind_none,
-    Refinement.refl, Option.some_bind, h, Option.pure_def, Option.some_bind, Refinement.some_some]
+    Refinement.refl, Option.pure_def, Option.some_bind, Refinement.some_some]
   simp only [ushr_xor_distrib, xor_assoc]
 
 /-- info: 'AliveHandwritten.AndOrXor.alive_simplifyAndOrXor2515' depends on