From a04c28d4c92f8bf95c69b14b71bfbfcf11fe438a Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Fri, 4 Dec 2015 17:57:03 -0800 Subject: [PATCH] refactor(library/algebra): construct simplifier sets incrementally --- library/algebra/group.lean | 27 ++++ library/algebra/ring.lean | 22 ++++ library/algebra/simplifier.lean | 123 ------------------ library/init/simplifier.lean | 7 + .../blast/simplifier/simp_rule_set.cpp | 14 ++ src/library/blast/simplifier/simp_rule_set.h | 3 +- src/library/blast/simplifier/simplifier.cpp | 34 +++-- tests/lean/simplifier12.lean | 8 +- tests/lean/simplifier14.lean | 36 ++--- tests/lean/simplifier15.lean | 2 +- tests/lean/simplifier18.lean | 36 ++--- tests/lean/simplifier19.lean | 6 +- tests/lean/simplifier_light.lean | 6 +- tests/lean/simplifier_norm_num.lean | 10 +- .../simplifier_norm_num.lean.expected.out | 1 + 15 files changed, 152 insertions(+), 183 deletions(-) delete mode 100644 library/algebra/simplifier.lean diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 7369f4cb6..03271ba20 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -580,3 +580,30 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A := mul_left_inv := add.left_inv⦄ end algebra + +namespace simplifier + +namespace unit +attribute algebra.zero_add [simp] +attribute algebra.add_zero [simp] + +attribute algebra.one_mul [simp] +attribute algebra.mul_one [simp] +end unit + +namespace neg +attribute algebra.neg_neg [simp] +attribute algebra.sub_eq_add_neg [simp] +end neg + +namespace ac +attribute algebra.add.assoc [simp] +attribute algebra.add.comm [simp] +attribute algebra.add.left_comm [simp] + +attribute algebra.mul.left_comm [simp] +attribute algebra.mul.comm [simp] +attribute algebra.mul.assoc [simp] +end ac + +end simplifier diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index a1fec765a..80a157b0a 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -195,6 +195,9 @@ section rewrite [-left_distrib, add.right_inv, mul_zero] end + theorem neg_mul_eq_neg_mul_symm : - a * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul + theorem neg_mul_eq_mul_neg_symm : a * - b = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg + theorem neg_mul_neg : -a * -b = a * b := calc -a * -b = -(a * -b) : by rewrite -neg_mul_eq_neg_mul @@ -402,3 +405,22 @@ section end end algebra + +namespace simplifier + +namespace unit +attribute algebra.zero_mul [simp] +attribute algebra.mul_zero [simp] +end unit + +namespace neg +attribute algebra.neg_mul_eq_neg_mul_symm [simp] +attribute algebra.neg_mul_eq_mul_neg_symm [simp] +end neg + +namespace distrib +attribute algebra.left_distrib [simp] +attribute algebra.right_distrib [simp] +end distrib + +end simplifier diff --git a/library/algebra/simplifier.lean b/library/algebra/simplifier.lean deleted file mode 100644 index e76698252..000000000 --- a/library/algebra/simplifier.lean +++ /dev/null @@ -1,123 +0,0 @@ -/- -Copyright (c) 2015 Daniel Selsam. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Author: Daniel Selsam --/ -import algebra.ring algebra.numeral - -namespace simplifier - -namespace empty -end empty - -namespace iff -attribute eq_self_iff_true [simp] -end iff - --- TODO(dhs): make these [simp] rules in the global namespace -namespace neg_helper - open algebra - variables {A : Type} [s : ring A] (a b : A) - include s - lemma neg_mul1 : (- a) * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul - lemma neg_mul2 : a * (- b) = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg - lemma sub_def : a - b = a + (- b) := rfl -end neg_helper - -namespace neg -attribute neg_helper.neg_mul1 [simp] -attribute neg_helper.neg_mul2 [simp] -attribute neg_helper.sub_def [simp] -attribute algebra.neg_neg [simp] -end neg - -namespace unit -attribute algebra.zero_add [simp] -attribute algebra.add_zero [simp] - -attribute algebra.zero_mul [simp] -attribute algebra.mul_zero [simp] - -attribute algebra.one_mul [simp] -attribute algebra.mul_one [simp] -end unit - -namespace ac -export simplifier.iff simplifier.neg simplifier.unit - -attribute algebra.add.assoc [simp] -attribute algebra.add.comm [simp] -attribute algebra.add.left_comm [simp] - -attribute algebra.mul.left_comm [simp] -attribute algebra.mul.comm [simp] -attribute algebra.mul.assoc [simp] - -end ac - -namespace distrib -attribute algebra.left_distrib [simp] -attribute algebra.right_distrib [simp] -end distrib - -namespace som -export simplifier.ac simplifier.distrib -end som - -namespace numeral - --- TODO(dhs): remove `add1` from the original lemmas and delete this -namespace numeral_helper -open algebra - -theorem bit1_add_bit1 {A : Type} [s : add_comm_semigroup A] - [s' : has_one A] (a b : A) : bit1 a + bit1 b = bit0 ((a + b) + 1) - := norm_num.bit1_add_bit1 a b - -theorem bit1_add_one {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A) - : bit1 a + one = bit0 (a + 1) := norm_num.add1_bit1 a - -theorem one_add_bit1 {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A) - : one + bit1 a = bit0 (a + 1) := by rewrite [!add.comm, bit1_add_one] - -lemma one_add_bit0 [simp] {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A) - : 1 + bit0 a = bit1 a := norm_num.one_add_bit0 a - -lemma bit0_add_one [simp] {A : Type} [s : add_comm_semigroup A] [s' : has_one A] (a : A) - : bit0 a + 1 = bit1 a := norm_num.bit0_add_one a - -lemma mul_bit0_helper0 [simp] {A : Type} [s : comm_ring A] (a b : A) - : bit0 a * bit0 b = bit0 (bit0 a * b) := norm_num.mul_bit0_helper (bit0 a) b (bit0 a * b) rfl - -lemma mul_bit0_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A) - : bit1 a * bit0 b = bit0 (bit1 a * b) := norm_num.mul_bit0_helper (bit1 a) b (bit1 a * b) rfl - -lemma mul_bit1_helper0 [simp] {A : Type} [s : comm_ring A] (a b : A) - : bit0 a * bit1 b = bit0 (bit0 a * b) + bit0 a := norm_num.mul_bit1_helper (bit0 a) b (bit0 a * b) (bit0 (bit0 a * b) + bit0 a) rfl rfl - -lemma mul_bit1_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A) - : bit1 a * bit1 b = bit0 (bit1 a * b) + bit1 a := norm_num.mul_bit1_helper (bit1 a) b (bit1 a * b) (bit0 (bit1 a * b) + bit1 a) rfl rfl - -end numeral_helper - -export simplifier.ac - -attribute norm_num.bit0_add_bit0 [simp] -attribute numeral_helper.bit1_add_one [simp] -attribute norm_num.bit1_add_bit0 [simp] -attribute numeral_helper.bit1_add_bit1 [simp] -attribute norm_num.bit0_add_bit1 [simp] -attribute numeral_helper.one_add_bit1 [simp] - -attribute norm_num.one_add_one [simp] -attribute numeral_helper.one_add_bit0 [simp] -attribute numeral_helper.bit0_add_one [simp] - -attribute numeral_helper.mul_bit0_helper0 [simp] -attribute numeral_helper.mul_bit0_helper1 [simp] -attribute numeral_helper.mul_bit1_helper0 [simp] -attribute numeral_helper.mul_bit1_helper1 [simp] - -end numeral - -end simplifier diff --git a/library/init/simplifier.lean b/library/init/simplifier.lean index 10c7e65ca..de6804522 100644 --- a/library/init/simplifier.lean +++ b/library/init/simplifier.lean @@ -8,6 +8,13 @@ import init.logic namespace simplifier +namespace empty +end empty + +namespace prove +attribute eq_self_iff_true [simp] +end prove + namespace unit_simp open eq.ops diff --git a/src/library/blast/simplifier/simp_rule_set.cpp b/src/library/blast/simplifier/simp_rule_set.cpp index 9410afef3..e2f4e5d33 100644 --- a/src/library/blast/simplifier/simp_rule_set.cpp +++ b/src/library/blast/simplifier/simp_rule_set.cpp @@ -556,6 +556,20 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, return set; } +simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list const & nss) { + simp_rule_sets set; + for (name const & ns : nss) { + list const * entries = rrs_ext::get_entries(env, ns); + if (entries) { + for (auto const & e : *entries) { + tmp_type_context tctx(env, ios); + set = add_core(tctx, set, e.m_name, e.m_priority); + } + } + } + return set; +} + io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s) { options const & opts = out.get_options(); out.get_stream() << mk_pair(s.pp(out.get_formatter()), opts); diff --git a/src/library/blast/simplifier/simp_rule_set.h b/src/library/blast/simplifier/simp_rule_set.h index a372f78dc..0c812d1cf 100644 --- a/src/library/blast/simplifier/simp_rule_set.h +++ b/src/library/blast/simplifier/simp_rule_set.h @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "library/tmp_type_context.h" #include "library/head_map.h" #include "library/io_state_stream.h" -#include #ifndef LEAN_SIMP_DEFAULT_PRIORITY #define LEAN_SIMP_DEFAULT_PRIORITY 1000 @@ -146,6 +145,8 @@ bool is_congr_rule(environment const & env, name const & n); simp_rule_sets get_simp_rule_sets(environment const & env); /** \brief Get simplification rule sets in the given namespace. */ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns); +/** \brief Get simplification rule sets in the given namespaces. */ +simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list const & nss); io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s); diff --git a/src/library/blast/simplifier/simplifier.cpp b/src/library/blast/simplifier/simplifier.cpp index 38517e97f..8fd7b4ecd 100644 --- a/src/library/blast/simplifier/simplifier.cpp +++ b/src/library/blast/simplifier/simplifier.cpp @@ -1,7 +1,7 @@ /* - Copyright (c) 2015 Daniel Selsam. All rights reserved. - Released under Apache 2.0 license as described in the file LICENSE. - Author: Daniel Selsam +Copyright (c) 2015 Daniel Selsam. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Daniel Selsam */ #include "kernel/abstract.h" #include "kernel/expr_maps.h" @@ -60,10 +60,11 @@ using simp::result; /* Names */ -static name * g_simplify_empty_namespace = nullptr; +static name * g_simplify_prove_namespace = nullptr; +static name * g_simplify_neg_namespace = nullptr; static name * g_simplify_unit_namespace = nullptr; static name * g_simplify_ac_namespace = nullptr; -static name * g_simplify_som_namespace = nullptr; +static name * g_simplify_distrib_namespace = nullptr; static name * g_simplify_numeral_namespace = nullptr; /* Options */ @@ -980,7 +981,9 @@ result simplifier::fuse(expr const & e) { /* Prove (1) == (3) using simplify with [ac] */ flet no_simplify_numerals(m_numerals, false); auto pf_1_3 = prove(get_app_builder().mk_eq(e, e_grp), - get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace)); + get_simp_rule_sets(env(), ios(), + {*g_simplify_prove_namespace, *g_simplify_unit_namespace, + *g_simplify_neg_namespace, *g_simplify_ac_namespace})); if (!pf_1_3) { diagnostic(env(), ios()) << e << "\n\n =?=\n\n" << e_grp << "\n"; throw blast_exception("Failed to prove (1) == (3) during fusion", e); @@ -988,7 +991,10 @@ result simplifier::fuse(expr const & e) { /* Prove (4) == (5) using simplify with [som] */ auto pf_4_5 = prove(get_app_builder().mk_eq(e_grp_ls, e_fused_ls), - get_simp_rule_sets(env(), ios(), *g_simplify_som_namespace)); + get_simp_rule_sets(env(), ios(), + {*g_simplify_prove_namespace, *g_simplify_unit_namespace, + *g_simplify_neg_namespace, *g_simplify_ac_namespace, + *g_simplify_distrib_namespace})); if (!pf_4_5) { diagnostic(env(), ios()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n"; throw blast_exception("Failed to prove (4) == (5) during fusion", e); @@ -996,7 +1002,9 @@ result simplifier::fuse(expr const & e) { /* Prove (5) == (6) using simplify with [numeral] */ flet simplify_numerals(m_numerals, true); - result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(), *g_simplify_ac_namespace)); + result r_simp_ls = simplify(e_fused_ls, get_simp_rule_sets(env(), ios(), + {*g_simplify_unit_namespace, *g_simplify_neg_namespace, + *g_simplify_ac_namespace})); /* Prove (4) == (6) by transitivity of proofs (2) and (3) */ expr pf_4_6; @@ -1049,10 +1057,11 @@ 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_prove_namespace = new name{"simplifier", "prove"}; + g_simplify_neg_namespace = new name{"simplifier", "neg"}; g_simplify_unit_namespace = new name{"simplifier", "unit"}; g_simplify_ac_namespace = new name{"simplifier", "ac"}; - g_simplify_som_namespace = new name{"simplifier", "som"}; + g_simplify_distrib_namespace = new name{"simplifier", "distrib"}; g_simplify_numeral_namespace = new name{"simplifier", "numeral"}; g_simplify_max_steps = new name{"simplify", "max_steps"}; @@ -1097,10 +1106,11 @@ void finalize_simplifier() { delete g_simplify_max_steps; delete g_simplify_numeral_namespace; - delete g_simplify_som_namespace; + delete g_simplify_distrib_namespace; delete g_simplify_ac_namespace; delete g_simplify_unit_namespace; - delete g_simplify_empty_namespace; + delete g_simplify_neg_namespace; + delete g_simplify_prove_namespace; } /* Entry points */ diff --git a/tests/lean/simplifier12.lean b/tests/lean/simplifier12.lean index b2ccd19e0..d402c6bcc 100644 --- a/tests/lean/simplifier12.lean +++ b/tests/lean/simplifier12.lean @@ -1,5 +1,5 @@ -import algebra.simplifier -open algebra simplifier.som +import algebra.ring +open algebra set_option simplify.max_steps 1000 universe l @@ -7,4 +7,6 @@ constants (T : Type.{l}) (s : algebra.comm_ring T) constants (x1 x2 x3 x4 : T) (f g : T → T) attribute s [instance] -#simplify eq simplifier.som 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1) +open simplifier.unit simplifier.ac simplifier.neg simplifier.distrib + +#simplify eq env 0 x2 + (1 * g x1 + 0 + (f x3 * 3 * 1 * (x2 + 0 + g x1 * 7) * x2 * 1)) + 5 * (x4 + f x1) diff --git a/tests/lean/simplifier14.lean b/tests/lean/simplifier14.lean index 0841c666a..06488b661 100644 --- a/tests/lean/simplifier14.lean +++ b/tests/lean/simplifier14.lean @@ -1,5 +1,5 @@ -- Basic fusion -import algebra.simplifier +import algebra.ring algebra.numeral open algebra universe l @@ -9,19 +9,21 @@ attribute s [instance] set_option simplify.max_steps 50000 set_option simplify.fuse true -#simplify eq simplifier.som 0 x1 -#simplify eq simplifier.som 0 x1 + x1 -#simplify eq simplifier.som 0 (x1 + x1) + x1 -#simplify eq simplifier.som 0 (x1 + x1) + (x1 + x1) -#simplify eq simplifier.som 0 x1 + x1 + x1 + x1 -#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1 -#simplify eq simplifier.som 0 x1 - x1 -#simplify eq simplifier.som 0 (x1 - x1) + x1 -#simplify eq simplifier.som 0 (x1 + x1) - (x1 + x1) -#simplify eq simplifier.som 0 x1 + x1 - x1 - x1 -#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1 -#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 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2 -#simplify eq simplifier.som 0 x2 + x1 - x2 - (- x1) +open simplifier.unit simplifier.ac simplifier.neg + +#simplify eq env 0 x1 +#simplify eq env 0 x1 + x1 +#simplify eq env 0 (x1 + x1) + x1 +#simplify eq env 0 (x1 + x1) + (x1 + x1) +#simplify eq env 0 x1 + x1 + x1 + x1 +#simplify eq env 0 x1 + x1 + (x1 + x1) + x1 +#simplify eq env 0 x1 - x1 +#simplify eq env 0 (x1 - x1) + x1 +#simplify eq env 0 (x1 + x1) - (x1 + x1) +#simplify eq env 0 x1 + x1 - x1 - x1 +#simplify eq env 0 x1 + x1 + (x1 + x1) + x1 +#simplify eq env 0 (x1 - x2) + x2 - x1 +#simplify eq env 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1 +#simplify eq env 0 x2 + x1 - x2 - - x1 +#simplify eq env 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2 +#simplify eq env 0 x2 + x1 - x2 - (- x1) diff --git a/tests/lean/simplifier15.lean b/tests/lean/simplifier15.lean index 6f619b176..5f6442cc0 100644 --- a/tests/lean/simplifier15.lean +++ b/tests/lean/simplifier15.lean @@ -1,5 +1,5 @@ -- normalizing reducible non-subsingleton instances -import algebra.simplifier +import algebra.ring open algebra universe l diff --git a/tests/lean/simplifier18.lean b/tests/lean/simplifier18.lean index 41ba4bc21..d5a9ef3ee 100644 --- a/tests/lean/simplifier18.lean +++ b/tests/lean/simplifier18.lean @@ -1,5 +1,5 @@ -- Basic fusion -import algebra.simplifier +import algebra.ring algebra.numeral open algebra universe l @@ -9,19 +9,21 @@ 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 2 * 2 + x1 -#simplify eq simplifier.som 0 x2 * (2 * 2) + x1 -#simplify eq simplifier.som 0 2 * 2 * x2 + x1 -#simplify eq simplifier.som 0 2 * x2 * 2 + x1 -#simplify eq simplifier.som 0 200 * x2 * 200 + x1 -#simplify eq simplifier.som 0 x1 * 200 * x2 * 200 + x1 -#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * 200 + x1 -#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * x4 * 200 + x1 +open simplifier.unit simplifier.ac simplifier.neg + +#simplify eq env 0 x1 * x2 +#simplify eq env 0 x1 * 2 * x2 +#simplify eq env 0 x1 * 2 * x2 * 3 +#simplify eq env 0 2 * x2 + x1 * 8 * x2 * 4 +#simplify eq env 0 2 * x2 - x1 * 8 * x2 * 4 +#simplify eq env 0 2 * x2 - 8 * x2 * 4 * x1 +#simplify eq env 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2 +#simplify eq env 0 (x1 * x3 + x1 * 2 + x2 * 3 * x3 + x1 * x2) - 2* x2 * x1 + 1 * x2 * x1 - 3 * x1 * x3 +#simplify eq env 0 2 * 2 + x1 +#simplify eq env 0 x2 * (2 * 2) + x1 +#simplify eq env 0 2 * 2 * x2 + x1 +#simplify eq env 0 2 * x2 * 2 + x1 +#simplify eq env 0 200 * x2 * 200 + x1 +#simplify eq env 0 x1 * 200 * x2 * 200 + x1 +#simplify eq env 0 x1 * 200 * x2 * x3 * 200 + x1 +#simplify eq env 0 x1 * 200 * x2 * x3 * x4 * 200 + x1 diff --git a/tests/lean/simplifier19.lean b/tests/lean/simplifier19.lean index ced40ce92..0b6190023 100644 --- a/tests/lean/simplifier19.lean +++ b/tests/lean/simplifier19.lean @@ -1,5 +1,5 @@ -- Nested fusion -import algebra.simplifier +import algebra.ring algebra.numeral open algebra universe l @@ -9,4 +9,6 @@ attribute s [instance] set_option simplify.max_steps 50000 set_option simplify.fuse true -#simplify eq simplifier.som 0 f (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) + g (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) +open simplifier.unit simplifier.ac simplifier.neg + +#simplify eq env 0 f (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) + g (x1 * x2 * 3 * 4 - 4 * 3 * x1 * x2) diff --git a/tests/lean/simplifier_light.lean b/tests/lean/simplifier_light.lean index 2c178da39..3227ea847 100644 --- a/tests/lean/simplifier_light.lean +++ b/tests/lean/simplifier_light.lean @@ -1,8 +1,8 @@ -- Test [light] annotation -- Remark: it will take some additional work to get ⁻¹ to rewrite well -- when there is a proof obligation. -import algebra.simplifier algebra.field data.set data.finset -open algebra simplifier.ac +import algebra.ring algebra.field data.set data.finset +open algebra attribute neg [light 2] attribute inv [light 2] @@ -12,6 +12,8 @@ attribute add_neg_cancel_left [simp] attribute mul.right_inv [simp] attribute mul_inv_cancel_left [simp] +open simplifier.unit simplifier.ac + namespace ag universe l constants (A : Type.{l}) (s1 : add_comm_group A) (s2 : has_one A) diff --git a/tests/lean/simplifier_norm_num.lean b/tests/lean/simplifier_norm_num.lean index 2d3eb385f..d72d93370 100644 --- a/tests/lean/simplifier_norm_num.lean +++ b/tests/lean/simplifier_norm_num.lean @@ -1,9 +1,10 @@ -import algebra.simplifier +import algebra.ring algebra.numeral open algebra -open simplifier.numeral - set_option simplify.max_steps 5000000 +-- TODO(dhs): we need to create the simplifier.numeral namespace incrementally. +-- Once it exists, we can uncomment the following line to use it simplify. +set_option simplify.numerals true universe l constants (A : Type.{l}) (A_comm_ring : comm_ring A) attribute A_comm_ring [instance] @@ -54,5 +55,4 @@ attribute A_comm_ring [instance] #simplify eq env 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733) --- The following test is too slow --- #simplify eq 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536 +#simplify eq env 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536 diff --git a/tests/lean/simplifier_norm_num.lean.expected.out b/tests/lean/simplifier_norm_num.lean.expected.out index 3b82bbf47..d66457d0b 100644 --- a/tests/lean/simplifier_norm_num.lean.expected.out +++ b/tests/lean/simplifier_norm_num.lean.expected.out @@ -40,3 +40,4 @@ 90 15241383936 130049014430002489296 +6599110652246543565516387775250463433475607911914556819497064648