Make bv_automata fallible (#673)

Same as #670 but from a branch on the main repo.

SSA/Experimental/Bits/Fast/Tactic.lean

@@ -8,7 +8,6 @@ open Lean Elab Tactic
 open Lean Meta
 open scoped Qq
 
-
 /-!
 # BitVec Automata Tactic
 There are two ways of expressing BitVec expressions. One is:
@@ -296,6 +295,40 @@ def introduceMapIndexToFVar : TacticM Unit := withMainContext <|  do
 
 elab "introduceMapIndexToFVar" : tactic => introduceMapIndexToFVar
 
+/- Copy-pasted from Lean/Elab/Tactic/ElabTerm.lean
+-/
+
+private def preprocessPropToDecide (expectedType : Expr) : TermElabM Expr := do
+  let mut expectedType ← instantiateMVars expectedType
+  if expectedType.hasFVar then
+    expectedType ← zetaReduce expectedType
+  if expectedType.hasFVar || expectedType.hasMVar then
+    throwError "expected type must not contain free or meta variables{indentExpr expectedType}"
+  return expectedType
+
+private def mkNativeAuxDecl (baseName : Name) (type value : Expr) : TermElabM Name := do
+  let auxName ← Term.mkAuxName baseName
+  let decl := Declaration.defnDecl {
+    name := auxName, levelParams := [], type, value
+    hints := .abbrev
+    safety := .safe
+  }
+  addDecl decl
+  compileDecl decl
+  pure auxName
+
+elab "safe_native_decide" : tactic =>
+  Lean.Elab.Tactic.closeMainGoalUsing `safeNativeDecide fun expectedType => do
+    let expectedType ← preprocessPropToDecide expectedType
+    let d ← mkDecide expectedType
+    let auxDeclName ← mkNativeAuxDecl `_nativeDecide (Lean.mkConst `Bool) d
+    -- new lines
+    unless ← reduceBoolNative auxDeclName do
+      throwError "The statement is false"
+    let rflPrf ← mkEqRefl (toExpr true)
+    let s := d.appArg! -- get instance from `d`
+    return mkApp3 (Lean.mkConst ``of_decide_eq_true) expectedType s <| mkApp3 (Lean.mkConst ``Lean.ofReduceBool) (Lean.mkConst auxDeclName) (toExpr true) rflPrf
+
 /--
 Create bv_automata tactic which solves equalities on bitvectors.
 -/
@@ -322,7 +355,7 @@ macro "bv_automata" : tactic =>
   intros _ _
   apply congrFun
   apply congrFun
-  native_decide
+  safe_native_decide
   ))
 
 /-!
@@ -337,6 +370,10 @@ info: 'alive_1' depends on axioms: [propext, sorryAx, Classical.choice, Lean.ofR
 -/
 #guard_msgs in #print axioms alive_1
 
+def false_statement {w : ℕ} (x y : BitVec w) : x = y := by
+  try bv_automata
+  sorry
+
 def test_OfNat_ofNat (x : BitVec 1) : 1 + x = x + 1 := by
   bv_automata
 

SSA/Projects/InstCombine/ForLean.lean

@@ -183,12 +183,6 @@ 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 _