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

feat(library/blast/congruence_closure): add blast.cc.heq option

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-10 00:15:26 -08:00
parent b7be3ec6de
commit 22a6b7f1c3
6 changed files with 57 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -683,6 +683,7 @@ static environment congr_cmd_core(parser & p, congr_kind kind) {
case congr_arg_kind::Fixed: out << "fixed"; break;
case congr_arg_kind::FixedNoParam: out << "fixed-noparm"; break;
case congr_arg_kind::Eq: out << "eq"; break;
case congr_arg_kind::HEq: out << "heq"; break;
case congr_arg_kind::Cast: out << "cast"; break;
}
}
@ -716,7 +717,7 @@ static environment hcongr_cmd(parser & p) {
app_builder b(ctx);
fun_info_manager infom(ctx);
congr_lemma_manager cm(b, infom);
optional<hcongr_lemma> r = cm.mk_hcongr(e);
optional<congr_lemma> r = cm.mk_hcongr(e);
if (!r)
throw parser_error("failed to generated heterogeneous congruence lemma", pos);
auto out = p.regular_stream();

26
src/library/blast/congruence_closure.cpp
View file

@ -6,6 +6,7 @@ Author: Leonardo de Moura
*/
#include <algorithm>
#include <vector>
#include "util/sexpr/option_declarations.h"
#include "kernel/abstract.h"
#include "library/trace.h"
#include "library/constants.h"
@ -16,8 +17,18 @@ Author: Leonardo de Moura
#include "library/blast/trace.h"
#include "library/blast/options.h"
#ifndef LEAN_DEFAULT_BLAST_CC_HEQ
#define LEAN_DEFAULT_BLAST_CC_HEQ true
#endif
namespace lean {
namespace blast {
static name * g_blast_cc_heq = nullptr;
bool get_blast_cc_heq(options const & o) {
return o.get_bool(*g_blast_cc_heq, LEAN_DEFAULT_BLAST_CC_HEQ);
}
/* Not all user-defined congruence lemmas can be use by this module
We cache the ones that can be used. */
struct congr_lemma_key {
@ -258,6 +269,7 @@ static optional<ext_congr_lemma> to_ext_congr_lemma(name const & R, expr const &
}
switch (kinds[i]) {
case congr_arg_kind::FixedNoParam:
case congr_arg_kind::HEq:
// User defined congruence rules do not use FixedNoParam
lean_unreachable();
break;
@ -483,6 +495,8 @@ int congruence_closure::congr_key_cmp::operator()(congr_key const & k1, congr_ke
for (unsigned i = 0; i < args1.size(); i++) {
lean_assert(*it1); lean_assert(*it2);
switch (head(*it2)) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Eq:
lean_assert(head(*it1));
r = g_cc->compare_root(*head(*it1), args1[i], args2[i]);
@ -545,6 +559,8 @@ auto congruence_closure::mk_congr_key(ext_congr_lemma const & lemma, expr const
for (unsigned i = 0; i < args.size(); i++) {
lean_assert(*it1); lean_assert(*it2);
switch (head(*it2)) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Eq:
lean_assert(head(*it1));
h = hash(h, get_root(*head(*it1), args[i]).hash());
@ -1039,6 +1055,8 @@ expr congruence_closure::mk_congr_proof_core(name const & R, expr const & lhs, e
for (unsigned i = 0; i < lhs_args.size(); i++) {
lean_assert(*it1 && *it2);
switch (head(*it2)) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Eq:
lean_assert(head(*it1));
lemma_args.push_back(lhs_args[i]);
@ -1473,9 +1491,17 @@ void initialize_congruence_closure() {
g_congr_mark = new expr(mk_constant(name(prefix, "[congruence]")));
g_iff_true_mark = new expr(mk_constant(name(prefix, "[iff-true]")));
g_lift_mark = new expr(mk_constant(name(prefix, "[lift]")));
g_blast_cc_heq = new name{"blast", "cc", "heq"};
register_bool_option(*g_blast_cc_heq, LEAN_DEFAULT_BLAST_CC_HEQ,
"(blast) enable support for heterogeneous equality "
"and more general congruence lemmas in the congruence closure module "
"(this option is ignore in HoTT mode)");
}
void finalize_congruence_closure() {
delete g_blast_cc_heq;
delete g_congr_mark;
delete g_iff_true_mark;
delete g_lift_mark;

1
src/library/blast/congruence_closure.h
View file

@ -260,7 +260,6 @@ struct ext_congr_lemma {
ext_congr_lemma(name const & R, congr_lemma const & H, list<optional<name>> const & rel_names, bool lift_needed);
name const & get_relation() const { return m_R; }
congr_lemma const & get_congr_lemma() const { return m_congr_lemma; }
list<optional<name>> const & get_arg_rel_names() const { return m_rel_names; }
};

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

@ -285,6 +285,8 @@ optional<result> simplifier::cache_lookup(expr const & e) {
lean_assert(ckind == congr_arg_kind::Cast || new_args[i] == old_args[i], static_cast<unsigned>(ckind), new_args[i], old_args[i]);
expr rfl;
switch (ckind) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Fixed:
proof = mk_app(proof, new_args[i]);
type = instantiate(binding_body(type), new_args[i]);
@ -830,6 +832,8 @@ optional<result> simplifier::normalize_subsingleton_args(expr const & e) {
for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
expr rfl;
switch (ckind) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Fixed:
proof = mk_app(proof, args[i]);
type = instantiate(binding_body(type), args[i]);
@ -887,6 +891,8 @@ optional<result> simplifier::synth_congr(expr const & e, F && simp) {
bool has_cast = false;
for_each(congr_lemma->get_arg_kinds(), [&](congr_arg_kind const & ckind) {
switch (ckind) {
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Fixed:
proof = mk_app(proof, args[i]);
type = instantiate(binding_body(type), args[i]);

32
src/library/congr_lemma_manager.cpp
View file

@ -27,12 +27,11 @@ struct congr_lemma_manager::imp {
type_context & m_ctx;
typedef expr_unsigned key;
typedef expr_unsigned_map<result> cache;
typedef expr_unsigned_map<hresult> hcache;
cache m_simp_cache;
cache m_simp_cache_spec;
cache m_cache;
cache m_cache_spec;
hcache m_hcache;
cache m_hcache;
cache m_rel_cache[2];
relation_info_getter m_relation_info_getter;
@ -184,6 +183,8 @@ struct congr_lemma_manager::imp {
hyps.push_back(eq);
break;
}
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Fixed:
rhss.push_back(lhs);
eqs.push_back(none_expr());
@ -261,6 +262,8 @@ struct congr_lemma_manager::imp {
simp_lemma_args.push_back(eq);
break;
}
case congr_arg_kind::HEq:
lean_unreachable();
case congr_arg_kind::Fixed:
rhs = lhs;
rhss.push_back(rhs);
@ -465,7 +468,7 @@ struct congr_lemma_manager::imp {
}
}
optional<hresult> mk_hcongr_core(expr const & fn, unsigned nargs) {
optional<result> mk_hcongr_core(expr const & fn, unsigned nargs) {
try {
expr fn_type_lhs = relaxed_whnf(infer(fn));
expr fn_type_rhs = fn_type_lhs;
@ -474,11 +477,11 @@ struct congr_lemma_manager::imp {
buffer<expr> rhss;
buffer<expr> eqs;
buffer<expr> hyps; // contains lhss + rhss + eqs
buffer<hcongr_arg_kind> kinds;
buffer<congr_arg_kind> kinds;
for (unsigned i = 0; i < nargs; i++) {
if (!is_pi(fn_type_lhs)) {
trace_too_many_arguments(fn, nargs);
return optional<hresult>();
return optional<result>();
}
expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type_lhs), binding_domain(fn_type_lhs));
lhss.push_back(lhs); hyps.push_back(lhs);
@ -487,10 +490,10 @@ struct congr_lemma_manager::imp {
expr eq_type;
if (binding_domain(fn_type_lhs) == binding_domain(fn_type_rhs)) {
eq_type = m_builder.mk_eq(lhs, rhs);
kinds.push_back(hcongr_arg_kind::Eq);
kinds.push_back(congr_arg_kind::Eq);
} else {
eq_type = m_builder.mk_heq(lhs, rhs);
kinds.push_back(hcongr_arg_kind::HEq);
kinds.push_back(congr_arg_kind::HEq);
}
expr h_eq = m_ctx.mk_tmp_local(e_name.append_after(i), eq_type);
eqs.push_back(h_eq); hyps.push_back(h_eq);
@ -507,10 +510,10 @@ struct congr_lemma_manager::imp {
}
expr result_type = Pi(hyps, eq_type);
expr result_proof = mk_hcongr_proof(result_type);
return optional<hresult>(result_type, result_proof, to_list(kinds));
return optional<result>(result_type, result_proof, to_list(kinds));
} catch (app_builder_exception &) {
trace_app_builder_failure(fn);
return optional<hresult>();
return optional<result>();
}
}
@ -574,18 +577,17 @@ public:
return optional<result>(new_r);
}
optional<hresult> mk_hcongr(expr const & fn, unsigned nargs) {
optional<result> mk_hcongr(expr const & fn, unsigned nargs) {
auto r = m_hcache.find(key(fn, nargs));
if (r != m_hcache.end())
return optional<hresult>(r->second);
return optional<result>(r->second);
auto new_r = mk_hcongr_core(fn, nargs);
if (new_r)
m_hcache.insert(mk_pair(key(fn, nargs), *new_r));
return new_r;
}
optional<hresult> mk_hcongr(expr const & fn) {
optional<result> mk_hcongr(expr const & fn) {
fun_info finfo = m_fmanager.get(fn);
return mk_hcongr(fn, finfo.get_arity());
}
@ -712,10 +714,10 @@ auto congr_lemma_manager::mk_congr(expr const & fn, unsigned nargs) -> optional<
auto congr_lemma_manager::mk_specialized_congr(expr const & fn) -> optional<result> {
return m_ptr->mk_specialized_congr(fn);
}
auto congr_lemma_manager::mk_hcongr(expr const & fn) -> optional<hresult> {
auto congr_lemma_manager::mk_hcongr(expr const & fn) -> optional<result> {
return m_ptr->mk_hcongr(fn);
}
auto congr_lemma_manager::mk_hcongr(expr const & fn, unsigned nargs) -> optional<hresult> {
auto congr_lemma_manager::mk_hcongr(expr const & fn, unsigned nargs) -> optional<result> {
return m_ptr->mk_hcongr(fn, nargs);
}
auto congr_lemma_manager::mk_rel_iff_congr(expr const & R) -> optional<result> {

25
src/library/congr_lemma_manager.h
View file

@ -21,7 +21,10 @@ enum class congr_arg_kind {
Eq,
/* congr-simp lemma contains only one parameter for this kind of argument, and congr-lemmas contains two.
They correspond to arguments that are subsingletons/propositions. */
Cast
Cast,
/* The lemma contains three parameters for this kind of argument a_i, b_i and (eq_i : a_i == b_i).
a_i and b_i represent the left and right hand sides, and eq_i is a proof for their heterogeneous equality. */
HEq
};
class congr_lemma {
@ -37,20 +40,6 @@ public:
bool all_eq_kind() const;
};
enum class hcongr_arg_kind { Eq, HEq };
class hcongr_lemma {
expr m_type;
expr m_proof;
list<hcongr_arg_kind> m_arg_kinds;
public:
hcongr_lemma(expr const & type, expr const & proof, list<hcongr_arg_kind> const & ks):
m_type(type), m_proof(proof), m_arg_kinds(ks) {}
expr const & get_type() const { return m_type; }
expr const & get_proof() const { return m_proof; }
list<hcongr_arg_kind> const & get_arg_kinds() const { return m_arg_kinds; }
};
class congr_lemma_manager {
struct imp;
std::unique_ptr<imp> m_ptr;
@ -58,7 +47,6 @@ public:
congr_lemma_manager(app_builder & b, fun_info_manager & fm);
~congr_lemma_manager();
typedef congr_lemma result;
typedef hcongr_lemma hresult;
type_context & ctx();
unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs);
@ -73,8 +61,8 @@ public:
/* Create a specialized theorem using (a prefix of) the arguments of the given application. */
optional<result> mk_specialized_congr(expr const & a);
optional<hresult> mk_hcongr(expr const & fn);
optional<hresult> mk_hcongr(expr const & fn, unsigned nargs);
optional<result> mk_hcongr(expr const & fn);
optional<result> mk_hcongr(expr const & fn, unsigned nargs);
/** \brief If R is an equivalence relation, construct the congruence lemma
@ -87,7 +75,6 @@ public:
R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */
optional<result> mk_rel_eq_congr(expr const & R);
};
void initialize_congr_lemma_manager();
void finalize_congr_lemma_manager();
}