Use ring to solve Alive theorems (#134)

* Use `ring` to solve Alive theorems * Update mathlib version to new `bitvec-ring` branch * Mark `ring`-solvable theorems with `done` * fix: fix FHE proofs after mathlib bump. --------- Co-authored-by: Siddharth Bhat <[email protected]>
opencompl · Nov 13, 2023 · 1fc339f · 1fc339f
1 parent b51dfa6
commit 1fc339f
Show file tree

Hide file tree

Showing 7 changed files with 35 additions and 30 deletions.
diff --git a/SSA/Projects/FullyHomomorphicEncryption/Basic.lean b/SSA/Projects/FullyHomomorphicEncryption/Basic.lean
@@ -304,7 +304,7 @@ theorem sub_modByMonic (a b mod : (ZMod q)[X]) : (a - b) %ₘ mod = a %ₘ mod -
   ring_nf
   repeat rw[sub_eq_add_neg]
   simp[Polynomial.add_modByMonic]
-  rw[neg_modByMonic]
+  rw[Polynomial.neg_modByMonic]
 
 /-- Representative is an multiplicative homomorphism upto modulo -/
 @[simp]
@@ -325,6 +325,7 @@ theorem R.representative_mul [Fact (q > 1)] (a b : R q n) : (a * b).representati
   repeat rw[Polynomial.add_modByMonic]
   ring_nf
   repeat rw[sub_modByMonic]
+  simp
 
   have H1 : (-(a' * f q n * (b' /ₘ f q n))) %ₘ f q n = 0 := by
     rw[Polynomial.dvd_iff_modByMonic_eq_zero (hq := f_monic q n)]

diff --git a/SSA/Projects/InstCombine/AliveStatements.lean b/SSA/Projects/InstCombine/AliveStatements.lean
@@ -1,4 +1,5 @@
 import Std.Data.BitVec
+import Mathlib.Data.StdBitVec.Lemmas
 
 import SSA.Projects.InstCombine.TacticAuto
 import SSA.Projects.InstCombine.ForStd
@@ -27,17 +28,17 @@ theorem bitvec_AddSub_1156 :
 theorem bitvec_AddSub_1164 :
  ∀ (w : Nat) (a b : BitVec w), 0 - a + b = b - a
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1165 :
  ∀ (w : Nat) (a b : BitVec w), 0 - a + (0 - b) = 0 - (a + b)
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1176 :
  ∀ (w : Nat) (a b : BitVec w), a + (0 - b) = a - b
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1202 :
  ∀ (w : Nat) (x C : BitVec w), (x ^^^ -1) + C = C - 1 - x
@@ -57,12 +58,12 @@ theorem bitvec_AddSub_1309 :
 theorem bitvec_AddSub_1539 :
  ∀ (w : Nat) (a x : BitVec w), x - (0 - a) = x + a
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1539_2 :
  ∀ (w : Nat) (x C : BitVec w), x - C = x + -C
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1556:
  ∀ (y x : BitVec 1), x - y = x ^^^ y
@@ -82,17 +83,17 @@ theorem bitvec_AddSub_1564 :
 theorem bitvec_AddSub_1574 :
  ∀ (w : Nat) (X C C2 : BitVec w), C - (X + C2) = C - C2 - X
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1614 :
  ∀ (w : Nat) (Y X : BitVec w), X - (X + Y) = 0 - Y
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1619 :
  ∀ (w : Nat) (Y X : BitVec w), X - Y - X = 0 - Y
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_AddSub_1624 :
  ∀ (w : Nat) (A B : BitVec w), (A ||| B) - (A ^^^ B) = A &&& B
@@ -362,7 +363,7 @@ theorem bitvec_AndOrXor_2663 :
 theorem bitvec_152 :
  ∀ (w : Nat) (x : BitVec w), x * -1 = 0 - x
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_160:
  ∀ (x C1 C2 : BitVec 7), x <<< C2 * C1 = x * C1 <<< C2
@@ -372,7 +373,7 @@ theorem bitvec_160:
 theorem bitvec_229 :
  ∀ (w : Nat) (X C1 Op1 : BitVec w), (X + C1) * Op1 = X * Op1 + C1 * Op1
 := by alive_auto
-      try sorry
+      done
 
 theorem bitvec_239 :
  ∀ (w : Nat) (Y X : BitVec w), (0 - X) * (0 - Y) = X * Y
@@ -533,5 +534,5 @@ theorem bitvec_InstCombineShift__582 :
 
 theorem bitvec_InstCombineShift__724:
  ∀ (A C2 C1 : BitVec 31), C1 <<< A <<< C2 = C1 <<< C2 <<< A
-
-:=sorry
+:= by alive_auto
+      try sorry
diff --git a/SSA/Projects/InstCombine/TacticAuto.lean b/SSA/Projects/InstCombine/TacticAuto.lean
@@ -1,7 +1,10 @@
+import Mathlib.Tactic.Ring
+
 macro "alive_auto": tactic =>
   `(tactic|
       (
-        skip; --placeholder, as `simp` will currently timeout sometimes
-        try simp (config := {decide := false})
+        intros
+        (try simp (config := {decide := false}) [-Std.BitVec.ofNat_eq_ofNat])
+        try ring_nf
       )
    )
diff --git a/lake-manifest.json b/lake-manifest.json
@@ -2,14 +2,6 @@
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/leanprover-community/mathlib4",
-    "subDir?": null,
-    "rev": "9eb5aaff128911772f3564ce032b44a94d5f8ba7",
-    "opts": {},
-    "name": "mathlib",
-    "inputRev?": "9eb5aaff128911772f3564ce032b44a94d5f8ba7",
-    "inherited": false}},
-  {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
     "subDir?": null,
     "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
@@ -25,36 +17,44 @@
     "name": "partax",
     "inputRev?": "master",
     "inherited": false}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/mathlib4",
+    "subDir?": null,
+    "rev": "3b5350301929a51585dedea497e172a23e4a4485",
+    "opts": {},
+    "name": "mathlib",
+    "inputRev?": "bitvec-ring",
+    "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "fb56324020c8e4f3d451e8901b290dea82c072ae",
+    "rev": "fb07d160aff0e8bdf403a78a5167fc7acf9c8227",
     "opts": {},
     "name": "std",
     "inputRev?": "main",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "rev": "511eb96eca98a7474683b8ae55193a7e7c51bc39",
     "opts": {},
     "name": "Qq",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/aesop",
     "subDir?": null,
-    "rev": "9dc4a1097a690216eaa7cf2d2290efd447e60d7a",
+    "rev": "cb87803274405db79ec578fc07c4730c093efb90",
     "opts": {},
     "name": "aesop",
     "inputRev?": "master",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover-community/ProofWidgets4",
     "subDir?": null,
-    "rev": "5382e38eca1e2537d75d4c4705a9e744424b0037",
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.19",
+    "inputRev?": "v0.0.21",
     "inherited": true}}],
  "name": "SSA"}
diff --git a/lakefile.lean b/lakefile.lean
@@ -37,7 +37,7 @@ lean_exe mlirnatural {
 
 -- NOTE: this must be 'm'mathlib, as indicated from:
 --  https://github.com/leanprover-community/mathlib4#using-mathlib4-as-a-dependency
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "9eb5aaff128911772f3564ce032b44a94d5f8ba7"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "bitvec-ring"
 
 require Cli from git "https://github.com/mhuisi/lean4-cli.git" @ "nightly"
 

diff --git a/lakefile.olean b/lakefile.olean
diff --git a/lean-toolchain b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.2.0-rc4
+leanprover/lean4:v4.3.0-rc1