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

feat(library/blast/simplifier): draft of fusion

Browse source
This commit is contained in:
Daniel Selsam 2015-11-16 08:54:21 -08:00
parent c694d443d7
commit 5e8068b2b2
19 changed files with 719 additions and 152 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

116
library/algebra/simplifier.lean
View file

@ -7,23 +7,30 @@ import algebra.ring algebra.numeral
namespace simplifier
namespace sum_of_monomials
-- TODO(dhs): refactor this once we fix `export` command
-- 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
lemma
end neg_helper
attribute algebra.add.assoc [simp]
attribute algebra.add.comm [simp]
attribute algebra.add.left_comm [simp]
namespace ac
attribute algebra.mul.left_comm [simp]
attribute algebra.mul.comm [simp]
attribute algebra.mul.assoc [simp]
-- iff
lemma eq_iff_true [simp] {A : Type} (a : A) : a = a ↔ true := sorry
attribute algebra.left_distrib [simp]
attribute algebra.right_distrib [simp]
end sum_of_monomials
namespace units
-- neg
attribute neg_helper.neg_mul1 [simp]
attribute neg_helper.neg_mul2 [simp]
attribute neg_helper.sub_def [simp]
attribute algebra.neg_neg [simp]
-- unit
attribute algebra.zero_add [simp]
attribute algebra.add_zero [simp]
@ -33,7 +40,54 @@ attribute algebra.mul_zero [simp]
attribute algebra.one_mul [simp]
attribute algebra.mul_one [simp]
end units
-- 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
namespace som
-- iff
lemma eq_iff_true [simp] {A : Type} (a : A) : a = a ↔ true := sorry
-- neg
attribute neg_helper.neg_mul1 [simp]
attribute neg_helper.neg_mul2 [simp]
attribute neg_helper.sub_def [simp]
attribute algebra.neg_neg [simp]
-- 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]
-- 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]
-- distrib
attribute algebra.left_distrib [simp]
attribute algebra.right_distrib [simp]
end som
namespace numeral
-- TODO(dhs): remove `add1` from the original lemmas and delete this
namespace numeral_helper
@ -69,8 +123,32 @@ lemma mul_bit1_helper1 [simp] {A : Type} [s : comm_ring A] (a b : A)
end numeral_helper
namespace numeral
-- neg
attribute neg_helper.neg_mul1 [simp]
attribute neg_helper.neg_mul2 [simp]
attribute neg_helper.sub_def [simp]
attribute algebra.neg_neg [simp]
-- 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]
-- 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]
-- numerals
attribute norm_num.bit0_add_bit0 [simp]
attribute numeral_helper.bit1_add_one [simp]
attribute norm_num.bit1_add_bit0 [simp]
@ -78,9 +156,6 @@ attribute numeral_helper.bit1_add_bit1 [simp]
attribute norm_num.bit0_add_bit1 [simp]
attribute numeral_helper.one_add_bit1 [simp]
attribute algebra.zero_add [simp]
attribute algebra.add_zero [simp]
attribute norm_num.one_add_one [simp]
attribute numeral_helper.one_add_bit0 [simp]
attribute numeral_helper.bit0_add_one [simp]
@ -90,11 +165,6 @@ attribute numeral_helper.mul_bit0_helper1 [simp]
attribute numeral_helper.mul_bit1_helper0 [simp]
attribute numeral_helper.mul_bit1_helper1 [simp]
attribute algebra.zero_mul [simp]
attribute algebra.mul_zero [simp]
attribute algebra.one_mul [simp]
attribute algebra.mul_one [simp]
end numeral
end simplifier

12
src/frontends/lean/builtin_cmds.cpp
View file

@ -1329,13 +1329,19 @@ static environment congr_cmd(parser & p) {
static environment simplify_cmd(parser & p) {
name rel = p.check_constant_next("invalid #simplify command, constant expected");
name ns = p.check_id_next("invalid #simplify command, id expected");
unsigned o = p.parse_small_nat();
expr e; level_param_names ls;
std::tie(e, ls) = parse_local_expr(p);
blast::scope_debug scope(p.env(), p.ios());
blast::simp::result r = blast::simplify(rel, e, get_simp_rule_sets(p.env()));
simp_rule_sets srss;
if (ns == name("null")) { }
if (ns == name("env")) { srss = get_simp_rule_sets(p.env()); }
else { srss = get_simp_rule_sets(p.env(), p.ios(), ns); }
blast::simp::result r = blast::simplify(rel, e, srss);
flycheck_information info(p.regular_stream());
if (info.enabled()) {
@ -1343,8 +1349,8 @@ static environment simplify_cmd(parser & p) {
p.regular_stream() << "simplify result:\n";
}
if (r.is_none()) {
p.regular_stream() << "<refl>" << endl;
if (!r.has_proof()) {
p.regular_stream() << "(refl): " << r.get_new() << endl;
} else {
auto tc = mk_type_checker(p.env(), p.mk_ngen());

66
src/library/app_builder.cpp
View file

@ -459,6 +459,48 @@ struct app_builder::imp {
return mk_app(get_congr_name(), {H1, H2});
}
expr mk_partial_add(expr const & A) {
level lvl = get_level(A);
auto A_has_add = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_add_name(), {lvl}), A));
if (!A_has_add) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_add_name(), {lvl}), A, *A_has_add);
}
expr mk_partial_mul(expr const & A) {
level lvl = get_level(A);
auto A_has_mul = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_mul_name(), {lvl}), A));
if (!A_has_mul) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_mul_name(), {lvl}), A, *A_has_mul);
}
expr mk_zero(expr const & A) {
level lvl = get_level(A);
auto A_has_zero = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_zero_name(), {lvl}), A));
if (!A_has_zero) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_zero_name(), {lvl}), A, *A_has_zero);
}
expr mk_one(expr const & A) {
level lvl = get_level(A);
auto A_has_one = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_has_one_name(), {lvl}), A));
if (!A_has_one) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_one_name(), {lvl}), A, *A_has_one);
}
expr mk_partial_left_distrib(expr const & A) {
level lvl = get_level(A);
auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_algebra_distrib_name(), {lvl}), A));
if (!A_distrib) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_algebra_left_distrib_name(), {lvl}), A, *A_distrib);
}
expr mk_partial_right_distrib(expr const & A) {
level lvl = get_level(A);
auto A_distrib = m_ctx->mk_class_instance(::lean::mk_app(mk_constant(get_algebra_distrib_name(), {lvl}), A));
if (!A_distrib) throw app_builder_exception();
return ::lean::mk_app(mk_constant(get_algebra_right_distrib_name(), {lvl}), A, *A_distrib);
}
expr mk_false_rec(expr const & c, expr const & H) {
level c_lvl = get_level(c);
if (is_standard(m_ctx->env())) {
@ -560,6 +602,30 @@ expr app_builder::mk_congr(expr const & H1, expr const & H2) {
return m_ptr->mk_congr(H1, H2);
}
expr app_builder::mk_partial_add(expr const & A) {
return m_ptr->mk_partial_add(A);
}
expr app_builder::mk_partial_mul(expr const & A) {
return m_ptr->mk_partial_mul(A);
}
expr app_builder::mk_zero(expr const & A) {
return m_ptr->mk_zero(A);
}
expr app_builder::mk_one(expr const & A) {
return m_ptr->mk_one(A);
}
expr app_builder::mk_partial_left_distrib(expr const & A) {
return m_ptr->mk_partial_left_distrib(A);
}
expr app_builder::mk_partial_right_distrib(expr const & A) {
return m_ptr->mk_partial_right_distrib(A);
}
expr app_builder::mk_sorry(expr const & type) {
return mk_app(get_sorry_name(), type);
}

7
src/library/app_builder.h
View file

@ -116,6 +116,13 @@ public:
expr mk_congr_fun(expr const & H, expr const & a);
expr mk_congr(expr const & H1, expr const & H2);
expr mk_partial_add(expr const & A);
expr mk_partial_mul(expr const & A);
expr mk_zero(expr const & A);
expr mk_one(expr const & A);
expr mk_partial_left_distrib(expr const & A);
expr mk_partial_right_distrib(expr const & A);
/** \brief Create (@sorry type) */
expr mk_sorry(expr const & type);

39
src/library/blast/blast.cpp
View file

@ -16,6 +16,7 @@ Author: Leonardo de Moura
#include "library/type_context.h"
#include "library/relation_manager.h"
#include "library/congr_lemma_manager.h"
#include "library/abstract_expr_manager.h"
#include "library/projection.h"
#include "library/tactic/goal.h"
#include "library/blast/expr.h"
@ -56,6 +57,7 @@ class blastenv {
app_builder m_app_builder;
fun_info_manager m_fun_info_manager;
congr_lemma_manager m_congr_lemma_manager;
abstract_expr_manager m_abstract_expr_manager;
class tctx : public type_context {
blastenv & m_benv;
@ -410,6 +412,7 @@ public:
m_app_builder(*m_tmp_ctx),
m_fun_info_manager(*m_tmp_ctx),
m_congr_lemma_manager(m_app_builder, m_fun_info_manager),
m_abstract_expr_manager(m_fun_info_manager),
m_tctx(*this),
m_normalizer(m_tctx) {
init_uref_mref_href_idxs();
@ -482,6 +485,14 @@ public:
return m_congr_lemma_manager.mk_congr_simp(fn);
}
optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args) {
return m_congr_lemma_manager.mk_congr(fn, num_args);
}
optional<congr_lemma> mk_congr_lemma(expr const & fn) {
return m_congr_lemma_manager.mk_congr(fn);
}
fun_info get_fun_info(expr const & fn) {
return m_fun_info_manager.get(fn);
}
@ -490,6 +501,14 @@ public:
return m_fun_info_manager.get(fn, nargs);
}
unsigned abstract_hash(expr const & e) {
return m_abstract_expr_manager.hash(e);
}
bool abstract_is_equal(expr const & e1, expr const & e2) {
return m_abstract_expr_manager.is_equal(e1, e2);
}
/** \brief Convert an external expression into a blast expression
It converts meta-variables to blast meta-variables, and ensures the expressions
are maximally shared.
@ -629,6 +648,16 @@ optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn) {
return g_blastenv->mk_congr_lemma_for_simp(fn);
}
optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args) {
lean_assert(g_blastenv);
return g_blastenv->mk_congr_lemma(fn, num_args);
}
optional<congr_lemma> mk_congr_lemma(expr const & fn) {
lean_assert(g_blastenv);
return g_blastenv->mk_congr_lemma(fn);
}
fun_info get_fun_info(expr const & fn) {
lean_assert(g_blastenv);
return g_blastenv->get_fun_info(fn);
@ -639,6 +668,16 @@ fun_info get_fun_info(expr const & fn, unsigned nargs) {
return g_blastenv->get_fun_info(fn, nargs);
}
unsigned abstract_hash(expr const & e) {
lean_assert(g_blastenv);
return g_blastenv->abstract_hash(e);
}
bool abstract_is_equal(expr const & e1, expr const & e2) {
lean_assert(g_blastenv);
return g_blastenv->abstract_is_equal(e1, e2);
}
void display_curr_state() {
curr_state().display(env(), ios());
display("\n");

18
src/library/blast/blast.h
View file

@ -79,12 +79,30 @@ optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn, unsigned num_args
/** \brief Similar to previous procedure, but num_args == arith of fn */
optional<congr_lemma> mk_congr_lemma_for_simp(expr const & fn);
/** \brief Create a congruence lemma for the given function.
\pre num_args <= arity of fn
\remark The procedure may fail when app_builder used by it fails.
Example: it fail to infer the type of fn.
\remark The generated lemma is useful for proving that two terms
that are definitionally equal upto subsingletons are propositionally
equal.
\remark The type \c congr_lemma is defined at library/congr_lemma_manager.h */
optional<congr_lemma> mk_congr_lemma(expr const & fn, unsigned num_args);
/** \brief Similar to previous procedure, but num_args == arith of fn */
optional<congr_lemma> mk_congr_lemma(expr const & fn);
/** \brief Retrieve information for the given function. */
fun_info get_fun_info(expr const & fn);
/** \brief Retrieve information for the given function.
\pre nargs <= arity fn. */
fun_info get_fun_info(expr const & fn, unsigned nargs);
/** \brief Hash and equality test for abstract expressions */
unsigned abstract_hash(expr const & e);
bool abstract_is_equal(expr const & e1, expr const & e2);
/** \brief Display the current state of the blast tactic in the diagnostic channel. */
void display_curr_state();
/** \brief Display the given expression in the diagnostic channel. */

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

@ -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"
@ -17,6 +17,7 @@ Author: Daniel Selsam
#include "library/simplifier/simp_rule_set.h"
#include "library/simplifier/ceqv.h"
#include "library/app_builder.h"
#include "library/num.h"
#include "util/flet.h"
#include "util/pair.h"
#include "util/sexpr/option_declarations.h"
@ -53,6 +54,13 @@ namespace blast {
using simp::result;
/* Names */
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_numeral_namespace = nullptr;
/* Options */
static name * g_simplify_max_steps = nullptr;
@ -98,11 +106,6 @@ bool get_simplify_fuse() {
/* Miscellaneous helpers */
static bool is_const_app(expr const & e, name const & n, unsigned nargs) {
expr const & f = get_app_fn(e);
return is_constant(f) && const_name(f) == n && get_app_num_args(e) == nargs;
}
static bool is_add_app(expr const & e) {
return is_const_app(e, get_add_name(), 4);
}
@ -140,15 +143,13 @@ class simplifier {
bool m_fuse{get_simplify_fuse()};
/* Cache */
static std::hash<simp_rule_set*> m_srss_hash;
struct key {
name m_rel;
expr m_e;
unsigned m_hash;
key(name const & rel, expr const & e):
m_rel(rel), m_e(e), m_hash(hash(rel.hash(), e.hash())) { }
m_rel(rel), m_e(e), m_hash(hash(rel.hash(), abstract_hash(e))) { }
};
struct key_hash_fn {
@ -157,7 +158,7 @@ class simplifier {
struct key_eq_fn {
bool operator()(key const & k1, key const & k2) const {
return k1.m_rel == k2.m_rel && k1.m_e == k2.m_e;
return k1.m_rel == k2.m_rel && abstract_is_equal(k1.m_e, k2.m_e);
}
};
@ -186,17 +187,19 @@ class simplifier {
return srss;
}
expr unfold_reducible_instances(expr const & e);
bool instantiate_emetas(blast_tmp_type_context & tmp_tctx, unsigned num_emeta,
list<expr> const & emetas, list<bool> const & instances);
/* Results */
result lift_from_eq(expr const & x, result const & r);
result lift_from_eq(expr const & e_old, result const & r_eq);
result join(result const & r1, result const & r2);
result funext(result const & r, expr const & l);
result finalize(result const & r);
/* Simplification */
result simplify(expr const & e, simp_rule_sets const & srss);
result simplify(expr const & e, bool is_root);
result simplify_lambda(expr const & e);
result simplify_pi(expr const & e);
@ -205,6 +208,7 @@ class simplifier {
/* Proving */
optional<expr> prove(expr const & thm);
optional<expr> prove(expr const & thm, simp_rule_sets const & srss);
/* Rewriting */
result rewrite(expr const & e);
@ -212,6 +216,7 @@ class simplifier {
result rewrite(expr const & e, simp_rule const & sr);
/* Congruence */
result congr_fun_arg(result const & r_f, result const & r_arg);
result congr(result const & r_f, result const & r_arg);
result congr_fun(result const & r_f, expr const & arg);
result congr_arg(expr const & f, result const & r_arg);
@ -230,45 +235,91 @@ class simplifier {
public:
simplifier(name const & rel, simp_rule_sets const & srss);
result operator()(expr const & e) { return simplify(e, true); }
simplifier(name const & rel): m_app_builder(*m_tmp_tctx), m_rel(rel) { }
result operator()(expr const & e, simp_rule_sets const & srss) { return simplify(e, srss); }
};
/* Constructor */
simplifier::simplifier(name const & rel, simp_rule_sets const & srss):
m_app_builder(*m_tmp_tctx), m_rel(rel), m_srss(srss) { }
/* Cache */
optional<result> simplifier::cache_lookup(expr const & e) {
auto it = m_cache.find(key(m_rel, e));
if (it != m_cache.end()) return optional<result>(it->second);
return optional<result>();
if (it == m_cache.end()) return optional<result>();
/* The cache ignores subsingletons, so we may need to
synthesize a congruence lemma. */
expr e_old = it->first.m_e;
result r_old = it->second;
lean_assert(abstract_is_equal(e, e_old));
if (e == e_old) return optional<result>(r_old);
lean_assert(is_app(e_old));
buffer<expr> new_args, old_args;
expr const & f_new = get_app_args(e, new_args);
lean_verify(f_new == get_app_args(e_old, old_args));
auto congr_lemma = mk_congr_lemma(f_new, new_args.size());
if (!congr_lemma) return optional<result>();
expr proof = congr_lemma->get_proof();
expr type = congr_lemma->get_type();
unsigned i = 0;
for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
if (ckind != congr_arg_kind::Cast) {
lean_assert(new_args[i] == old_args[i]);
}
proof = mk_app(proof, new_args[i]);
type = instantiate(binding_body(type), new_args[i]);
expr rfl;
switch (ckind) {
case congr_arg_kind::Fixed:
break;
case congr_arg_kind::Eq:
rfl = m_app_builder.mk_eq_refl(old_args[i]);
proof = mk_app(proof, old_args[i], rfl);
type = instantiate(binding_body(type), old_args[i]);
type = instantiate(binding_body(type), rfl);
break;
case congr_arg_kind::Cast:
proof = mk_app(proof, old_args[i]);
type = instantiate(binding_body(type), old_args[i]);
break;
}
i++;
});
lean_assert(is_eq(type));
result r_congr = result(e_old, proof);
return optional<result>(join(r_congr, r_old));
}
void simplifier::cache_save(expr const & e, result const & r) {
m_cache.insert(mk_pair(key(m_rel, e), r));
}
/* Results */
result simplifier::lift_from_eq(expr const & x, result const & r) {
lean_assert(!r.is_none());
expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(x));
expr motive_local = m_app_builder.mk_app(m_rel, x, l);
result simplifier::lift_from_eq(expr const & e_old, result const & r_eq) {
if (!r_eq.has_proof()) return r_eq;
lean_assert(r_eq.has_proof());
/* r_eq.get_proof() : e_old = r_eq.get_new() */
/* goal : e_old <m_rel> r_eq.get_new() */
expr l = m_tmp_tctx->mk_tmp_local(m_tmp_tctx->infer(e_old));
expr motive_local = m_app_builder.mk_app(m_rel, e_old, l);
/* motive = fun y, e_old <m_rel> y */
expr motive = Fun(l, motive_local);
expr Rxx = m_app_builder.mk_refl(m_rel, x);
expr pf = m_app_builder.mk_eq_rec(motive, Rxx, r.get_proof());
return result(r.get_new(), pf);
/* Rxx = x <m_rel> x */
expr Rxx = m_app_builder.mk_refl(m_rel, e_old);
expr pf = m_app_builder.mk_eq_rec(motive, Rxx, r_eq.get_proof());
return result(r_eq.get_new(), pf);
}
result simplifier::join(result const & r1, result const & r2) {
/* Assumes that both results are with respect to the same relation */
if (r1.is_none()) {
if (!r1.has_proof()) {
return r2;
} else if (r2.is_none()) {
return r1;
} else if (!r2.has_proof()) {
lean_assert(r1.has_proof());
return result(r2.get_new(), r1.get_proof());
} else {
/* If they both have proofs, we need to glue them together with transitivity. */
lean_assert(r1.has_proof() && r2.has_proof());
expr trans = m_app_builder.mk_trans(m_rel, r1.get_proof(), r2.get_proof());
return result(r2.get_new(), trans);
}
@ -276,20 +327,27 @@ result simplifier::join(result const & r1, result const & r2) {
result simplifier::funext(result const & r, expr const & l) {
// theorem funext {f₁ f₂ : Πx : A, B x} : (∀x, f₁ x = f₂ x) → f₁ = f₂ :=
lean_assert(!r.is_none());
expr e = Fun(l, r.get_new());
if (!r.has_proof()) return result(e);
expr pf = m_app_builder.mk_app(get_funext_name(), Fun(l, r.get_proof()));
return result(e, pf);
}
result simplifier::finalize(result const & r) {
if (!r.is_none()) return r;
if (r.has_proof()) return r;
expr pf = m_app_builder.mk_refl(m_rel, r.get_new());
return result(r.get_new(), pf);
}
/* Simplification */
result simplifier::simplify(expr const & e, simp_rule_sets const & srss) {
flet<simp_rule_sets> set_srss(m_srss, srss);
simplify_cache fresh_cache;
flet<simplify_cache> set_simplify_cache(m_cache, fresh_cache);
return simplify(e, true);
}
result simplifier::simplify(expr const & e, bool is_root) {
m_num_steps++;
flet<unsigned> inc_depth(m_depth, m_depth+1);
@ -339,39 +397,37 @@ result simplifier::simplify(expr const & e, bool is_root) {
if (!m_top_down) r = join(r, rewrite(whnf(r.get_new())));
if (r.get_new() == e && !using_eq()) {
result r_eq;
{
flet<name> use_eq(m_rel, get_eq_name());
r = simplify(r.get_new(), is_root);
r_eq = simplify(r.get_new(), is_root);
}
if (!r.is_none()) r = lift_from_eq(e, r);
r = join(r, lift_from_eq(r.get_new(), r_eq));
}
if (m_exhaustive && r.get_new() != e) r = join(r, simplify(r.get_new(), is_root));
if (m_fuse && using_eq()) r = join(r, maybe_fuse(r.get_new(), is_root));
if (m_exhaustive && r.has_proof()) r = join(r, simplify(r.get_new(), is_root));
if (m_memoize) cache_save(e, r);
if (m_fuse && using_eq()) r = join(r, maybe_fuse(r.get_new(), is_root));
return r;
}
result simplifier::simplify_lambda(expr const & _e) {
lean_assert(is_lambda(_e));
expr e = _e;
result simplifier::simplify_lambda(expr const & e) {
lean_assert(is_lambda(e));
expr t = e;
buffer<expr> ls;
while (is_lambda(e)) {
expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
expr l = m_tmp_tctx->mk_tmp_local(d, binding_info(e));
while (is_lambda(t)) {
expr d = instantiate_rev(binding_domain(t), ls.size(), ls.data());
expr l = m_tmp_tctx->mk_tmp_local(d, binding_info(t));
ls.push_back(l);
e = instantiate(binding_body(e), l);
t = instantiate(binding_body(t), l);
}
result r = simplify(e, false);
if (r.is_none()) { return result(_e); }
result r = simplify(t, false);
for (int i = ls.size() - 1; i >= 0; --i) r = funext(r, ls[i]);
return r;
}
@ -380,14 +436,31 @@ result simplifier::simplify_pi(expr const & e) {
return try_congrs(e);
}
result simplifier::simplify_app(expr const & e) {
lean_assert(is_app(e));
expr simplifier::unfold_reducible_instances(expr const & e) {
buffer<expr> args;
expr f = get_app_args(e, args);
fun_info f_info = get_fun_info(f, args.size());
int i = -1;
for_each(f_info.get_params_info(), [&](param_info const & p_info) {
i++;
if (p_info.is_inst_implicit() && !p_info.is_subsingleton()) {
// ios().get_diagnostic_channel() << "normalize: "
// << args[i] << "\n==>\n" << blast::normalize(args[i]) << "\n";
args[i] = blast::normalize(args[i]);
}
});
return mk_app(f, args);
}
result simplifier::simplify_app(expr const & _e) {
lean_assert(is_app(_e));
expr e = unfold_reducible_instances(_e);
/* (1) Try user-defined congruences */
result r = try_congrs(e);
if (!r.is_none()) {
if (using_eq()) return join(r, simplify_fun(r.get_new()));
else return r;
result r_user = try_congrs(e);
if (r_user.has_proof()) {
if (using_eq()) return join(r_user, simplify_fun(r_user.get_new()));
else return r_user;
}
/* (2) Synthesize congruence lemma */
@ -409,17 +482,13 @@ result simplifier::simplify_app(expr const & e) {
result r_f = simplify(f, false);
if (is_dependent_fn(f)) {
if (r_f.is_none()) return e;
else return congr_fun(r_f, arg);
if (r_f.has_proof()) return congr_fun(r_f, arg);
else return mk_app(r_f.get_new(), arg);
} else {
result r_arg = simplify(arg, false);
if (r_f.is_none() && r_arg.is_none()) return e;
else if (r_f.is_none()) return congr_arg(f, r_arg);
else if (r_arg.is_none()) return congr_fun(r_f, arg);
else return congr(r_f, r_arg);
return congr_fun_arg(r_f, r_arg);
}
}
return result(e);
}
@ -428,8 +497,7 @@ result simplifier::simplify_fun(expr const & e) {
buffer<expr> args;
expr const & f = get_app_args(e, args);
result r_f = simplify(f, true);
if (r_f.is_none()) return result(e);
else return congr_funs(r_f, args);
return congr_funs(r_f, args);
}
/* Proving */
@ -446,6 +514,18 @@ optional<expr> simplifier::prove(expr const & thm) {
return none_expr();
}
optional<expr> simplifier::prove(expr const & thm, simp_rule_sets const & srss) {
flet<name> set_name(m_rel, get_iff_name());
result r_cond = simplify(thm, srss);
if (is_constant(r_cond.get_new()) && const_name(r_cond.get_new()) == get_true_name()) {
expr pf = m_app_builder.mk_app(get_iff_elim_right_name(),
finalize(r_cond).get_proof(),
mk_constant(get_true_intro_name()));
return some_expr(pf);
}
return none_expr();
}
/* Rewriting */
result simplifier::rewrite(expr const & e) {
@ -453,7 +533,7 @@ result simplifier::rewrite(expr const & e) {
while (true) {
result r_ctx = rewrite(r.get_new(), m_ctx_srss);
result r_new = rewrite(r_ctx.get_new(), m_srss);
if (r_ctx.is_none() && r_new.is_none()) break;
if (!r_ctx.has_proof() && !r_new.has_proof()) break;
r = join(join(r, r_ctx), r_new);
}
return r;
@ -470,7 +550,7 @@ result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
for_each(*srs, [&](simp_rule const & sr) {
result r_new = rewrite(r.get_new(), sr);
if (r_new.is_none()) return;
if (!r_new.has_proof()) return;
r = join(r, r_new);
});
return r;
@ -504,13 +584,20 @@ result simplifier::rewrite(expr const & e, simp_rule const & sr) {
}
expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
return result(result(new_rhs, pf));
return result(new_rhs, pf);
}
/* Congruence */
result simplifier::congr_fun_arg(result const & r_f, result const & r_arg) {
if (!r_f.has_proof() && !r_arg.has_proof()) return result(mk_app(r_f.get_new(), r_arg.get_new()));
else if (!r_f.has_proof()) return congr_arg(r_f.get_new(), r_arg);
else if (!r_arg.has_proof()) return congr_fun(r_f, r_arg.get_new());
else return congr(r_f, r_arg);
}
result simplifier::congr(result const & r_f, result const & r_arg) {
lean_assert(!r_f.is_none() && !r_arg.is_none());
lean_assert(r_f.has_proof() && r_arg.has_proof());
// theorem congr {A B : Type} {f₁ f₂ : A → B} {a₁ a₂ : A} (H₁ : f₁ = f₂) (H₂ : a₁ = a₂) : f₁ a₁ = f₂ a₂
expr e = mk_app(r_f.get_new(), r_arg.get_new());
expr pf = m_app_builder.mk_congr(r_f.get_proof(), r_arg.get_proof());
@ -518,7 +605,7 @@ result simplifier::congr(result const & r_f, result const & r_arg) {
}
result simplifier::congr_fun(result const & r_f, expr const & arg) {
lean_assert(!r_f.is_none());
lean_assert(r_f.has_proof());
// theorem congr_fun {A : Type} {B : A → Type} {f g : Π x, B x} (H : f = g) (a : A) : f a = g a
expr e = mk_app(r_f.get_new(), arg);
expr pf = m_app_builder.mk_congr_fun(r_f.get_proof(), arg);
@ -526,20 +613,23 @@ result simplifier::congr_fun(result const & r_f, expr const & arg) {
}
result simplifier::congr_arg(expr const & f, result const & r_arg) {
lean_assert(!r_arg.is_none());
lean_assert(r_arg.has_proof());
// theorem congr_arg {A B : Type} {a₁ a₂ : A} (f : A → B) : a₁ = a₂ → f a₁ = f a₂
expr e = mk_app(f, r_arg.get_new());
expr pf = m_app_builder.mk_congr_arg(f, r_arg.get_proof());
return result(e, pf);
}
/* Note: handles reflexivity */
result simplifier::congr_funs(result const & r_f, buffer<expr> const & args) {
lean_assert(!r_f.is_none());
// congr_fun : ∀ {A : Type} {B : A → Type} {f g : Π (x : A), B x}, f = g → (∀ (a : A), f a = g a)
expr e = r_f.get_new();
expr pf = r_f.get_proof();
for (unsigned i = 0; i < args.size(); ++i) {
e = mk_app(e, args[i]);
}
if (!r_f.has_proof()) return result(e);
expr pf = r_f.get_proof();
for (unsigned i = 0; i < args.size(); ++i) {
pf = m_app_builder.mk_app(get_congr_fun_name(), pf, args[i]);
}
return result(e, pf);
@ -554,7 +644,7 @@ result simplifier::try_congrs(expr const & e) {
result r(e);
for_each(*crs, [&](congr_rule const & cr) {
if (!r.is_none()) return;
if (r.has_proof()) return;
r = try_congr(e, cr);
});
return r;
@ -575,42 +665,34 @@ result simplifier::try_congr(expr const & e, congr_rule const & cr) {
bool simplified = false;
list<expr> const & congr_hyps = cr.get_congr_hyps();
for_each(congr_hyps, [&](expr const & m) {
if (failed) return;
buffer<expr> ls;
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
if (failed) return;
buffer<expr> ls;
expr m_type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
while (is_pi(m_type)) {
expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type));
lean_assert(!has_metavar(l));
ls.push_back(l);
m_type = instantiate(binding_body(m_type), l);
}
expr h_rel, h_lhs, h_rhs;
lean_verify(is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
{
flet<name> set_name(m_rel, const_name(h_rel));
flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
/* We need a new cache when we add to the context */
simplify_cache fresh_cache;
flet<simplify_cache> set_simplify_cache(m_cache, fresh_cache);
h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
lean_assert(!has_metavar(h_lhs));
result r_congr_hyp = simplify(h_lhs, true);
expr hyp;
if (r_congr_hyp.is_none()) {
hyp = finalize(r_congr_hyp).get_proof();
} else {
hyp = r_congr_hyp.get_proof();
simplified = true;
while (is_pi(m_type)) {
expr d = instantiate_rev(binding_domain(m_type), ls.size(), ls.data());
expr l = tmp_tctx->mk_tmp_local(d, binding_info(m_type));
lean_assert(!has_metavar(l));
ls.push_back(l);
m_type = instantiate(binding_body(m_type), l);
}
if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true;
}
expr h_rel, h_lhs, h_rhs;
lean_verify(is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel));
{
flet<name> set_name(m_rel, const_name(h_rel));
flet<simp_rule_sets> set_ctx_srss(m_ctx_srss, add_to_srss(m_ctx_srss, ls));
h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
lean_assert(!has_metavar(h_lhs));
result r_congr_hyp = simplify(h_lhs, m_srss);
if (r_congr_hyp.has_proof()) simplified = true;
r_congr_hyp = finalize(r_congr_hyp);
expr hyp = finalize(r_congr_hyp).get_proof();
if (!tmp_tctx->is_def_eq(m, Fun(ls, hyp))) failed = true;
}
});
if (failed || !simplified) return result(e);
@ -693,7 +775,7 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
type = instantiate(binding_body(type), args[i]);
if (ckind == congr_arg_kind::Eq) {
result r_arg = simp(args[i]);
if (!r_arg.is_none()) simplified = true;
if (r_arg.has_proof()) simplified = true;
r_arg = finalize(r_arg);
proof = mk_app(proof, r_arg.get_new(), r_arg.get_proof());
type = instantiate(binding_body(type), r_arg.get_new());
@ -701,25 +783,25 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
}
i++;
});
if (simplified) {
lean_assert(is_eq(type));
buffer<expr> type_args;
get_app_args(type, type_args);
expr & new_e = type_args[2];
return optional<result>(result(new_e, proof));
} else {
return optional<result>(result(e));
}
lean_assert(is_eq(type));
buffer<expr> type_args;
get_app_args(type, type_args);
expr & new_e = type_args[2];
if (simplified) return optional<result>(result(new_e, proof));
else return optional<result>(result(new_e));
}
/* Fusion */
result simplifier::maybe_fuse(expr const & e, bool is_root) {
// ios().get_diagnostic_channel() << "maybe_fuse(" << e << ", " << is_root << ")\n";
if (!is_app(e)) return result(e);
if (is_root && is_add_app(e)) return fuse(e);
if (!is_root && is_add_app(e)) return result(e);
lean_assert(!is_add_app(e));
/* At this point we know we are an application of something other than + */
optional<result> r = synth_congr(e, [&](expr const & arg) {
// ios().get_diagnostic_channel() << "synth_fuse: " << arg << "\n";
if (is_add_app(arg)) return fuse(arg);
else return result(arg);
});
@ -729,14 +811,169 @@ result simplifier::maybe_fuse(expr const & e, bool is_root) {
result simplifier::fuse(expr const & e) {
lean_assert(is_add_app(e));
// TODO(dhs): implement fusion
return result(e);
// ios().get_diagnostic_channel() << "FUSE: " << e << "\n\n";
flet<bool> no_recursive_fusion(m_fuse, false);
/* Note: we assume all negations are on the outside of the summands */
/* Example
1. Input (e): n1 * x1 * n2 * x2 + x3 + - (x1 * x2 * n3) + (- x3) + x4
2. Split summands: (n1 * n2) * (x1 * x2) + 1 * x3 + (- n3) * (x1 * x2) + (- 1) * x3 + 1 * x4
3. Group by variable (e_grp): ((n1 * n2) * (x1 * x2) + (- n3) * (x1 * x2)) + (1 * x3 + (-1) * x3) + x4
4. Introduce locals (e_grp_ls): ((n1 * n2) * l1 + (- n3) * l1) + (1 * l2 + (-1) * l2) + l3
5. Fuse (e_fused_ls): (n1 * n2 + (- n3)) * l1 + (1 + (- 1)) * l2 + 1 * l3
6. Simplify coefficients (e_simp_ls): (n1 * n2 + (- n3)) * l1 + l3
7. Instantiate locals (e_simp): (n1 * n2 + (- n3)) * (x1 * x2) + x4
Proofs
1. Prove (1) == (3) using simplify with [ac]
2. Prove (4) == (5) using simplify with [som]
3. Prove (5) == (6) using simplify with [numeral]
4. Prove (4) == (6) by transitivity of proofs (2) and (3)
5. Prove (3) == (7) by instantiating proof (4)
6. Prove (1) == (7) by transitivity of proofs (1) and (5)
*/
/* Construct useful expressions */
buffer<expr> args;
get_app_args(e,args);
expr T = args[0];
expr f_add, f_mul, zero, one;
try {
f_add = m_app_builder.mk_partial_add(T);
f_mul = m_app_builder.mk_partial_mul(T);
zero = m_app_builder.mk_zero(T);
one = m_app_builder.mk_one(T);
expr left_distrib = m_app_builder.mk_partial_left_distrib(T);
} catch (app_builder_exception & ex) {
ios().get_diagnostic_channel() << "Cannot synthesize necessary instances\n";
return result(e);
}
/* (1 ==> 2) Split each summand into (a) numerals and (b) variables */
buffer<expr> numerals;
buffer<expr> variables;
expr s = e;
while (is_add_app(s)) {
buffer<expr> args;
expr f = get_app_args(s,args);
auto n_v = split_summand(args[2], f_mul, one);
numerals.push_back(n_v.first);
variables.push_back(n_v.second);
s = args[3];
}
auto n_v = split_summand(s, f_mul, one);
numerals.push_back(n_v.first);
variables.push_back(n_v.second);
lean_assert(numerals.size() == variables.size());
/* (2 ==> 3, 4, 5) Group the summands by variable */
expr_bi_struct_map<list<expr> > variable_to_numerals;
for (unsigned i = 0; i < numerals.size(); i++) {
auto it = variable_to_numerals.find(variables[i]);
if (it != variable_to_numerals.end()) it->second = cons(numerals[i], it->second);
else variable_to_numerals.insert({variables[i],list<expr>(numerals[i])});
}
expr e_grp = zero;
expr e_grp_ls = zero;
expr e_fused_ls = zero;
buffer<expr> locals;
variables.clear();
for (auto v_ns : variable_to_numerals) {
expr local = m_tmp_tctx->mk_tmp_local(T);
locals.push_back(local);
variables.push_back(v_ns.first);
expr term = zero;
expr term_ls = zero;
expr term_fused_ls = zero;
for_each(v_ns.second, [&](expr const & n) {
term = mk_app(f_add, mk_app(f_mul, v_ns.first, n), term);
term_ls = mk_app(f_add, mk_app(f_mul, local, n), term_ls);
term_fused_ls = mk_app(f_add, n, term_fused_ls);
});
e_grp = mk_app(f_add, term, e_grp);
e_grp_ls = mk_app(f_add, term_ls, e_grp_ls);
e_fused_ls = mk_app(f_add, mk_app(f_mul, term_fused_ls, local), e_fused_ls);
}
/* Prove (1) == (3) using simplify with [ac] */
auto pf_1_3 = prove(m_app_builder.mk_eq(e, e_grp),
get_simp_rule_sets(env(), ios(), *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);
}
/* Prove (4) == (5) using simplify with [som] */
auto pf_4_5 = prove(m_app_builder.mk_eq(e_grp_ls, e_fused_ls),
get_simp_rule_sets(env(), ios(), *g_simplify_som_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);
}
/* Prove (5) == (6) using simplify with [numeral] */
result r_simp_ls = simplify(e_fused_ls,
get_simp_rule_sets(env(), ios(), *g_simplify_numeral_namespace));
/* Prove (4) == (6) by transitivity of proofs (2) and (3) */
expr pf_4_6;
if (!r_simp_ls.has_proof()) pf_4_6 = *pf_4_5;
else pf_4_6 = m_app_builder.mk_eq_trans(*pf_4_5, r_simp_ls.get_proof());
/* Prove (3) == (7) by instantiating proof (4) */
expr pf_3_7 = mk_app(Fun(locals, pf_4_6), variables);
/* Prove (1) == (7) by transitivity of proofs (1) and (5) */
expr pf_1_7 = m_app_builder.mk_eq_trans(*pf_1_3, pf_3_7);
return result(mk_app(Fun(locals, r_simp_ls.get_new()), variables), pf_1_7);
}
expr_pair simplifier::split_summand(expr const & e, expr const & f_mul, expr const & one) {
/* [e] is a possibly negated, possibly null product, where some of the multiplicands are numerals
and the rest are treated as variables. This method does the following conversion:
- (x1 * n1 * x2 * n3) ==> (-1 * n1 * n3) * (x1 * x2) */
expr s = e;
expr numeral = one;
expr variable = one;
if (is_neg_app(s)) {
buffer<expr> args;
get_app_args(s,args);
numeral = m_app_builder.mk_app(get_neg_name(), one);
s = args[2];
}
while (is_mul_app(s)) {
buffer<expr> args;
get_app_args(s,args);
expr const & multiplicand = args[2];
if (is_num(multiplicand)) numeral = mk_app(f_mul, multiplicand, numeral);
else {
if (variable == one) variable = multiplicand;
else variable = mk_app(f_mul, multiplicand, variable);
}
s = args[3];
}
if (is_num(s)) numeral = mk_app(f_mul, s, numeral);
else {
if (variable == one) variable = s;
else variable = mk_app(f_mul, s, variable);
}
return mk_pair(numeral, variable);
}
/* Setup and teardown */
void initialize_simplifier() {
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_numeral_namespace = new name{"simplifier","numeral"};
g_simplify_max_steps = new name{"simplify", "max_steps"};
g_simplify_top_down = new name{"simplify", "top_down"};
g_simplify_exhaustive = new name{"simplify", "exhaustive"};
@ -773,11 +1010,16 @@ void finalize_simplifier() {
delete g_simplify_exhaustive;
delete g_simplify_top_down;
delete g_simplify_max_steps;
delete g_simplify_numeral_namespace;
delete g_simplify_som_namespace;
delete g_simplify_ac_namespace;
delete g_simplify_unit_namespace;
}
/* Entry point */
result simplify(name const & rel, expr const & e, simp_rule_sets const & srss) {
return simplifier(rel, srss)(e);
return simplifier(rel)(e, srss);
}
}}

13
src/library/blast/simplifier.h
View file

@ -16,22 +16,27 @@ namespace simp {
/* Struct to store results of simplification */
struct result {
/* Invariant [m_pf : m_orig <rel> m_new] */
/* Note: we only keep [m_old] to make the code easier to understand.
It could be optimized away in the future. */
expr m_new;
/* If proof is not provided, it is assumed to be reflexivity */
optional<expr> m_proof;
public:
result() {}
result(expr const & e): m_new(e) {}
result(expr const & e, expr const & pf): m_new(e), m_proof(pf) {}
result(expr const & e, optional<expr> const & pf): m_new(e), m_proof(pf) {}
result(expr const & e, expr const & proof): m_new(e), m_proof(proof) {}
result(expr const & e, optional<expr> const & proof): m_new(e), m_proof(proof) {}
bool has_proof() const { return static_cast<bool>(m_proof); }
bool is_none() const { return !static_cast<bool>(m_proof); }
expr get_new() const { return m_new; }
expr get_proof() const { lean_assert(m_proof); return *m_proof; }
/* The following assumes that [e] and [m_new] are definitionally equal */
void update(expr const & e) { m_new = e; }
};
}
simp::result simplify(name const & rel, expr const & e, simp_rule_sets const & srss);

16
src/library/constants.cpp
View file

@ -4,6 +4,9 @@
#include "util/name.h"
namespace lean{
name const * g_absurd = nullptr;
name const * g_algebra_distrib = nullptr;
name const * g_algebra_left_distrib = nullptr;
name const * g_algebra_right_distrib = nullptr;
name const * g_add = nullptr;
name const * g_and = nullptr;
name const * g_and_elim_left = nullptr;
@ -45,6 +48,7 @@ name const * g_has_one = nullptr;
name const * g_has_zero_zero = nullptr;
name const * g_has_one_one = nullptr;
name const * g_has_add = nullptr;
name const * g_has_mul = nullptr;
name const * g_heq = nullptr;
name const * g_heq_refl = nullptr;
name const * g_heq_to_eq = nullptr;
@ -173,6 +177,9 @@ name const * g_well_founded = nullptr;
name const * g_zero = nullptr;
void initialize_constants() {
g_absurd = new name{"absurd"};
g_algebra_distrib = new name{"algebra", "distrib"};
g_algebra_left_distrib = new name{"algebra", "left_distrib"};
g_algebra_right_distrib = new name{"algebra", "right_distrib"};
g_add = new name{"add"};
g_and = new name{"and"};
g_and_elim_left = new name{"and", "elim_left"};
@ -214,6 +221,7 @@ void initialize_constants() {
g_has_zero_zero = new name{"has_zero", "zero"};
g_has_one_one = new name{"has_one", "one"};
g_has_add = new name{"has_add"};
g_has_mul = new name{"has_mul"};
g_heq = new name{"heq"};
g_heq_refl = new name{"heq", "refl"};
g_heq_to_eq = new name{"heq", "to_eq"};
@ -343,6 +351,9 @@ void initialize_constants() {
}
void finalize_constants() {
delete g_absurd;
delete g_algebra_distrib;
delete g_algebra_left_distrib;
delete g_algebra_right_distrib;
delete g_add;
delete g_and;
delete g_and_elim_left;
@ -384,6 +395,7 @@ void finalize_constants() {
delete g_has_zero_zero;
delete g_has_one_one;
delete g_has_add;
delete g_has_mul;
delete g_heq;
delete g_heq_refl;
delete g_heq_to_eq;
@ -512,6 +524,9 @@ void finalize_constants() {
delete g_zero;
}
name const & get_absurd_name() { return *g_absurd; }
name const & get_algebra_distrib_name() { return *g_algebra_distrib; }
name const & get_algebra_left_distrib_name() { return *g_algebra_left_distrib; }
name const & get_algebra_right_distrib_name() { return *g_algebra_right_distrib; }
name const & get_add_name() { return *g_add; }
name const & get_and_name() { return *g_and; }
name const & get_and_elim_left_name() { return *g_and_elim_left; }
@ -553,6 +568,7 @@ name const & get_has_one_name() { return *g_has_one; }
name const & get_has_zero_zero_name() { return *g_has_zero_zero; }
name const & get_has_one_one_name() { return *g_has_one_one; }
name const & get_has_add_name() { return *g_has_add; }
name const & get_has_mul_name() { return *g_has_mul; }
name const & get_heq_name() { return *g_heq; }
name const & get_heq_refl_name() { return *g_heq_refl; }
name const & get_heq_to_eq_name() { return *g_heq_to_eq; }

4
src/library/constants.h
View file

@ -6,6 +6,9 @@ namespace lean {
void initialize_constants();
void finalize_constants();
name const & get_absurd_name();
name const & get_algebra_distrib_name();
name const & get_algebra_left_distrib_name();
name const & get_algebra_right_distrib_name();
name const & get_add_name();
name const & get_and_name();
name const & get_and_elim_left_name();
@ -47,6 +50,7 @@ name const & get_has_one_name();
name const & get_has_zero_zero_name();
name const & get_has_one_one_name();
name const & get_has_add_name();
name const & get_has_mul_name();
name const & get_heq_name();
name const & get_heq_refl_name();
name const & get_heq_to_eq_name();

4
src/library/constants.txt
View file

@ -1,4 +1,7 @@
absurd
algebra.distrib
algebra.left_distrib
algebra.right_distrib
add
and
and.elim_left
@ -40,6 +43,7 @@ has_one
has_zero.zero
has_one.one
has_add
has_mul
heq
heq.refl
heq.to_eq

2
src/library/simplifier/simp_rule_set.cpp
View file

@ -532,8 +532,8 @@ simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios,
simp_rule_sets set;
list<pair<bool, name>> const * cnames = rrs_ext::get_entries(env, ns);
if (cnames) {
tmp_type_context tctx(env, ios);
for (pair<bool, name> const & p : *cnames) {
tmp_type_context tctx(env, ios);
set = add_core(tctx, set, p.second);
}
}

2
tests/lean/simplifier12.lean
View file

@ -1,5 +1,5 @@
import algebra.simplifier
open algebra simplifier.sum_of_monomials simplifier.units
open algebra simplifier.som
set_option simplify.max_steps 1000
universe l

29
tests/lean/simplifier14.lean Normal file
View file

@ -0,0 +1,29 @@
-- 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 10000
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 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

1
tests/lean/simplifier14.lean.expected.out Normal file
View file

@ -0,0 +1 @@
TODO

19
tests/lean/simplifier15.lean Normal file
View file

@ -0,0 +1,19 @@
-- normalizing reducible non-subsingleton instances
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 pp.all true
#simplify eq null 0 x1
#simplify eq null 0 x1 + x1
#simplify eq null 0 x1 + x1 + x1
#simplify eq null 0 x1 + x1 + x1 + x1
#simplify eq null 0 x1 + x1 + (x1 + x1) + x1
#simplify eq simplifier.ac 0 x1 + x1 + x1
#simplify eq simplifier.ac 0 x1 + x1 + x1 + x1
#simplify eq simplifier.ac 0 x1 + x1 + (x1 + x1) + x1

24
tests/lean/simplifier15.lean.expected.out Normal file
View file

@ -0,0 +1,24 @@
(refl): x1
(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1
(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
x1
(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
x1)
x1
(refl): @add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s))
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1))
x1
@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)
@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1))
@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1
(@add.{l} T (@has_add.mk.{l} T (@algebra.comm_ring.add.{l} T s)) x1 x1)))

15
tests/lean/simplifier16.lean Normal file
View file

@ -0,0 +1,15 @@
-- Canonicalizing subsingletons
import algebra.ring
open algebra
set_option pp.all true
universes l j k
constants (A : Type.{l}) (s : comm_ring A)
attribute s [instance]
constants (x y : A) (P : A → Type.{j}) (P_ss : ∀ a, subsingleton (P a))
constants (f : Π a, P a → A) (Px1 Px2 Px3 : P x)
constants (g : A → A → A)
attribute P_ss [instance]
#simplify eq env 0 g (f x Px1) (f x Px2)
#simplify eq env 0 g (f x Px1) (g (f x Px2) (f x Px3))

2
tests/lean/simplifier16.lean.expected.out Normal file
View file

@ -0,0 +1,2 @@
g (f x Px1) (f x Px1)
g (f x Px1) (g (f x Px1) (f x Px1))