michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(library/algebra): construct simplifier sets incrementally

Browse source
This commit is contained in:
Daniel Selsam 2015-12-04 17:57:03 -08:00 committed by Leonardo de Moura
parent 2682fe9525
commit a04c28d4c9
15 changed files with 152 additions and 183 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
library/algebra/group.lean
View file

@ -580,3 +580,30 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A :=
mul_left_inv := add.left_inv⦄ mul_left_inv := add.left_inv⦄
end algebra 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

22
library/algebra/ring.lean
View file

@ -195,6 +195,9 @@ section
rewrite [-left_distrib, add.right_inv, mul_zero] rewrite [-left_distrib, add.right_inv, mul_zero]
end 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 := theorem neg_mul_neg : -a * -b = a * b :=
calc calc
-a * -b = -(a * -b) : by rewrite -neg_mul_eq_neg_mul -a * -b = -(a * -b) : by rewrite -neg_mul_eq_neg_mul
@ -402,3 +405,22 @@ section
end end
end algebra 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

123
library/algebra/simplifier.lean
View file

@ -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

7
library/init/simplifier.lean
View file

@ -8,6 +8,13 @@ import init.logic
namespace simplifier namespace simplifier
namespace empty
end empty
namespace prove
attribute eq_self_iff_true [simp]
end prove
namespace unit_simp namespace unit_simp
open eq.ops open eq.ops

14
src/library/blast/simplifier/simp_rule_set.cpp
View file

@ -556,6 +556,20 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
return set; return set;
} }
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, std::initializer_list<name> const & nss) {
simp_rule_sets set;
for (name const & ns : nss) {
list<rrs_entry> 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) { io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s) {
options const & opts = out.get_options(); options const & opts = out.get_options();
out.get_stream() << mk_pair(s.pp(out.get_formatter()), opts); out.get_stream() << mk_pair(s.pp(out.get_formatter()), opts);

3
src/library/blast/simplifier/simp_rule_set.h
View file

@ -8,7 +8,6 @@ Author: Leonardo de Moura
#include "library/tmp_type_context.h" #include "library/tmp_type_context.h"
#include "library/head_map.h" #include "library/head_map.h"
#include "library/io_state_stream.h" #include "library/io_state_stream.h"
#include <vector>
#ifndef LEAN_SIMP_DEFAULT_PRIORITY #ifndef LEAN_SIMP_DEFAULT_PRIORITY
#define LEAN_SIMP_DEFAULT_PRIORITY 1000 #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); simp_rule_sets get_simp_rule_sets(environment const & env);
/** \brief Get simplification rule sets in the given namespace. */ /** \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); 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<name> const & nss);
io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s); io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s);

34
src/library/blast/simplifier/simplifier.cpp
View file

@ -1,7 +1,7 @@
/* /*
Copyright (c) 2015 Daniel Selsam. All rights reserved. Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE. Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam Author: Daniel Selsam
*/ */
#include "kernel/abstract.h" #include "kernel/abstract.h"
#include "kernel/expr_maps.h" #include "kernel/expr_maps.h"
@ -60,10 +60,11 @@ using simp::result;
/* Names */ /* 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_unit_namespace = nullptr;
static name * g_simplify_ac_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; static name * g_simplify_numeral_namespace = nullptr;
/* Options */ /* Options */
@ -980,7 +981,9 @@ result simplifier::fuse(expr const & e) {
/* Prove (1) == (3) using simplify with [ac] */ /* Prove (1) == (3) using simplify with [ac] */
flet<bool> no_simplify_numerals(m_numerals, false); flet<bool> no_simplify_numerals(m_numerals, false);
auto pf_1_3 = prove(get_app_builder().mk_eq(e, e_grp), 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) { if (!pf_1_3) {
diagnostic(env(), ios()) << e << "\n\n =?=\n\n" << e_grp << "\n"; diagnostic(env(), ios()) << e << "\n\n =?=\n\n" << e_grp << "\n";
throw blast_exception("Failed to prove (1) == (3) during fusion", e); 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] */ /* Prove (4) == (5) using simplify with [som] */
auto pf_4_5 = prove(get_app_builder().mk_eq(e_grp_ls, e_fused_ls), 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) { if (!pf_4_5) {
diagnostic(env(), ios()) << e_grp_ls << "\n\n =?=\n\n" << e_fused_ls << "\n"; 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); 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] */ /* Prove (5) == (6) using simplify with [numeral] */
flet<bool> simplify_numerals(m_numerals, true); flet<bool> 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) */ /* Prove (4) == (6) by transitivity of proofs (2) and (3) */
expr pf_4_6; 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 */ /* Setup and teardown */
void initialize_simplifier() { 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_unit_namespace = new name{"simplifier", "unit"};
g_simplify_ac_namespace = new name{"simplifier", "ac"}; 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_numeral_namespace = new name{"simplifier", "numeral"};
g_simplify_max_steps = new name{"simplify", "max_steps"}; g_simplify_max_steps = new name{"simplify", "max_steps"};
@ -1097,10 +1106,11 @@ void finalize_simplifier() {
delete g_simplify_max_steps; delete g_simplify_max_steps;
delete g_simplify_numeral_namespace; delete g_simplify_numeral_namespace;
delete g_simplify_som_namespace; delete g_simplify_distrib_namespace;
delete g_simplify_ac_namespace; delete g_simplify_ac_namespace;
delete g_simplify_unit_namespace; delete g_simplify_unit_namespace;
delete g_simplify_empty_namespace; delete g_simplify_neg_namespace;
delete g_simplify_prove_namespace;
} }
/* Entry points */ /* Entry points */

8
tests/lean/simplifier12.lean
View file

@ -1,5 +1,5 @@
import algebra.simplifier import algebra.ring
open algebra simplifier.som open algebra
set_option simplify.max_steps 1000 set_option simplify.max_steps 1000
universe l 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) constants (x1 x2 x3 x4 : T) (f g : T → T)
attribute s [instance] 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)

36
tests/lean/simplifier14.lean
View file

@ -1,5 +1,5 @@
-- Basic fusion -- Basic fusion
import algebra.simplifier import algebra.ring algebra.numeral
open algebra open algebra
universe l universe l
@ -9,19 +9,21 @@ attribute s [instance]
set_option simplify.max_steps 50000 set_option simplify.max_steps 50000
set_option simplify.fuse true set_option simplify.fuse true
#simplify eq simplifier.som 0 x1 open simplifier.unit simplifier.ac simplifier.neg
#simplify eq simplifier.som 0 x1 + x1
#simplify eq simplifier.som 0 (x1 + x1) + x1 #simplify eq env 0 x1
#simplify eq simplifier.som 0 (x1 + x1) + (x1 + x1) #simplify eq env 0 x1 + x1
#simplify eq simplifier.som 0 x1 + x1 + x1 + x1 #simplify eq env 0 (x1 + x1) + x1
#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1 #simplify eq env 0 (x1 + x1) + (x1 + x1)
#simplify eq simplifier.som 0 x1 - x1 #simplify eq env 0 x1 + x1 + x1 + x1
#simplify eq simplifier.som 0 (x1 - x1) + x1 #simplify eq env 0 x1 + x1 + (x1 + x1) + x1
#simplify eq simplifier.som 0 (x1 + x1) - (x1 + x1) #simplify eq env 0 x1 - x1
#simplify eq simplifier.som 0 x1 + x1 - x1 - x1 #simplify eq env 0 (x1 - x1) + x1
#simplify eq simplifier.som 0 x1 + x1 + (x1 + x1) + x1 #simplify eq env 0 (x1 + x1) - (x1 + x1)
#simplify eq simplifier.som 0 (x1 - x2) + x2 - x1 #simplify eq env 0 x1 + x1 - x1 - x1
#simplify eq simplifier.som 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1 #simplify eq env 0 x1 + x1 + (x1 + x1) + x1
#simplify eq simplifier.som 0 x2 + x1 - x2 - - x1 #simplify eq env 0 (x1 - x2) + x2 - x1
#simplify eq simplifier.som 0 (x1 - 2 * x3 * x2) + x2 * x3 * 3 - 1 * 0 * x1 * x2 #simplify eq env 0 (x1 + x1 + x2 + x1) - 2* x2 + 1 * x2 - 3 * x1
#simplify eq simplifier.som 0 x2 + x1 - x2 - (- 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)

2
tests/lean/simplifier15.lean
View file

@ -1,5 +1,5 @@
-- normalizing reducible non-subsingleton instances -- normalizing reducible non-subsingleton instances
import algebra.simplifier import algebra.ring
open algebra open algebra
universe l universe l

36
tests/lean/simplifier18.lean
View file

@ -1,5 +1,5 @@
-- Basic fusion -- Basic fusion
import algebra.simplifier import algebra.ring algebra.numeral
open algebra open algebra
universe l universe l
@ -9,19 +9,21 @@ attribute s [instance]
set_option simplify.max_steps 50000 set_option simplify.max_steps 50000
set_option simplify.fuse true set_option simplify.fuse true
#simplify eq simplifier.som 0 x1 * x2 open simplifier.unit simplifier.ac simplifier.neg
#simplify eq simplifier.som 0 x1 * 2 * x2
#simplify eq simplifier.som 0 x1 * 2 * x2 * 3 #simplify eq env 0 x1 * x2
#simplify eq simplifier.som 0 2 * x2 + x1 * 8 * x2 * 4 #simplify eq env 0 x1 * 2 * x2
#simplify eq simplifier.som 0 2 * x2 - x1 * 8 * x2 * 4 #simplify eq env 0 x1 * 2 * x2 * 3
#simplify eq simplifier.som 0 2 * x2 - 8 * x2 * 4 * x1 #simplify eq env 0 2 * x2 + x1 * 8 * x2 * 4
#simplify eq simplifier.som 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2 #simplify eq env 0 2 * x2 - x1 * 8 * x2 * 4
#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 env 0 2 * x2 - 8 * x2 * 4 * x1
#simplify eq simplifier.som 0 2 * 2 + x1 #simplify eq env 0 x2 * x1 + 3 * x1 + (2 * x2 - 8 * x2 * 4 * x1) + x1 * x2
#simplify eq simplifier.som 0 x2 * (2 * 2) + x1 #simplify eq env 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 * x2 + x1 #simplify eq env 0 2 * 2 + x1
#simplify eq simplifier.som 0 2 * x2 * 2 + x1 #simplify eq env 0 x2 * (2 * 2) + x1
#simplify eq simplifier.som 0 200 * x2 * 200 + x1 #simplify eq env 0 2 * 2 * x2 + x1
#simplify eq simplifier.som 0 x1 * 200 * x2 * 200 + x1 #simplify eq env 0 2 * x2 * 2 + x1
#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * 200 + x1 #simplify eq env 0 200 * x2 * 200 + x1
#simplify eq simplifier.som 0 x1 * 200 * x2 * x3 * x4 * 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

6
tests/lean/simplifier19.lean
View file

@ -1,5 +1,5 @@
-- Nested fusion -- Nested fusion
import algebra.simplifier import algebra.ring algebra.numeral
open algebra open algebra
universe l universe l
@ -9,4 +9,6 @@ attribute s [instance]
set_option simplify.max_steps 50000 set_option simplify.max_steps 50000
set_option simplify.fuse true 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)

6
tests/lean/simplifier_light.lean
View file

@ -1,8 +1,8 @@
-- Test [light] annotation -- Test [light] annotation
-- Remark: it will take some additional work to get ⁻¹ to rewrite well -- Remark: it will take some additional work to get ⁻¹ to rewrite well
-- when there is a proof obligation. -- when there is a proof obligation.
import algebra.simplifier algebra.field data.set data.finset import algebra.ring algebra.field data.set data.finset
open algebra simplifier.ac open algebra
attribute neg [light 2] attribute neg [light 2]
attribute inv [light 2] attribute inv [light 2]
@ -12,6 +12,8 @@ attribute add_neg_cancel_left [simp]
attribute mul.right_inv [simp] attribute mul.right_inv [simp]
attribute mul_inv_cancel_left [simp] attribute mul_inv_cancel_left [simp]
open simplifier.unit simplifier.ac
namespace ag namespace ag
universe l universe l
constants (A : Type.{l}) (s1 : add_comm_group A) (s2 : has_one A) constants (A : Type.{l}) (s1 : add_comm_group A) (s2 : has_one A)

10
tests/lean/simplifier_norm_num.lean
View file

@ -1,9 +1,10 @@
import algebra.simplifier import algebra.ring algebra.numeral
open algebra open algebra
open simplifier.numeral
set_option simplify.max_steps 5000000 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 universe l
constants (A : Type.{l}) (A_comm_ring : comm_ring A) constants (A : Type.{l}) (A_comm_ring : comm_ring A)
attribute A_comm_ring [instance] 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) #simplify eq env 0 (0 + 45343453:A) * (53653343 + 1) * (53453 + 2) + (0 + 1 + 2 + 2200000000034733)
-- The following test is too slow #simplify eq env 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536
-- #simplify eq 0 (23000000000343434534345316:A) * (53653343563534534 + 5367536453653573573453) * 53453756475777536 + 2200000000034733531531531534536

1
tests/lean/simplifier_norm_num.lean.expected.out
View file

@ -40,3 +40,4 @@
90 90
15241383936 15241383936
130049014430002489296 130049014430002489296
6599110652246543565516387775250463433475607911914556819497064648