chore: use simp-normal form in LLVM.select (#760)

This simplifies:

```lean
⊢ ∀ (x : BitVec 8),
  ((if false = true ∧ x >>> 7#8 <<< 7#8 ≠ x then none
        else if 7#8 ≥ ↑8 then none else some (x.sshiftRight (7#8).toNat)).bind
      fun x' => some (x'.xor 127#8)) ⊑
    match some (ofBool (x >ₛ -1#8)) with
    | none => none
    | some { toFin := ⟨1, ⋯⟩ } => some 127#8
    | some { toFin := ⟨0, ⋯⟩ } => some 128#8
```

```lean
∀ (x : BitVec 8),
  ((if false = true ∧ x >>> 7#8 <<< 7#8 ≠ x then none
        else if 7#8 ≥ ↑8 then none else some (x.sshiftRight (7#8).toNat)).bind
      fun x' => some (x'.xor 127#8)) ⊑
    match ofBool (x >ₛ -1#8) with
    | 1#1 => some 127#8
    | 0#1 => some 128#8
```

In particular, we manage to get rid of the `some` in the match and do
not have the annoying `{ toFin := ⟨1, ⋯⟩ } ` but instead just `1#1`. We
probably want to get rid of the match entirely and replace it by an
`if`, but this seems to have side-effects require further investigation.

SSA/Projects/InstCombine/AliveHandwrittenExamples.lean

@@ -42,6 +42,9 @@ theorem alive_DivRemOfSelect (w : Nat) :
     alive_DivRemOfSelect_src w ⊑ alive_DivRemOfSelect_tgt w := by
   unfold alive_DivRemOfSelect_src alive_DivRemOfSelect_tgt
   simp_alive_peephole
+  simp_alive_undef
+  simp_alive_ops
+  simp_alive_case_bash
   alive_auto
 
 end AliveHandwritten

SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean

@@ -151,8 +151,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
         have htwopow_pos : 2^w'' > 0 := Nat.pow_pos (by omega)
         rw [Nat.mod_eq_of_lt (a := 3) (by omega)]
         split
-        case h_1 c hugt => contradiction
-        case h_2 c hugt =>
+        case h_1 c hugt =>
           clear c
           have hugt :
             (1 + BitVec.toNat x) % 2 ^ Nat.succ (Nat.succ w'') < 3 := by
@@ -191,7 +190,7 @@ def alive_simplifyMulDivRem805 (w : Nat) :
                 subst heqzero
                 simp [BitVec.sdiv_zero]
           · exact intMin_neq_one (by omega)
-        case h_3 c hugt =>
+        case h_2 c hugt =>
           clear c
           simp only [toNat_add, toNat_ofNat, Nat.mod_add_mod, Nat.reducePow, Fin.zero_eta,
             Fin.isValue, ofFin_ofNat, ofNat_eq_ofNat, Option.some.injEq,

SSA/Projects/InstCombine/LLVM/Semantics.lean

@@ -406,11 +406,11 @@ def ashr {w : Nat} (x y : IntW w) (flag : ExactFlag := {exact := false}) : IntW
  If the condition is an i1 and it evaluates to 1, the instruction returns the first value argument; otherwise, it returns the second value argument.
 -/
 @[simp_llvm_option]
-def select {w : Nat} (c? : IntW 1) (x? y? : IntW w ) : IntW w :=
-  match c? with
-  | none => none
-  | some true => x?
-  | some false => y?
+def select {w : Nat} (c? : IntW 1) (x? y? : IntW w ) : IntW w := do
+  let c ← c?
+  match c with
+  | 1#1 => x?
+  | 0#1 => y?
 
 inductive IntPredicate where
   | eq