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

feat(library/blast/simplifier): basic infrastructure

Browse source
This commit is contained in:
Daniel Selsam 2015-11-04 21:53:12 -08:00 committed by Leonardo de Moura
parent 78a9116a23
commit 8e5e8e6540
27 changed files with 1017 additions and 121 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -45,6 +45,8 @@ Author: Leonardo de Moura
#include "library/congr_lemma_manager.h"
#include "library/definitional/projection.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier.h"
#include "compiler/preprocess_rec.h"
#include "frontends/lean/util.h"
#include "frontends/lean/parser.h"
@ -475,7 +477,7 @@ static void print_simp_rules(parser & p) {
if (p.curr_is_identifier()) {
ns = p.get_name_val();
p.next();
s = get_simp_rule_sets(p.env(), ns);
s = get_simp_rule_sets(p.env(), p.ios(), ns);
} else {
s = get_simp_rule_sets(p.env());
}
@ -1311,6 +1313,38 @@ static environment congr_lemma_cmd(parser & p) {
return env;
}
static environment simplify_cmd(parser & p) {
name rel = p.check_constant_next("invalid #simplify command, constant 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::branch b;
blast::simp::result r = blast::simplify(b,rel,e);
flycheck_information info(p.regular_stream());
if (info.enabled()) {
p.display_information_pos(p.cmd_pos());
p.regular_stream() << "simplify result:\n";
}
if (r.is_none()) {
p.regular_stream() << "<refl>" << endl;
}
else {
auto tc = mk_type_checker(p.env(), p.mk_ngen());
expr pf_type = tc->check(r.get_proof(), ls).first;
if (o == 0) p.regular_stream() << r.get_new() << endl;
else if (o == 1) p.regular_stream() << r.get_proof() << endl;
else p.regular_stream() << pf_type << endl;
}
return p.env();
}
void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("open", "create aliases for declarations, and use objects defined in other namespaces",
open_cmd));
@ -1344,6 +1378,7 @@ void init_cmd_table(cmd_table & r) {
add_cmd(r, cmd_info("#accessible", "(for debugging purposes) display number of accessible declarations for blast tactic", accessible_cmd));
add_cmd(r, cmd_info("#decl_stats", "(for debugging purposes) display declaration statistics", decl_stats_cmd));
add_cmd(r, cmd_info("#relevant_thms", "(for debugging purposes) select relevant theorems using Meng&Paulson heuristic", relevant_thms_cmd));
add_cmd(r, cmd_info("#simplify", "(for debugging purposes) simplify given expression", simplify_cmd));
register_decl_cmds(r);
register_inductive_cmd(r);

2
src/frontends/lean/token_table.cpp
View file

@ -120,7 +120,7 @@ void init_token_table(token_table & t) {
"add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
"multiple_instances", "find_decl", "attribute", "persistent",
"include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",
"#compile", "#accessible", "#decl_stats", "#relevant_thms", "#app_builder", "#refl", "#symm",
"#compile", "#accessible", "#decl_stats", "#relevant_thms", "#simplify", "#app_builder", "#refl", "#symm",
"#trans", "#replace", "#congr", nullptr};
pair<char const *, char const *> aliases[] =

2
src/library/blast/CMakeLists.txt
View file

@ -1,2 +1,2 @@
add_library(blast OBJECT expr.cpp branch.cpp state.cpp blast.cpp
blast_tactic.cpp init_module.cpp)
blast_tactic.cpp init_module.cpp simplifier.cpp)

3
src/library/blast/init_module.cpp
View file

@ -8,16 +8,19 @@ Author: Leonardo de Moura
#include "library/blast/branch.h"
#include "library/blast/blast.h"
#include "library/blast/blast_tactic.h"
#include "library/blast/simplifier.h"
namespace lean {
void initialize_blast_module() {
blast::initialize_expr();
blast::initialize_branch();
initialize_blast();
blast::initialize_simplifier();
initialize_blast_tactic();
}
void finalize_blast_module() {
finalize_blast_tactic();
blast::finalize_simplifier();
finalize_blast();
blast::finalize_branch();
blast::finalize_expr();

621
src/library/blast/simplifier.cpp Normal file
View file

@ -0,0 +1,621 @@
/*
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"
#include "kernel/instantiate.h"
#include "library/constants.h"
#include "library/expr_lt.h"
#include "library/class_instance_resolution.h"
#include "library/relation_manager.h"
#include "library/blast/expr.h"
#include "library/blast/blast_exception.h"
#include "library/blast/blast.h"
#include "library/blast/simplifier.h"
#include "library/simplifier/simp_rule_set.h"
#include "library/simplifier/ceqv.h"
#include "library/app_builder.h"
#include "util/flet.h"
#include "util/pair.h"
#include "util/sexpr/option_declarations.h"
#include <array>
#include <iostream> // TODO just for occasional debugging
#ifndef LEAN_DEFAULT_SIMPLIFY_MAX_STEPS
#define LEAN_DEFAULT_SIMPLIFY_MAX_STEPS 100
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_TOP_DOWN
#define LEAN_DEFAULT_SIMPLIFY_TOP_DOWN false
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE
#define LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_MEMOIZE
#define LEAN_DEFAULT_SIMPLIFY_MEMOIZE true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL
#define LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL true
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS
#define LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS false
#endif
#ifndef LEAN_DEFAULT_SIMPLIFY_TRACE
#define LEAN_DEFAULT_SIMPLIFY_TRACE false
#endif
namespace lean {
namespace blast {
using simp::result;
/* Options */
static name * g_simplify_max_steps = nullptr;
static name * g_simplify_top_down = nullptr;
static name * g_simplify_exhaustive = nullptr;
static name * g_simplify_memoize = nullptr;
static name * g_simplify_contextual = nullptr;
static name * g_simplify_expand_macros = nullptr;
static name * g_simplify_trace = nullptr;
unsigned get_simplify_max_steps() {
return ios().get_options().get_unsigned(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS);
}
bool get_simplify_top_down() {
return ios().get_options().get_bool(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN);
}
bool get_simplify_exhaustive() {
return ios().get_options().get_bool(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE);
}
bool get_simplify_memoize() {
return ios().get_options().get_bool(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE);
}
bool get_simplify_contextual() {
return ios().get_options().get_bool(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL);
}
bool get_simplify_expand_macros() {
return ios().get_options().get_bool(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS);
}
bool get_simplify_trace() {
return ios().get_options().get_bool(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE);
}
/* Main simplifier class */
class simplifier {
blast_tmp_type_context m_tmp_tctx;
app_builder m_app_builder;
branch m_branch;
name m_rel;
list<expr> m_local_ctx;
/* Logging */
unsigned m_num_steps{0};
unsigned m_depth{0};
/* Options */
unsigned m_max_steps{get_simplify_max_steps()};
bool m_top_down{get_simplify_top_down()};
bool m_exhaustive{get_simplify_exhaustive()};
bool m_memoize{get_simplify_memoize()};
bool m_contextual{get_simplify_contextual()};
bool m_expand_macros{get_simplify_expand_macros()};
bool m_trace{get_simplify_trace()};
/* Cache */
expr_bi_struct_map<result> m_simplify_cache{};
/* Masks for building applications */
std::array<bool,6> eq_rec_all_mask{{true,true,true,true,true,true}};
/* Basic helpers */
bool using_eq() { return m_rel == get_eq_name(); }
bool is_dependent_fn(expr const & f) {
expr f_type = m_tmp_tctx->whnf(m_tmp_tctx->infer(f));
lean_assert(is_pi(f_type));
return has_free_vars(binding_body(f_type));
}
/* Results */
result lift_from_eq(expr const & x, result const & r);
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);
result simplify_lambda(expr const & e);
result simplify_pi(expr const & e);
result simplify_app(expr const & e);
result simplify_fun(expr const & e);
/* Rewriting */
result rewrite(expr const & e);
result rewrite(expr const & e, simp_rule const & sr);
void init_tmp_tctx_for(simp_rule_core const & sr);
/* Congruence */
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);
result congr_funs(result const & r_f, buffer<expr> const & args);
result try_congrs(expr const & e);
result try_congr(expr const & e, congr_rule const & cr);
public:
simplifier(branch const & b, name const & rel);
result operator()(expr const & e) { return simplify(e); }
};
/* Constructor */
simplifier::simplifier(branch const & b, name const & rel):
m_app_builder(*m_tmp_tctx), m_branch(b), m_rel(rel) { }
/* 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));
auto motive_local = m_app_builder.mk_app(m_rel,x,l);
lean_assert(motive_local);
expr motive = Fun(l,*motive_local);
auto Rxx = m_app_builder.mk_refl(m_rel,x);
lean_assert(Rxx);
auto pf = m_app_builder.mk_eq_rec(motive,*Rxx,r.get_proof());
return result(r.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()) {
return r2;
}
else if (r2.is_none()) {
return r1;
}
else {
auto trans = m_app_builder.mk_trans(m_rel,r1.get_proof(),r2.get_proof());
lean_assert(trans);
return result(r2.get_new(),*trans);
}
}
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 (auto pf = m_app_builder.mk_app(get_funext_name(),Fun(l,r.get_proof())))
return result(e,*pf);
else
throw blast_exception("failed on [funext] matching",e);
}
result simplifier::finalize(result const & r) {
if (!r.is_none()) return r;
if (auto pf = m_app_builder.mk_refl(m_rel,r.get_new()))
return result(r.get_new(),*pf);
else
throw blast_exception("failed on [refl] matching",r.get_new());
}
/* Simplification */
result simplifier::simplify(expr const & e) {
m_num_steps++;
flet<unsigned> inc_depth(m_depth, m_depth+1);
if (m_trace) {
ios().get_diagnostic_channel() << m_num_steps << "." << m_depth << "." << m_rel << ": " << e << "\n";
}
if (m_num_steps > m_max_steps)
throw blast_exception("simplifier failed, maximum number of steps exceeded", e);
if (m_memoize) {
auto it = m_simplify_cache.find(e);
if (it != m_simplify_cache.end()) return it->second;
}
result r(e);
if (m_top_down) r = join(r, rewrite(whnf(r.get_new())));
r.update(whnf(r.get_new()));
switch (r.get_new().kind()) {
case expr_kind::Local:
case expr_kind::Meta:
case expr_kind::Sort:
case expr_kind::Constant:
// no-op
break;
case expr_kind::Var:
lean_unreachable();
case expr_kind::Macro:
/* TODO
if (m_expand_macros) {
if (auto m = blast::expand_macro(e)) r = join(r,simplify(whnf(*m)));
}
*/
break;
case expr_kind::Lambda:
if (using_eq()) r = join(r,simplify_lambda(r.get_new()));
break;
case expr_kind::Pi:
r = join(r,simplify_pi(r.get_new()));
break;
case expr_kind::App:
r = join(r,simplify_app(r.get_new()));
break;
}
if (!m_top_down) r = join(r,rewrite(whnf(r.get_new())));
if (r.get_new() == e && !using_eq()) {
{
flet<name> use_eq(m_rel, get_eq_name());
r = simplify(r.get_new());
}
if (!r.is_none()) r = lift_from_eq(e,r);
}
if (m_exhaustive && r.get_new() != e) r = join(r,simplify(r.get_new()));
if (m_memoize) m_simplify_cache.insert(mk_pair(e, r));
return r;
}
result simplifier::simplify_lambda(expr const & _e) {
lean_assert(is_lambda(_e));
expr e = _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));
ls.push_back(l);
e = instantiate(binding_body(e),l);
}
result r = simplify(e);
if (r.is_none()) { return result(_e); }
for (int i = ls.size() - 1; i >= 0; --i) r = funext(r,ls[i]);
return r;
}
result simplifier::simplify_pi(expr const & e) {
lean_assert(is_pi(e));
return try_congrs(e);
}
result simplifier::simplify_app(expr const & e) {
lean_assert(is_app(e));
// TODO simplify operator as well, in cases (1) and (2)
/* (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;
}
/* (2) Synthesize congruence lemma */
if (using_eq()) {
// TODO
}
/* (3) Fall back on generic binary congruence */
if (using_eq()) {
expr const & f = app_fn(e);
expr const & arg = app_arg(e);
result r_f = simplify(f);
if (is_dependent_fn(f)) {
if (r_f.is_none()) return e;
else return congr_fun(r_f,arg);
}
else {
result r_arg = simplify(arg);
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 result(e);
}
result simplifier::simplify_fun(expr const & e) {
lean_assert(is_app(e));
buffer<expr> args;
expr const & f = get_app_args(e, args);
result r_f = simplify(f);
if (r_f.is_none()) return result(e);
else return congr_funs(simplify(f),args);
}
/* Rewriting */
result simplifier::rewrite(expr const & e) {
result r(e);
/* First, we rewrite with local hypotheses */
//TODO
/* Next, we rewrite with the [simp_rule_set] */
simp_rule_set const * sr = get_simp_rule_sets(env()).find(m_rel);
if (!sr) return r;
list<simp_rule> const * srs = sr->find_simp(e);
if (!srs) return r;
for_each(*srs,[&](simp_rule const & sr) { r = join(r,rewrite(r.get_new(),sr)); });
return r;
}
result simplifier::rewrite(expr const & e, simp_rule const & sr) {
// TODO restore
// blast_tmp_type_context tmp_tctx(sr.get_num_umeta(),sr.get_num_emeta());
blast_tmp_type_context tmp_tctx;
tmp_tctx->clear();
tmp_tctx->set_next_uvar_idx(sr.get_num_umeta());
tmp_tctx->set_next_mvar_idx(sr.get_num_emeta());
if (!tmp_tctx->is_def_eq(e,sr.get_lhs())) return result(e);
/* Traverse metavariables backwards */
for (int i = sr.get_num_emeta() - 1; i >= 0; --i) {
expr const & m = sr.get_emeta(i);
bool is_instance = sr.is_instance(i);
if (is_instance) {
expr type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
if (auto v = tmp_tctx->mk_class_instance(type)) {
if (!tmp_tctx->force_assign(m, *v))
return result(e);
} else {
return result(e);
}
}
if (tmp_tctx->is_mvar_assigned(i)) continue;
if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
// TODO try to prove
return result(e);
}
/* We fail if there is a meta variable that we still cannot assign */
return result(e);
}
for (unsigned i = 0; i < sr.get_num_umeta(); i++) {
if (!tmp_tctx->is_uvar_assigned(i)) return result(e);
}
expr e_s = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
if (sr.is_perm() && !is_lt(e_s,e,false)) return result(e);
expr pf = tmp_tctx->instantiate_uvars_mvars(sr.get_proof());
return result(result(e_s,pf));
}
/* Congruence */
result simplifier::congr(result const & r_f, result const & r_arg) {
lean_assert(!r_f.is_none() && !r_arg.is_none());
// 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());
if (auto pf = m_app_builder.mk_app(get_congr_name(),r_f.get_proof(),r_arg.get_proof()))
return result(e,*pf);
else
throw blast_exception("failed on [congr] matching",e);
}
result simplifier::congr_fun(result const & r_f, expr const & arg) {
lean_assert(!r_f.is_none());
// 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);
if (auto pf = m_app_builder.mk_app(get_congr_fun_name(),r_f.get_proof(),arg))
return result(e,*pf);
else
throw blast_exception("failed on [congr_fun] matching",e);
}
result simplifier::congr_arg(expr const & f, result const & r_arg) {
lean_assert(!r_arg.is_none());
// 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());
if (auto pf = m_app_builder.mk_app(get_congr_arg_name(),f,r_arg.get_proof()))
return result(e,*pf);
else
throw blast_exception("failed on [congr_arg] matching",e);
}
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]);
auto p = m_app_builder.mk_app(get_congr_fun_name(),pf,args[i]);
if (p) pf = *p;
else throw blast_exception("failed on [congr_fun] matching",e);
}
return result(e,pf);
}
result simplifier::try_congrs(expr const & e) {
simp_rule_set const * sr = get_simp_rule_sets(env()).find(m_rel);
if (!sr) return result(e);
list<congr_rule> const * crs = sr->find_congr(e);
if (!crs) return result(e);
result r(e);
for_each(*crs,[&](congr_rule const & cr) {
if (!r.is_none()) return;
r = try_congr(e,cr);
});
return r;
}
result simplifier::try_congr(expr const & e, congr_rule const & cr) {
// TODO restore
// blast_tmp_type_context tmp_tctx(cr.get_num_umeta(),cr.get_num_emeta());
blast_tmp_type_context tmp_tctx;
tmp_tctx->clear();
tmp_tctx->set_next_uvar_idx(cr.get_num_umeta());
tmp_tctx->set_next_mvar_idx(cr.get_num_emeta());
if (!tmp_tctx->is_def_eq(e,cr.get_lhs())) return result(e);
/* First, iterate over the congruence hypotheses */
bool failed = false;
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->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(e));
ls.push_back(l);
m_type = instantiate(binding_body(m_type),l);
}
expr h_rel, h_lhs, h_rhs;
bool valid = is_simp_relation(env(), m_type, h_rel, h_lhs, h_rhs) && is_constant(h_rel);
lean_assert(valid);
{
flet<name> set_name(m_rel,const_name(h_rel));
flet<list<expr>> set_local_ctx(m_local_ctx,to_list(ls));
h_lhs = tmp_tctx->instantiate_uvars_mvars(h_lhs);
result r_congr_hyp = simplify(h_lhs);
expr hyp;
if (r_congr_hyp.is_none()) {
hyp = finalize(r_congr_hyp).get_proof();
}
else {
hyp = r_congr_hyp.get_proof();
simplified = true;
}
hyp = Fun(ls,hyp);
if (!tmp_tctx->is_def_eq(m,hyp)) failed = true;
}
});
if (failed || !simplified) return result(e);
/* Traverse metavariables backwards, proving or synthesizing the rest */
for (int i = cr.get_num_emeta() - 1; i >= 0; --i) {
expr const & m = cr.get_emeta(i);
bool is_instance = cr.is_instance(i);
if (is_instance) {
expr type = tmp_tctx->instantiate_uvars_mvars(tmp_tctx->infer(m));
if (auto v = tmp_tctx->mk_class_instance(type)) {
if (!tmp_tctx->force_assign(m, *v))
return result(e);
} else {
return result(e);
}
}
if (tmp_tctx->is_mvar_assigned(i)) continue;
if (tmp_tctx->is_prop(tmp_tctx->infer(m))) {
// TODO try to prove
return result(e);
}
/* We fail if there is a meta variable that we still cannot assign */
return result(e);
}
for (unsigned i = 0; i < cr.get_num_umeta(); i++) {
if (!tmp_tctx->is_uvar_assigned(i)) return result(e);
}
expr e_s = tmp_tctx->instantiate_uvars_mvars(cr.get_rhs());
expr pf = tmp_tctx->instantiate_uvars_mvars(cr.get_proof());
return result(e_s,pf);
}
/* Setup and teardown */
void initialize_simplifier() {
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"};
g_simplify_memoize = new name{"simplify", "memoize"};
g_simplify_contextual = new name{"simplify", "contextual"};
g_simplify_expand_macros = new name{"simplify", "expand_macros"};
g_simplify_trace = new name{"simplify", "trace"};
register_unsigned_option(*g_simplify_max_steps, LEAN_DEFAULT_SIMPLIFY_MAX_STEPS,
"(simplify) max allowed steps in simplification");
register_bool_option(*g_simplify_top_down, LEAN_DEFAULT_SIMPLIFY_TOP_DOWN,
"(simplify) use top-down rewriting instead of bottom-up");
register_bool_option(*g_simplify_exhaustive, LEAN_DEFAULT_SIMPLIFY_EXHAUSTIVE,
"(simplify) rewrite exhaustively");
register_bool_option(*g_simplify_memoize, LEAN_DEFAULT_SIMPLIFY_MEMOIZE,
"(simplify) memoize simplifications");
register_bool_option(*g_simplify_contextual, LEAN_DEFAULT_SIMPLIFY_CONTEXTUAL,
"(simplify) use contextual simplification");
register_bool_option(*g_simplify_expand_macros, LEAN_DEFAULT_SIMPLIFY_EXPAND_MACROS,
"(simplify) expand macros");
register_bool_option(*g_simplify_trace, LEAN_DEFAULT_SIMPLIFY_TRACE,
"(simplify) trace");
}
void finalize_simplifier() {
delete g_simplify_trace;
delete g_simplify_expand_macros;
delete g_simplify_contextual;
delete g_simplify_memoize;
delete g_simplify_exhaustive;
delete g_simplify_top_down;
delete g_simplify_max_steps;
}
/* Entry point */
result simplify(branch const & b, name const & rel, expr const & e) {
return simplifier(b,rel)(e);
}
}}

43
src/library/blast/simplifier.h Normal file
View file

@ -0,0 +1,43 @@
/*
Copyright (c) 2015 Daniel Selsam. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Daniel Selsam
*/
#pragma once
#include "kernel/expr_pair.h"
#include "library/blast/branch.h"
namespace lean {
namespace blast {
namespace simp {
/* Struct to store results of simplification */
struct result {
/* Invariant [m_pf : m_orig <rel> m_new] */
expr m_new;
optional<expr> m_proof;
public:
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) {}
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(branch const & b, name const & rel, expr const & e);
void initialize_simplifier();
void finalize_simplifier();
}
}

4
src/library/constants.cpp
View file

@ -178,6 +178,8 @@ void initialize_constants() {
g_congr = new name{"congr"};
g_congr_arg = new name{"congr_arg"};
g_congr_fun = new name{"congr_fun"};
g_congr_fun = new name{"congr_fun"};
g_congr_arg = new name{"congr_arg"};
g_dite = new name{"dite"};
g_div = new name{"div"};
g_empty = new name{"empty"};
@ -336,9 +338,9 @@ void finalize_constants() {
delete g_bool_tt;
delete g_char;
delete g_char_mk;
delete g_congr;
delete g_congr_arg;
delete g_congr_fun;
delete g_congr;
delete g_dite;
delete g_div;
delete g_empty;

40
src/library/simplifier/ceqv.cpp
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "kernel/type_checker.h"
#include "kernel/abstract.h"
#include "kernel/instantiate.h"
#include "kernel/for_each_fn.h"
@ -15,7 +14,7 @@ Author: Leonardo de Moura
#include "library/simplifier/ceqv.h"
namespace lean {
bool is_ceqv(type_checker & tc, expr e);
bool is_ceqv(tmp_type_context & tctx, expr e);
bool is_simp_relation(environment const & env, name const & n) {
return is_trans_relation(env, n) && is_refl_relation(env, n);
@ -24,14 +23,14 @@ bool is_simp_relation(environment const & env, name const & n) {
/** \brief Auxiliary functional object for creating "conditional equations" */
class to_ceqvs_fn {
environment const & m_env;
type_checker & m_tc;
tmp_type_context & m_tctx;
static list<expr_pair> mk_singleton(expr const & e, expr const & H) {
return list<expr_pair>(mk_pair(e, H));
}
bool is_type(expr const & e) {
return is_sort(m_tc.whnf(m_tc.infer(e).first).first);
return is_sort(m_tctx.whnf(m_tctx.infer(e)));
}
bool is_relation(expr const & e) {
@ -48,8 +47,7 @@ class to_ceqvs_fn {
}
bool is_prop(expr const & e) {
constraint_seq cs;
return m_tc.is_prop(e, cs) && !cs;
return m_tctx.is_prop(e);
}
// If restricted is true, we don't use (e <-> true) rewrite
@ -69,7 +67,8 @@ class to_ceqvs_fn {
auto r2 = apply(arg2, H2, restrited);
return append(r1, r2);
} else if (is_pi(e)) {
expr local = mk_local(m_tc.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
// TODO(dhs): keep name?
expr local = m_tctx.mk_tmp_local(binding_domain(e), binding_info(e));
expr new_e = instantiate(binding_body(e), local);
expr new_H = mk_app(H, local);
auto r = apply(new_e, new_H, restrited);
@ -83,9 +82,9 @@ class to_ceqvs_fn {
}
} else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2) && is_prop(e)) {
// TODO(Leo): support HoTT mode if users request
expr not_c = mk_not(m_tc, c);
expr Hc = mk_local(m_tc.mk_fresh_name(), c);
expr Hnc = mk_local(m_tc.mk_fresh_name(), not_c);
expr not_c = mk_app(mk_constant(get_not_name()), c);
expr Hc = m_tctx.mk_tmp_local(c);
expr Hnc = m_tctx.mk_tmp_local(not_c);
expr H1 = mk_app({mk_constant(get_implies_of_if_pos_name()),
c, arg1, arg2, Hdec, e, Hc});
expr H2 = mk_app({mk_constant(get_implies_of_if_neg_name()),
@ -94,9 +93,8 @@ class to_ceqvs_fn {
auto r2 = lift(Hnc, apply(arg2, H2, restrited));
return append(r1, r2);
} else if (!restrited) {
constraint_seq cs;
expr new_e = m_tc.whnf(e, cs);
if (new_e != e && !cs) {
expr new_e = m_tctx.whnf(e);
if (new_e != e) {
if (auto r = apply(new_e, H, true))
return r;
}
@ -112,17 +110,17 @@ class to_ceqvs_fn {
}
}
public:
to_ceqvs_fn(type_checker & tc):m_env(tc.env()), m_tc(tc) {}
to_ceqvs_fn(tmp_type_context & tctx):m_env(tctx.env()), m_tctx(tctx) {}
list<expr_pair> operator()(expr const & e, expr const & H) {
bool restrited = false;
list<expr_pair> lst = apply(e, H, restrited);
return filter(lst, [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
return filter(lst, [&](expr_pair const & p) { return is_ceqv(m_tctx, p.first); });
}
};
list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H) {
return to_ceqvs_fn(tc)(e, H);
list<expr_pair> to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H) {
return to_ceqvs_fn(tctx)(e, H);
}
bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
@ -143,7 +141,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & lhs, expr
return is_simp_relation(env, e, rel, lhs, rhs);
}
bool is_ceqv(type_checker & tc, expr e) {
bool is_ceqv(tmp_type_context & tctx, expr e) {
if (has_expr_metavar(e))
return false;
name_set to_find;
@ -158,7 +156,7 @@ bool is_ceqv(type_checker & tc, expr e) {
return true;
}
};
environment const & env = tc.env();
environment const & env = tctx.env();
bool is_std = is_standard(env);
buffer<expr> hypotheses; // arguments that are propositions
while (is_pi(e)) {
@ -168,11 +166,11 @@ bool is_ceqv(type_checker & tc, expr e) {
// by matching the type.
for_each(binding_domain(e), visitor_fn);
}
expr local = mk_local(tc.mk_fresh_name(), binding_domain(e));
expr local = tctx.mk_tmp_local(binding_domain(e));
if (binding_info(e).is_inst_implicit()) {
// If the argument can be instantiated by type class resolution, then
// we don't need to find it in the lhs
} else if (is_std && tc.is_prop(binding_domain(e)).first) {
} else if (is_std && tctx.is_prop(binding_domain(e))) {
// If the argument is a proposition, we store it in hypotheses.
// We check whether the lhs occurs in hypotheses or not.
hypotheses.push_back(binding_domain(e));

6
src/library/simplifier/ceqv.h
View file

@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/type_checker.h"
#include "library/tmp_type_context.h"
#include "library/expr_pair.h"
namespace lean {
@ -14,7 +14,7 @@ bool is_simp_relation(environment const & env, expr const & e, expr & rel, expr
a "conditional" rewriting rule. Any equivalence relation registered using
the relation_manager is considered.
*/
list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H);
bool is_ceqv(type_checker & tc, expr e);
list<expr_pair> to_ceqvs(tmp_type_context & tctx, expr const & e, expr const & H);
bool is_ceqv(tmp_type_context & tctx, expr e);
bool is_permutation_ceqv(environment const & env, expr e);
}

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

@ -16,13 +16,14 @@ Author: Leonardo de Moura
#include "library/simplifier/simp_rule_set.h"
namespace lean {
simp_rule_core::simp_rule_core(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof):
m_id(id), m_univ_metas(univ_metas), m_metas(metas), m_lhs(lhs), m_rhs(rhs), m_proof(proof) {}
simp_rule_core::simp_rule_core(name const & id, levels const & umetas, std::vector<expr> const & emetas,
std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof):
m_id(id), m_umetas(umetas), m_emetas(emetas), m_instances(instances),
m_lhs(lhs), m_rhs(rhs), m_proof(proof) {}
simp_rule::simp_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof, bool is_perm):
simp_rule_core(id, univ_metas, metas, lhs, rhs, proof),
simp_rule::simp_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm):
simp_rule_core(id, umetas, emetas, instances, lhs, rhs, proof),
m_is_permutation(is_perm) {}
bool operator==(simp_rule const & r1, simp_rule const & r2) {
@ -31,18 +32,19 @@ bool operator==(simp_rule const & r1, simp_rule const & r2) {
format simp_rule::pp(formatter const & fmt) const {
format r;
r += format("#") + format(length(m_metas));
r += format("#") + format(get_num_emeta());
if (m_is_permutation)
r += space() + format("perm");
format r1 = comma() + space() + fmt(m_lhs);
r1 += space() + format("↦") + pp_indent_expr(fmt, m_rhs);
format r1 = comma() + space() + fmt(get_lhs());
r1 += space() + format("↦") + pp_indent_expr(fmt, get_rhs());
r += group(r1);
return r;
}
congr_rule::congr_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof, list<expr> const & congr_hyps):
simp_rule_core(id, univ_metas, metas, lhs, rhs, proof),
congr_rule::congr_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
list<expr> const & congr_hyps):
simp_rule_core(id, umetas, emetas, instances, lhs, rhs, proof),
m_congr_hyps(congr_hyps) {}
bool operator==(congr_rule const & r1, congr_rule const & r2) {
@ -51,15 +53,15 @@ bool operator==(congr_rule const & r1, congr_rule const & r2) {
format congr_rule::pp(formatter const & fmt) const {
format r;
r += format("#") + format(length(m_metas));
r += format("#") + format(get_num_emeta());
format r1;
for (expr const & h : m_congr_hyps) {
r1 += space() + paren(fmt(mlocal_type(h)));
}
r += group(r1);
r += space() + format(":") + space();
format r2 = paren(fmt(m_lhs));
r2 += space() + format("↦") + space() + paren(fmt(m_rhs));
format r2 = paren(fmt(get_lhs()));
r2 += space() + format("↦") + space() + paren(fmt(get_rhs()));
r += group(r2);
return r;
}
@ -253,33 +255,34 @@ format simp_rule_sets::pp(formatter const & fmt) const {
static name * g_prefix = nullptr;
simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s,
simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s,
name const & id, levels const & univ_metas, expr const & e, expr const & h) {
list<expr_pair> ceqvs = to_ceqvs(tc, e, h);
environment const & env = tc.env();
list<expr_pair> ceqvs = to_ceqvs(tctx, e, h);
environment const & env = tctx.env();
simp_rule_sets new_s = s;
for (expr_pair const & p : ceqvs) {
expr new_e = p.first;
expr new_h = p.second;
bool is_perm = is_permutation_ceqv(env, new_e);
buffer<expr> metas;
unsigned idx = 0;
while (is_pi(new_e)) {
expr mvar = mk_metavar(name(*g_prefix, idx), binding_domain(new_e));
idx++;
metas.push_back(mvar);
new_e = instantiate(binding_body(new_e), mvar);
expr rule = tctx.whnf(p.first);
expr proof = tctx.whnf(p.second);
bool is_perm = is_permutation_ceqv(env, rule);
std::vector<expr> emetas;
std::vector<bool> instances;
while (is_pi(rule)) {
expr mvar = tctx.mk_mvar(binding_domain(rule));
emetas.push_back(mvar);
instances.push_back(binding_info(rule).is_inst_implicit());
rule = tctx.whnf(instantiate(binding_body(rule), mvar));
proof = mk_app(proof,mvar);
}
expr rel, lhs, rhs;
if (is_simp_relation(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
new_s.insert(const_name(rel), simp_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm));
if (is_simp_relation(env, rule, rel, lhs, rhs) && is_constant(rel)) {
new_s.insert(const_name(rel), simp_rule(id, univ_metas, emetas, instances, lhs, rhs, proof, is_perm));
}
}
return new_s;
}
simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h) {
return add_core(tc, s, id, list<level>(), e, h);
simp_rule_sets add(tmp_type_context & tctx, simp_rule_sets const & s, name const & id, expr const & e, expr const & h) {
return add_core(tctx, s, id, list<level>(), e, h);
}
simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2) {
@ -293,17 +296,17 @@ simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2) {
static name * g_class_name = nullptr;
static std::string * g_key = nullptr;
static simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s, name const & cname) {
declaration const & d = tc.env().get(cname);
static simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s, name const & cname) {
declaration const & d = tctx.env().get(cname);
buffer<level> us;
unsigned num_univs = d.get_num_univ_params();
for (unsigned i = 0; i < num_univs; i++) {
us.push_back(mk_meta_univ(name(*g_prefix, i)));
us.push_back(tctx.mk_uvar());
}
levels ls = to_list(us);
expr e = instantiate_type_univ_params(d, ls);
expr e = tctx.whnf(instantiate_type_univ_params(d, ls));
expr h = mk_constant(cname, ls);
return add_core(tc, s, cname, ls, e, h);
return add_core(tctx, s, cname, ls, e, h);
}
@ -350,30 +353,30 @@ static bool is_valid_congr_hyp_rhs(expr const & rhs, name_set & found_mvars) {
return true;
}
void add_congr_core(environment const & env, simp_rule_sets & s, name const & n) {
declaration const & d = env.get(n);
type_checker tc(env);
void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n) {
declaration const & d = tctx.env().get(n);
buffer<level> us;
unsigned num_univs = d.get_num_univ_params();
for (unsigned i = 0; i < num_univs; i++) {
us.push_back(mk_meta_univ(name(*g_prefix, i)));
us.push_back(tctx.mk_uvar());
}
levels ls = to_list(us);
expr pr = mk_constant(n, ls);
expr e = instantiate_type_univ_params(d, ls);
buffer<bool> explicit_args;
buffer<expr> metas;
unsigned idx = 0;
while (is_pi(e)) {
expr mvar = mk_metavar(name(*g_prefix, idx), binding_domain(e));
idx++;
explicit_args.push_back(is_explicit(binding_info(e)));
metas.push_back(mvar);
e = instantiate(binding_body(e), mvar);
pr = mk_app(pr, mvar);
expr rule = instantiate_type_univ_params(d, ls);
expr proof = mk_constant(n, ls);
std::vector<expr> emetas;
std::vector<bool> instances, explicits;
while (is_pi(rule)) {
expr mvar = tctx.mk_mvar(binding_domain(rule));
emetas.push_back(mvar);
explicits.push_back(is_explicit(binding_info(rule)));
instances.push_back(binding_info(rule).is_inst_implicit());
rule = tctx.whnf(instantiate(binding_body(rule), mvar));
proof = mk_app(proof,mvar);
}
expr rel, lhs, rhs;
if (!is_simp_relation(env, e, rel, lhs, rhs) || !is_constant(rel)) {
if (!is_simp_relation(tctx.env(), rule, rel, lhs, rhs) || !is_constant(rel)) {
throw exception(sstream() << "invalid congruence rule, '" << n
<< "' resulting type is not of the form t ~ s, where '~' is a transitive and reflexive relation");
}
@ -414,19 +417,19 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
}
buffer<expr> congr_hyps;
lean_assert(metas.size() == explicit_args.size());
for (unsigned i = 0; i < metas.size(); i++) {
expr const & mvar = metas[i];
if (explicit_args[i] && !found_mvars.contains(mlocal_name(mvar))) {
lean_assert(emetas.size() == explicits.size());
for (unsigned i = 0; i < emetas.size(); i++) {
expr const & mvar = emetas[i];
if (explicits[i] && !found_mvars.contains(mlocal_name(mvar))) {
buffer<expr> locals;
expr type = mlocal_type(mvar);
while (is_pi(type)) {
expr local = mk_local(tc.mk_fresh_name(), binding_domain(type));
expr local = tctx.mk_tmp_local(binding_domain(type));
locals.push_back(local);
type = instantiate(binding_body(type), local);
}
expr h_rel, h_lhs, h_rhs;
if (!is_simp_relation(env, type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel))
if (!is_simp_relation(tctx.env(), type, h_rel, h_lhs, h_rhs) || !is_constant(h_rel))
continue;
unsigned j = 0;
for (expr const & local : locals) {
@ -452,8 +455,8 @@ void add_congr_core(environment const & env, simp_rule_sets & s, name const & n)
congr_hyps.push_back(mvar);
}
}
congr_rule rule(n, ls, to_list(metas), lhs, rhs, pr, to_list(congr_hyps));
s.insert(const_name(rel), rule);
s.insert(const_name(rel), congr_rule(n, ls, emetas, instances, lhs, rhs, proof, to_list(congr_hyps)));
}
struct rrs_state {
@ -461,14 +464,15 @@ struct rrs_state {
name_set m_simp_names;
name_set m_congr_names;
void add_simp(environment const & env, name const & cname) {
type_checker tc(env);
m_sets = add_core(tc, m_sets, cname);
void add_simp(environment const & env, io_state const & ios, name const & cname) {
tmp_type_context tctx{env,ios};
m_sets = add_core(tctx, m_sets, cname);
m_simp_names.insert(cname);
}
void add_congr(environment const & env, name const & n) {
add_congr_core(env, m_sets, n);
void add_congr(environment const & env, io_state const & ios, name const & n) {
tmp_type_context tctx{env,ios};
add_congr_core(tctx,m_sets, n);
m_congr_names.insert(n);
}
};
@ -476,11 +480,11 @@ struct rrs_state {
struct rrs_config {
typedef pair<bool, name> entry;
typedef rrs_state state;
static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
static void add_entry(environment const & env, io_state const & ios, state & s, entry const & e) {
if (e.first)
s.add_simp(env, e.second);
s.add_simp(env, ios, e.second);
else
s.add_congr(env, e.second);
s.add_congr(env, ios, e.second);
}
static name const & get_class_name() {
return *g_class_name;
@ -522,13 +526,13 @@ simp_rule_sets get_simp_rule_sets(environment const & env) {
return rrs_ext::get_state(env).m_sets;
}
simp_rule_sets get_simp_rule_sets(environment const & env, name const & ns) {
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns) {
simp_rule_sets set;
list<pair<bool, name>> const * cnames = rrs_ext::get_entries(env, ns);
if (cnames) {
type_checker tc(env);
tmp_type_context tctx(env,ios);
for (pair<bool, name> const & p : *cnames) {
set = add_core(tc, set, p.second);
set = add_core(tctx, set, p.second);
}
}
return set;

38
src/library/simplifier/simp_rule_set.h
View file

@ -5,9 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include "kernel/type_checker.h"
#include "library/tmp_type_context.h"
#include "library/head_map.h"
#include "library/io_state_stream.h"
#include <vector>
namespace lean {
class simp_rule_sets;
@ -15,17 +16,23 @@ class simp_rule_sets;
class simp_rule_core {
protected:
name m_id;
levels m_univ_metas;
list<expr> m_metas;
levels m_umetas;
std::vector<expr> m_emetas;
std::vector<bool> m_instances;
expr m_lhs;
expr m_rhs;
expr m_proof;
simp_rule_core(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof);
simp_rule_core(name const & id, levels const & umetas, std::vector<expr> const & emetas,
std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof);
public:
name const & get_id() const { return m_id; }
levels const & get_univ_metas() const { return m_univ_metas; }
list<expr> const & get_metas() const { return m_metas; }
unsigned get_num_umeta() const { return length(m_umetas); }
unsigned get_num_emeta() const { return m_emetas.size(); }
expr const & get_emeta(unsigned i) const { return m_emetas[i]; }
bool is_instance(unsigned i) const { return m_instances[i]; }
expr const & get_lhs() const { return m_lhs; }
expr const & get_rhs() const { return m_rhs; }
expr const & get_proof() const { return m_proof; }
@ -33,9 +40,9 @@ public:
class simp_rule : public simp_rule_core {
bool m_is_permutation;
simp_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof, bool is_perm);
friend simp_rule_sets add_core(type_checker & tc, simp_rule_sets const & s, name const & id,
simp_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof, bool is_perm);
friend simp_rule_sets add_core(tmp_type_context & tctx, simp_rule_sets const & s, name const & id,
levels const & univ_metas, expr const & e, expr const & h);
public:
friend bool operator==(simp_rule const & r1, simp_rule const & r2);
@ -48,9 +55,10 @@ inline bool operator!=(simp_rule const & r1, simp_rule const & r2) { return !ope
class congr_rule : public simp_rule_core {
list<expr> m_congr_hyps;
congr_rule(name const & id, levels const & univ_metas, list<expr> const & metas,
expr const & lhs, expr const & rhs, expr const & proof, list<expr> const & congr_hyps);
friend void add_congr_core(environment const & env, simp_rule_sets & s, name const & n);
congr_rule(name const & id, levels const & umetas, std::vector<expr> const & emetas,
std::vector<bool> const & instances, expr const & lhs, expr const & rhs, expr const & proof,
list<expr> const & congr_hyps);
friend void add_congr_core(tmp_type_context & tctx, simp_rule_sets & s, name const & n);
public:
friend bool operator==(congr_rule const & r1, congr_rule const & r2);
list<expr> const & get_congr_hyps() const { return m_congr_hyps; }
@ -108,7 +116,7 @@ public:
format pp(formatter const & fmt) const;
};
simp_rule_sets add(type_checker & tc, simp_rule_sets const & s, name const & id, expr const & e, expr const & h);
simp_rule_sets add(tmp_type_context & tctx, simp_rule_sets const & s, name const & id, expr const & e, expr const & h);
simp_rule_sets join(simp_rule_sets const & s1, simp_rule_sets const & s2);
environment add_simp_rule(environment const & env, name const & n, bool persistent = true);
@ -121,7 +129,7 @@ bool is_congr_rule(environment const & env, name const & n);
/** \brief Get current simplification rule sets */
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, name const & ns);
simp_rule_sets get_simp_rule_sets(environment const & env, io_state const & ios, name const & ns);
io_state_stream const & operator<<(io_state_stream const & out, simp_rule_sets const & s);

16
tests/lean/simplifier1.lean Normal file
View file

@ -0,0 +1,16 @@
/- Basic rewriting with eq without congruence or conditionals -/
universe l
constant T : Type.{l}
constants (x y z : T) (f g h : T → T)
constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
#simplify eq 2 (f x) -- f x
attribute Hfxgy [simp]
attribute Hgyhz [simp]
set_option simplify.exhaustive false
#simplify eq 2 (f x) -- g y
set_option simplify.exhaustive true
#simplify eq 2 (f x) -- h z

3
tests/lean/simplifier1.lean.expected.out Normal file
View file

@ -0,0 +1,3 @@
<refl>
f x = g y
f x = h z

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

@ -0,0 +1,15 @@
/- Basic rewriting with eq and lambda without congruence or conditionals -/
universe l
constant T : Type.{l}
constants (x y z : T) (f g h : T → T)
constants (Hfxgy : f x = g y) (Hgyhz : g y = h z)
attribute Hfxgy [simp]
attribute Hgyhz [simp]
set_option simplify.exhaustive false
#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), g y
set_option simplify.exhaustive true
#simplify eq 0 (λ a b c : bool, f x) -- λ (a b c : bool), h z

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

@ -0,0 +1,2 @@
λ (x x x : bool), g y
λ (x x x : bool), h z

36
tests/lean/simplifier3.lean Normal file
View file

@ -0,0 +1,36 @@
/- Basic rewriting with eq and generic congruence, with no conditionals -/
namespace test_congr
universe l
constant T : Type.{l}
constants (x y z : T → T) (f g h : (T → T) → (T → T)) (a b c : T)
constants (Hfxgy : f x = g y) (Hgyhz : g y = h z) (Hab : a = b) (Hbc : b = c)
#simplify eq 2 (f x a) -- f x a
attribute Hfxgy [simp]
attribute Hgyhz [simp]
attribute Hab [simp]
attribute Hbc [simp]
set_option simplify.exhaustive false
#simplify eq 2 (f x a) -- g y b
set_option simplify.exhaustive true
#simplify eq 2 (f x a) -- h z c
end test_congr
namespace test_congr_fun
universes l1 l2
constants (T : Type.{l1}) (U : T → Type.{l2})
constants (f g : Π (x:T), U x) (x y : T)
constants (Hfg : f = g) (Hxy : x = y)
attribute Hfg [simp]
attribute Hxy [simp]
#simplify eq 2 (f x)
end test_congr_fun

4
tests/lean/simplifier3.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
<refl>
f x a = g y b
f x a = h z c
f x = g x

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

@ -0,0 +1,19 @@
/- Basic rewriting with a custom relation without congruence or conditionals -/
import logic.connectives data.nat
universe l
constant T : Type.{l}
constants (x y z : T) (f g h : T → T)
constants (R : T → T → Prop)
constants (R_refl : ∀ x, R x x) (R_sym : ∀ x y, R x y → R y x) (R_trans : ∀ x y z, R x y → R y z → R x z)
constants (Hfxgy : R (f x) (g y)) (Hgyhz : R (g y) (h z))
attribute R_refl [refl]
attribute R_sym [symm]
#simplify R 2 (f x) -- f x
attribute R_trans [trans]
#simplify R 2 (f x) -- f x
attribute Hfxgy [simp]
#simplify R 2 (f x) -- f x
attribute Hgyhz [simp]
#simplify R 2 (f x) -- f x

4
tests/lean/simplifier4.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
<refl>
<refl>
R (f x) (g y)
R (f x) (h z)

13
tests/lean/simplifier5.lean Normal file
View file

@ -0,0 +1,13 @@
/- Basic rewriting with iff with congr_iff -/
import logic.connectives
open nat
#simplify iff 2 (@le nat nat_has_le 0 0) -- true
#simplify iff 2 (@le nat nat_has_le 0 1) -- true
#simplify iff 2 (@le nat nat_has_le 0 2) -- true
#simplify iff 2 (@lt nat nat_has_lt 0 0) -- false
#simplify iff 2 (@lt nat nat_has_lt 0 (succ 0)) -- true
#simplify iff 2 (@lt nat nat_has_lt 1 (succ 1)) -- true
#simplify iff 2 (@lt nat nat_has_lt 0 (succ (succ 0))) -- true
#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 0) -- true
#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @le nat nat_has_le 0 1) -- true
#simplify iff 2 (@le nat nat_has_le 0 0 ↔ @lt nat nat_has_lt 0 0) -- false

10
tests/lean/simplifier5.lean.expected.out Normal file
View file

@ -0,0 +1,10 @@
0 ≤ 0 ↔ true
0 ≤ 1 ↔ true
0 ≤ 2 ↔ true
0 < 0 ↔ false
0 < succ 0 ↔ true
1 < succ 1 ↔ true
0 < succ (succ 0) ↔ true
0 ≤ 0 ↔ 0 ≤ 0 ↔ true
0 ≤ 0 ↔ 0 ≤ 1 ↔ true
0 ≤ 0 ↔ 0 < 0 ↔ false

25
tests/lean/simplifier6.lean Normal file
View file

@ -0,0 +1,25 @@
/- Basic pi congruence -/
import logic.connectives logic.quantifiers
namespace pi_congr1
constants (p1 q1 p2 q2 p3 q3 : Prop) (H1 : p1 ↔ q1) (H2 : p2 ↔ q2) (H3 : p3 ↔ q3)
local attribute H1 [simp]
local attribute H2 [simp]
local attribute H3 [simp]
#simplify iff 1 p1
#simplify iff 1 p1 → p2
#simplify iff 1 p1 → p2 → p3
end pi_congr1
namespace pi_congr2
universe l
constants (T : Type.{l}) (P Q : T → Prop) (H : ∀ (x : T), P x ↔ Q x)
local attribute H [simp]
constant (x : T)
#simplify iff 1 (∀ (x : T), P x)
end pi_congr2

4
tests/lean/simplifier6.lean.expected.out Normal file
View file

@ -0,0 +1,4 @@
H1
congr_imp H1 H2
congr_imp H1 (congr_imp H2 H3)
congr_forall (λ (x : T), H x)

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

@ -0,0 +1,15 @@
-- Simplifying the operator with a user-defined congruence
import logic.connectives
constants (P1 Q1 P2 Q2 P3 Q3 : Prop) (H1 : P1 ↔ Q1) (H2 : P2 ↔ Q2) (H3 : P3 ↔ Q3)
constants (f g : Prop → Prop → Prop)
constants (Hf : and = f) (Hg : f = g)
attribute H1 [simp]
attribute H2 [simp]
attribute H3 [simp]
attribute Hf [simp]
attribute Hg [simp]
#simplify iff 2 (and P1 (and P2 P3))
#simplify iff 2 (and P1 (iff P2 P3))

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

@ -0,0 +1,2 @@
P1 ∧ P2 ∧ P3 ↔ g Q1 (g Q2 Q3)
P1 ∧ (P2 ↔ P3) ↔ g Q1 (Q2 ↔ Q3)

13
tests/lean/simplifier8.lean Normal file
View file

@ -0,0 +1,13 @@
-- deeper congruence
universe l
constants (T : Type.{l}) (x1 x2 x3 x4 x5 x6 : T) (f : T → T → T)
constants (f_comm : ∀ x y, f x y = f y x)
(f_l : ∀ x y z, f (f x y) z = f x (f y z))
(f_r : ∀ x y z, f x (f y z) = f y (f x z))
attribute f_comm [simp]
attribute f_l [simp]
attribute f_r [simp]
#simplify eq 0 (f (f x2 x4) (f x5 (f x3 (f x1 x6))))

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

@ -0,0 +1 @@
f x1 (f x2 (f x3 (f x4 (f x5 x6))))