feat: upstream a handwritten proof for alive - alive_DivRemOfSelectLa…

…rge proofs one (#262)

* feat: upstream a handwritten proof for alive - alive_DivRemOfSelect

This proof is factored out of #167
and is part of collection of proofs that we manually wrote to demonstrate
the status of leans automation in BitVectors and such.

* chore: golf

* chore: golf more --- intro; rcases -> rintro.

* chore: simp [simp_llvm] -> simp only [simp_llvm]

---------

Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com>

SSA/Projects/InstCombine/Alive.lean

@@ -10,6 +10,7 @@ import SSA.Projects.InstCombine.AliveStatements
 -- This has those examples from alive that failed to be
 -- translated correctly due to bugs in the translator.
 import SSA.Projects.InstCombine.AliveHandwrittenExamples
+import SSA.Projects.InstCombine.AliveHandwrittenLargeExamples
 
 -- The semantics for the MLIR base dialect
 import SSA.Projects.InstCombine.Base

SSA/Projects/InstCombine/AliveHandwrittenLargeExamples.lean

@@ -0,0 +1,53 @@
+import SSA.Projects.InstCombine.LLVM.EDSL
+import SSA.Projects.InstCombine.Tactic
+
+open BitVec
+open MLIR AST
+
+namespace AliveHandwritten
+
+namespace DivRemOfSelect
+
+/--
+Name: SimplifyDivRemOfSelect
+precondition: true
+%sel = select %c, %Y, 0
+%r = udiv %X, %sel
+  =>
+%r = udiv %X, %Y
+-/
+def alive_DivRemOfSelect_src (w : Nat) :=
+  [alive_icom (w)| {
+  ^bb0(%c: i1, %y : _, %x : _):
+    %c0 = "llvm.mlir.constant" () { value = 0 : _ } :() -> (_)
+    %v1 = "llvm.select" (%c,%y, %c0) : (i1, _, _) -> (_)
+    %v2 = "llvm.udiv"(%x, %v1) : (_, _) -> (_)
+    "llvm.return" (%v2) : (_) -> ()
+  }]
+
+def alive_DivRemOfSelect_tgt (w : Nat) :=
+  [alive_icom (w)| {
+  ^bb0(%c: i1, %y : _, %x : _):
+    %v1 = "llvm.udiv" (%x,%y) : (_, _) -> (_)
+    "llvm.return" (%v1) : (_) -> ()
+  }]
+
+theorem alive_DivRemOfSelect (w : Nat) :
+    alive_DivRemOfSelect_src w ⊑ alive_DivRemOfSelect_tgt w := by
+  unfold alive_DivRemOfSelect_src alive_DivRemOfSelect_tgt
+  simp_alive_ssa
+  simp_alive_undef
+  simp only [simp_llvm]
+  rintro y (rfl | ⟨vcond, hcond⟩) x
+  -- | select condition is itself `none`, nothing more to be done. propagate the `none`.
+  · cases x <;> cases y <;> simp
+  · simp at hcond
+    (obtain (rfl | rfl) : vcond = 1 ∨ vcond = 0 := by omega) <;> simp
+
+/--info: 'AliveHandwritten.DivRemOfSelect.alive_DivRemOfSelect' depends on
+axioms: [propext, Classical.choice, Quot.sound] -/
+#guard_msgs in #print axioms alive_DivRemOfSelect
+
+end DivRemOfSelect
+
+end AliveHandwritten