Implement Full Alive Translation (#126)

* wip: implement alive translation

* add simp lemma for -1

* haven't seen this one before: failed to compile pattern match

```
./././SSA/Projects/InstCombine/LLVM/Transform.lean:411:8: error: failed to compile pattern matching, stuck at
  remaining variables: [val✝:(String)]
  alternatives:
    [] |- ["eq"] => h_1 ()
  examples:(some _)
```

* add support for icmp.*

* toString instances

* TODO: we should delete mkOpExpr, and add special handlers for each of the cases handled there. Add special handling for icmp making

* add support for copy, select

* feat: add working version of AliveAutoGenerated, with code that doesn't yet work 'sorry'd out

* fix: add proof of bitvec fact

* fixup diff nits

* add new alive commit

* remove 'dsimp' as it was causing the proof state to explode

SSA/Core/Util/ConcreteOrMVar.lean

@@ -11,6 +11,10 @@ inductive ConcreteOrMVar (α : Type u) (φ : Nat)
   | mvar (i : Fin φ)
   deriving DecidableEq, Repr, Inhabited
 
+instance [ToString α] : ToString (ConcreteOrMVar α n) where
+  toString
+  | .concrete a => s!"concrete({a})"
+  | .mvar i => s!"mvar({i})"
 /-- A coercion from the concrete type `α` to the `ConcreteOrMVar` -/
 instance : Coe α (ConcreteOrMVar α φ) := ⟨.concrete⟩
 
@@ -42,4 +46,4 @@ def instantiate (as : Vector α φ) : ConcreteOrMVar α φ → α
   | .mvar i => as.get i
 
 
-end ConcreteOrMVar
+end ConcreteOrMVar

SSA/Projects/InstCombine/Alive.lean

@@ -1,8 +1,11 @@
 
 -- Auto generated alive statements
-import SSA.Projects.InstCombine.AliveAutoGenerated
+-- Do not import these into the default tree, because they take a long
+-- time to elaborate and typecheck.
+-- import SSA.Projects.InstCombine.AliveAutoGenerated
 
--- Pure math statements needed to proof alive statements
+-- Pure math statements needed to prove alive statements.
+-- Include these, as they are reasonably fast to typecheck.
 import SSA.Projects.InstCombine.AliveStatements
 
 -- The semantics for the MLIR base dialect