feat: hoist into separate file called AliveDemo

SSA/Projects/InstCombine/AliveDemo.lean

@@ -0,0 +1,104 @@
+import SSA.Projects.InstCombine.LLVM.EDSL
+import SSA.Projects.InstCombine.AliveStatements
+import SSA.Projects.InstCombine.Refinement
+import SSA.Projects.InstCombine.Tactic
+import SSA.Projects.InstCombine.TacticAuto
+
+open MLIR AST
+open Std (BitVec)
+open Ctxt (Var)
+
+namespace AliveAutoGenerated
+set_option pp.proofs false
+set_option pp.proofs.withType false
+set_option linter.deprecated false
+
+
+-- Name:AddSub:1176
+-- precondition: true
+/-
+  %nb = sub 0, %b
+  %c = add %a, %nb
+
+=>
+  %nb = sub 0, %b
+  %c = sub %a, %b
+
+-/
+def alive_AddSub_1176_src  (w : Nat)   :=
+[alive_icom ( w )| {
+^bb0(%a : _, %b : _):
+  %v1 = "llvm.mlir.constant" () { value = 0 : _ } :() -> (_)
+  %v2 = "llvm.sub" (%v1,%b) : (_, _) -> (_)
+  %v3 = "llvm.add" (%a,%v2) : (_, _) -> (_)
+  "llvm.return" (%v3) : (_) -> ()
+}]
+
+def alive_AddSub_1176_tgt  (w : Nat)  :=
+[alive_icom ( w )| {
+^bb0(%a : _, %b : _):
+  %v1 = "llvm.mlir.constant" () { value = 0 : _ } :() -> (_)
+  %v2 = "llvm.sub" (%v1,%b) : (_, _) -> (_)
+  %v3 = "llvm.sub" (%a,%b) : (_, _) -> (_)
+  "llvm.return" (%v3) : (_) -> ()
+}]
+
+theorem bitvec_AddSub_1176 :
+ ∀ (w : Nat) (a b : BitVec w), a + (0 - b) = a - b
+:= by alive_auto
+      done --ring
+
+theorem alive_AddSub_1176  (w : Nat)   : alive_AddSub_1176_src w  ⊑ alive_AddSub_1176_tgt w  := by
+  unfold alive_AddSub_1176_src alive_AddSub_1176_tgt
+  simp_alive_peephole
+  apply bitvec_AddSub_1176
+
+
+-- Name:AndOrXor:1230  ~A & ~B -> ~(A | B)
+-- precondition: true
+/-
+  %op0 = xor %notOp0, -1
+  %op1 = xor %notOp1, -1
+  %r = and %op0, %op1
+
+=>
+  %or = or %notOp0, %notOp1
+  %op0 = xor %notOp0, -1
+  %op1 = xor %notOp1, -1
+  %r = xor %or, -1
+
+-/
+def alive_AndOrXor_1230__A__B___A__B_src  (w : Nat)   :=
+[alive_icom ( w )| {
+^bb0(%notOp0 : _, %notOp1 : _):
+  %v1 = "llvm.mlir.constant" () { value = -1 : _ } :() -> (_)
+  %v2 = "llvm.xor" (%notOp0,%v1) : (_, _) -> (_)
+  %v3 = "llvm.mlir.constant" () { value = -1 : _ } :() -> (_)
+  %v4 = "llvm.xor" (%notOp1,%v3) : (_, _) -> (_)
+  %v5 = "llvm.and" (%v2,%v4) : (_, _) -> (_)
+  "llvm.return" (%v5) : (_) -> ()
+}]
+
+def alive_AndOrXor_1230__A__B___A__B_tgt  (w : Nat)  :=
+[alive_icom ( w )| {
+^bb0(%notOp0 : _, %notOp1 : _):
+  %v1 = "llvm.or" (%notOp0,%notOp1) : (_, _) -> (_)
+  %v2 = "llvm.mlir.constant" () { value = -1 : _ } :() -> (_)
+  %v3 = "llvm.xor" (%notOp0,%v2) : (_, _) -> (_)
+  %v4 = "llvm.mlir.constant" () { value = -1 : _ } :() -> (_)
+  %v5 = "llvm.xor" (%notOp1,%v4) : (_, _) -> (_)
+  %v6 = "llvm.mlir.constant" () { value = -1 : _ } :() -> (_)
+  %v7 = "llvm.xor" (%v1,%v6) : (_, _) -> (_)
+  "llvm.return" (%v7) : (_) -> ()
+}]
+
+theorem bitvec_AndOrXor_1230__A__B___A__B :
+ ∀ (w : Nat) (notOp0 notOp1 : BitVec w), (notOp0 ^^^ -1) &&& (notOp1 ^^^ -1) = (notOp0 ||| notOp1) ^^^ -1
+:= by alive_auto
+      done --ext
+
+theorem alive_AndOrXor_1230__A__B___A__B  (w : Nat)   : alive_AndOrXor_1230__A__B___A__B_src w  ⊑ alive_AndOrXor_1230__A__B___A__B_tgt w  := by
+  unfold alive_AndOrXor_1230__A__B___A__B_src alive_AndOrXor_1230__A__B___A__B_tgt
+  simp_alive_peephole
+  apply bitvec_AndOrXor_1230__A__B___A__B
+