Feat: Change Tactic Auto (#448)

Pair programming with @bollu. Made several changes.

1. Added formatting and indentation to `TacticAuto.lean`.
2. Changed the ordering of the `bool -> arithmetic` tactic, so that we
solve 1 more statement (went from 35 to 34).

---------

Co-authored-by: Tobias Grosser <[email protected]>
Co-authored-by: Atticus Kuhn <[email protected]>

SSA/Projects/InstCombine/TacticAuto.lean

@@ -85,21 +85,30 @@ macro "simp_alive_bitvec": tactic =>
         intros
         simp (config := {failIfUnchanged := false}) [(BitVec.negOne_eq_allOnes')]
         try ring_nf
-        try solve | (ext; simp [BitVec.negOne_eq_allOnes, BitVec.allOnes_sub_eq_xor];
-                     try cases BitVec.getLsb _ _ <;> try simp;
-                     try cases BitVec.getLsb _ _ <;> try simp;
-                     try cases BitVec.getLsb _ _ <;> try simp;
-                     try cases BitVec.getLsb _ _ <;> try simp;)
-        try solve | (simp [bv_ofBool])
         /-
-        There are 2 main kinds of operations on BitVecs
-        1. Boolean operations (^^^, &&&, |||) which can be solved by extensionality.
-        2. Arithmetic operations (+, -) which can be solved by `ring_nf`.
-        The purpose of the below line is to convert boolean
-        operations to arithmetic operations and then
-        solve the arithmetic with the `ring_nf` tactic.
+        Solve tries each arm in order, falling through
+        if the goal is not closed.
+        Note that all goals are tried with the original state
+        (i.e. backtracking semantics).
         -/
-        try solve | (simp only [← BitVec.allOnes_sub_eq_xor, BitVec.negOne_eq_allOnes']; ring_nf)
+        try solve
+          | ext; simp [BitVec.negOne_eq_allOnes, BitVec.allOnes_sub_eq_xor];
+            try cases BitVec.getLsb _ _ <;> try simp
+            try cases BitVec.getLsb _ _ <;> try simp
+            try cases BitVec.getLsb _ _ <;> try simp
+            try cases BitVec.getLsb _ _ <;> try simp
+          | simp [bv_ofBool]
+          /-
+          There are 2 main kinds of operations on BitVecs
+          1. Boolean operations (^^^, &&&, |||) which can be solved by extensionality.
+          2. Arithmetic operations (+, -) which can be solved by `ring_nf`.
+          The purpose of the below line is to convert boolean
+          operations to arithmetic operations and then
+          solve the arithmetic with the `ring_nf` tactic.
+          -/
+          | simp only [← BitVec.allOnes_sub_eq_xor]
+            simp only [← BitVec.negOne_eq_allOnes']
+            ring_nf
       )
    )