feat: canonicalize BitVec to arithmetic before running ring_nf (#437)

There are 2 main kinds of operations on BitVecs

1. Boolean operations (^^^, &&&, |||) which are solved by extensionality
2. Arithmetic operations (+, -) which are solved by `ring_nf`

The purpose of this commit is to convert boolean operations to
arithmetic operations and then
solve the arithmetic with the `ring_nf` tactic. See `bitvec_AddSub_1202`
in `SSA/Projects/InstCombine/AliveStatements.lean` for an example of
this.

`bitvec_AddSub_1202` was not solved by the `alive_auto` tactic before
this commit, and now it is solved by the `alive_auto` after this commit.


I added the line

```lean
 try solve | (simp only   [← BitVec.allOnes_sub_eq_xor,  BitVec.negOne_eq_allOnes'];  ring_nf)
```

to the `alive_auto` tactic.

---------

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

SSA/Projects/InstCombine/TacticAuto.lean

@@ -91,6 +91,15 @@ macro "simp_alive_bitvec": tactic =>
                      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.
+        -/
+        try solve | (simp only [← BitVec.allOnes_sub_eq_xor, BitVec.negOne_eq_allOnes']; ring_nf)
       )
    )