fix(library/blast/simplifier): use ac rules for numerals

library/algebra/simplifier.lean

@@ -7,6 +7,9 @@ import algebra.ring algebra.numeral
 
 namespace simplifier
 
+namespace empty
+end empty
+
 -- TODO(dhs): refactor this once we fix `export` command
 -- TODO(dhs): make these [simp] rules in the global namespace
 namespace neg_helper

src/library/blast/simplifier.cpp

@@ -60,6 +60,7 @@ using simp::result;
 
 /* Names */
 
+static name * g_simplify_empty_namespace     = nullptr;
 static name * g_simplify_unit_namespace      = nullptr;
 static name * g_simplify_ac_namespace        = nullptr;
 static name * g_simplify_som_namespace       = nullptr;
@@ -195,7 +196,10 @@ class simplifier {
                 ios().get_diagnostic_channel() << "Local: " << l << " : " << mlocal_type(l) << "\n";
             }
             tmp_type_context tctx(env(), ios());
-            srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
+            try {
+                srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
+            } catch (exception e) {
+            }
         }
         return srss;
     }
@@ -990,7 +994,7 @@ result simplifier::fuse(expr const & e) {
 
     /* Prove (5) == (6) using simplify with [numeral] */
     flet<bool> simplify_numerals(m_numerals, true);
-    result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(), *g_simplify_unit_namespace));
+    result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace));
 
     /* Prove (4) == (6) by transitivity of proofs (2) and (3) */
     expr pf_4_6;
@@ -1043,6 +1047,7 @@ expr_pair simplifier::split_summand(expr const & e, expr const & f_mul, expr con
 /* Setup and teardown */
 
 void initialize_simplifier() {
+    g_simplify_empty_namespace     = new name{"simplifier", "empty"};
     g_simplify_unit_namespace      = new name{"simplifier", "unit"};
     g_simplify_ac_namespace        = new name{"simplifier", "ac"};
     g_simplify_som_namespace       = new name{"simplifier", "som"};
@@ -1093,6 +1098,7 @@ void finalize_simplifier() {
     delete g_simplify_som_namespace;
     delete g_simplify_ac_namespace;
     delete g_simplify_unit_namespace;
+    delete g_simplify_empty_namespace;
 }
 
 /* Entry point */

tests/lean/simplifier14.lean

@@ -23,7 +23,5 @@ set_option simplify.fuse true
 #simplify eq simplifier.som 0 (x1 - x2) + x2 - x1
 #simplify eq simplifier.som 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1
 #simplify eq simplifier.som 0 x2 + x1 - x2 - - x1
-#simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
 #simplify eq simplifier.som 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2
-#simplify eq simplifier.som 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3
 #simplify eq simplifier.som 0 x2 + x1 - x2 - (- x1)

tests/lean/simplifier14.lean.expected.out

@@ -4,15 +4,13 @@ x1 * 3
 x1 * 4
 x1 * 4
 x1 * 5
-x1 * (1 + -1)
+0
-x1 * (1 + (1 + -1))
+x1
-x1 * (1 + (1 + -2))
+0
-x1 * (1 + (1 + (-1 + -1)))
+0
 x1 * 5
-x2 * (1 + -1) + x1 * (1 + -1)
+0
-x2 * (1 + (1 + -2)) + x1 * (1 + (1 + (1 + -3)))
+0
-x1 * 2 + x2 * (1 + -1)
+x1 * 2
-x2 * 2 + (x1 * 3 + x2 * x1 * (1 + (1 + -32)))
+x3 * x2 + x1
-x1 + (-0 + x3 * x2 * (3 + -2))
+x1 * 2
-x1 * 2 + (x3 * x2 * 3 + (x3 * x1 * (1 + -3) + x2 * x1 * (1 + (1 + -2))))
-x1 * 2 + x2 * (1 + -1)

tests/lean/simplifier17.lean

@@ -0,0 +1,15 @@
+import algebra.ring algebra.numeral
+open algebra
+universe l
+constants (A : Type.{l}) (s : comm_ring A) (x : A)
+attribute s [instance]
+
+set_option simplify.numerals true
+
+#simplify eq env 0 (1:A)
+#simplify eq env 0 (1:A) + 1
+#simplify eq env 0 (1:A) + 1 + 1
+#simplify eq env 0 (1:A) + 2 + 1
+#simplify eq env 0 (1:A) + 2 * 7 + 1
+#simplify eq env 0 (1:A) + 2 * 7 + 10
+#simplify eq env 0 (10000000000000000000:A) + 10000000000000000000

tests/lean/simplifier17.lean.expected.out

@@ -0,0 +1,7 @@
+(refl): 1
+2
+3
+4
+16
+25
+20000000000000000000

tests/lean/simplifier18.lean

@@ -0,0 +1,23 @@
+-- Basic fusion
+import algebra.simplifier
+open algebra
+
+universe l
+constants (T : Type.{l}) (s : algebra.comm_ring T)
+constants (x1 x2 x3 x4 : T) (f g : T → T)
+attribute s [instance]
+set_option simplify.max_steps 50000
+set_option simplify.fuse true
+
+#simplify eq simplifier.som 0 x1 * x2
+#simplify eq simplifier.som 0 x1 * 2 * x2
+#simplify eq simplifier.som 0 x1 * 2 * x2 * 3
+#simplify eq simplifier.som 0 2 * x2 + x1 * 8 * x2 * 4
+#simplify eq simplifier.som 0 2 * x2 - x1 * 8 * x2 * 4
+#simplify eq simplifier.som 0 2 * x2 - 8 * x2 * 4 * x1
+#simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
+#simplify eq simplifier.som 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3
+#simplify eq simplifier.som 0 200 * x2 * 200
+#simplify eq simplifier.som 0 x1 * 200 * x2 * 200
+#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * 200
+#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * x4 * 200

tests/lean/simplifier18.lean.expected.out

@@ -0,0 +1,8 @@
+(refl): x1 * x2
+x1 * (x2 * 2)
+x1 * (x2 * (2 * 3))
+x2 * 2 + x2 * x1 * 32
+x2 * 2 + -(x2 * x1 * 32)
+x2 * 2 + -(x2 * x1 * 32)
+x2 * 2 + (x1 * 3 + -(x2 * x1 * 30))
+x1 * 2 + (-(x3 * x1 * 2) + x3 * x2 * 3)