chore: re-hide bv_automata bug (#663)

The recent update of lean changed the behaviour of ring_nf, which led to
one simp lemma not firing exposing `bv_automata` to a state where it
would throw a bug: #660.
This PR adds a simp-lemma to simplify the offending statement, bringing
our CI back to the state before the recent lean update.

While not urgent anymore, the offending bug should anyhow be fixed at
some point.

.github/workflows/ci-tools.yml

@@ -60,4 +60,4 @@ jobs:
           lake -R exe cache get
           lake build AliveExamples
           (cd SSA/Projects/InstCombine/; ./update_alive_statements.py)
-          # Disabled due to https://github.com/opencompl/lean-mlir/issues/660 - bash -c '! git diff | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash
+          bash -c '! git diff | grep .'  # iff git diff is empty, 'grep .' fails, '!' inverts the failure, and in the forced bash

SSA/Projects/InstCombine/AliveStatements.lean

@@ -102,8 +102,6 @@ theorem bv_AddSub_1556 :
   simp_alive_undef
   simp_alive_ops
   simp_alive_case_bash
-  stop
-  /-issue 660: https://github.com/opencompl/lean-mlir/issues/660-/
   try alive_auto
   all_goals sorry
 

SSA/Projects/InstCombine/ForLean.lean

@@ -160,6 +160,12 @@ theorem width_one_cases (a : BitVec 1) : a = 0#1 ∨ a = 1#1 := by
     subst h
     simp
 
+@[simp]
+lemma sub_eq_xor (a b : BitVec 1) : a - b = a ^^^ b := by
+  have ha : a = 0 ∨ a = 1 := width_one_cases _
+  have hb : b = 0 ∨ b = 1 := width_one_cases _
+  rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))
+
 @[simp]
 lemma add_eq_xor (a b : BitVec 1) : a + b = a ^^^ b := by
   have ha : a = 0 ∨ a = 1 := width_one_cases _