max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor(library): port congr_lemma_manager to new type_context

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-22 18:05:00 -07:00
parent 9327d85f6c
commit b2c3352a80
3 changed files with 195 additions and 203 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/CMakeLists.txt
View file

@ -11,9 +11,9 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
aux_recursors.cpp norm_num.cpp trace.cpp
attribute_manager.cpp error_handling.cpp unification_hint.cpp
attribute_manager.cpp error_handling.cpp unification_hint.cpp
local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp lazy_abstraction.cpp
fun_info.cpp
fun_info.cpp congr_lemma.cpp
# Legacy -- The following files will be eventually deleted
normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp
@ -21,6 +21,6 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp
tmp_type_context.cpp
# fun_info_manager.cpp congr_lemma_manager.cpp abstract_expr_manager.cpp light_lt_manager.cpp
# abstract_expr_manager.cpp light_lt_manager.cpp
# proof_irrel_expr_manager.cpp
)

338
src/library/congr_lemma_manager.cpp → src/library/congr_lemma.cpp
View file

@ -1,5 +1,5 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
@ -8,12 +8,14 @@ Author: Leonardo de Moura
#include "kernel/abstract.h"
#include "library/util.h"
#include "library/trace.h"
#include "library/locals.h"
#include "library/constants.h"
#include "library/replace_visitor.h"
#include "library/relation_manager.h"
#include "library/locals.h"
#include "library/congr_lemma.h"
#include "library/expr_unsigned_map.h"
#include "library/congr_lemma_manager.h"
#include "library/relation_manager.h"
#include "library/cache_helper.h"
#include "library/app_builder.h"
#include "library/fun_info.h"
namespace lean {
bool congr_lemma::all_eq_kind() const {
@ -21,12 +23,9 @@ bool congr_lemma::all_eq_kind() const {
[](congr_arg_kind k) { return k == congr_arg_kind::Eq; });
}
struct congr_lemma_manager::imp {
app_builder & m_builder;
fun_info_manager & m_fmanager;
old_type_context & m_ctx;
typedef expr_unsigned key;
typedef expr_unsigned_map<result> cache;
struct congr_lemma_cache {
typedef expr_unsigned_map<congr_lemma> cache;
environment m_env;
cache m_simp_cache;
cache m_simp_cache_spec;
cache m_cache;
@ -34,6 +33,28 @@ struct congr_lemma_manager::imp {
cache m_hcache;
cache m_rel_cache[2];
relation_info_getter m_relation_info_getter;
congr_lemma_cache(environment const & env):
m_env(env),
m_relation_info_getter(mk_relation_info_getter(env)) {}
environment const & env() const { return m_env; }
};
typedef cache_compatibility_helper<congr_lemma_cache> congr_lemma_cache_helper;
MK_THREAD_LOCAL_GET_DEF(congr_lemma_cache_helper, get_clch);
congr_lemma_cache & get_congr_lemma_cache_for(type_context const & ctx) {
return get_clch().get_cache_for(ctx);
}
struct congr_lemma_manager {
typedef expr_unsigned key;
typedef congr_lemma result;
type_context & m_ctx;
congr_lemma_cache & m_cache;
congr_lemma_manager(type_context & ctx):
m_ctx(ctx), m_cache(get_congr_lemma_cache_for(ctx)) {}
expr infer(expr const & e) { return m_ctx.infer(e); }
expr whnf(expr const & e) { return m_ctx.whnf(e); }
@ -61,24 +82,24 @@ struct congr_lemma_manager::imp {
// Since the type depends on the major, we must use dependent elimination.
// and the motive just abstract rhs and *major
use_drec = true;
motive = Fun(rhs, Fun(*major, type));
motive = m_ctx.mk_lambda({rhs, *major}, type);
// We compute new_type by replacing rhs with lhs and *major with eq.refl(lhs) in type.
new_type = instantiate(abstract_local(type, rhs), lhs);
expr refl = m_builder.mk_eq_refl(lhs);
expr refl = mk_eq_refl(m_ctx, lhs);
new_type = instantiate(abstract_local(new_type, *major), refl);
} else {
// type does not depend on the *major.
// So, the motive is just (fun rhs, type), and
// new_type just replaces rhs with lhs.
use_drec = false;
motive = Fun(rhs, type);
motive = m_ctx.mk_lambda({rhs}, type);
new_type = instantiate(abstract_local(type, rhs), lhs);
}
expr minor = cast(e, new_type, tail(deps), eqs);
if (use_drec) {
return m_builder.mk_eq_drec(motive, minor, *major);
return mk_eq_drec(m_ctx, motive, minor, *major);
} else {
return m_builder.mk_eq_rec(motive, minor, *major);
return mk_eq_rec(m_ctx, motive, minor, *major);
}
}
}
@ -99,17 +120,17 @@ struct congr_lemma_manager::imp {
}
expr g = mk_app(fn, i, lhss.data());
if (i == kinds.size())
return m_builder.mk_eq_refl(g);
return mk_eq_refl(m_ctx, g);
lean_assert(kinds[i] == congr_arg_kind::Eq);
lean_assert(eqs[i]);
expr pr = m_builder.mk_congr_arg(g, *eqs[i]);
expr pr = mk_congr_arg(m_ctx, g, *eqs[i]);
i++;
for (; i < kinds.size(); i++) {
if (kinds[i] == congr_arg_kind::Eq) {
pr = m_builder.mk_congr(pr, *eqs[i]);
pr = ::lean::mk_congr(m_ctx, pr, *eqs[i]);
} else {
lean_assert(kinds[i] == congr_arg_kind::Fixed);
pr = m_builder.mk_congr_fun(pr, lhss[i]);
pr = mk_congr_fun(m_ctx, pr, lhss[i]);
}
}
return pr;
@ -120,7 +141,7 @@ struct congr_lemma_manager::imp {
\remark This is an auxiliary method used by mk_congr_simp. */
expr mk_congr_proof(unsigned i, expr const & lhs, expr const & rhs, buffer<optional<expr>> const & eqs) {
if (i == eqs.size()) {
return m_builder.mk_eq_refl(rhs);
return mk_eq_refl(m_ctx, rhs);
} else if (!eqs[i]) {
return mk_congr_proof(i+1, lhs, rhs, eqs);
} else {
@ -129,14 +150,14 @@ struct congr_lemma_manager::imp {
lean_verify(is_eq(mlocal_type(major), x_1, x_2));
lean_assert(is_local(x_1));
lean_assert(is_local(x_2));
expr motive_eq = m_builder.mk_eq(lhs, rhs);
expr motive = Fun(x_2, Fun(major, motive_eq));
expr motive_eq = mk_eq(m_ctx, lhs, rhs);
expr motive = m_ctx.mk_lambda({x_2, major}, motive_eq);
// We compute the new_rhs by replacing x_2 with x_1 and major with (eq.refl x_1) in rhs.
expr new_rhs = instantiate(abstract_local(rhs, x_2), x_1);
expr x1_refl = m_builder.mk_eq_refl(x_1);
expr x1_refl = mk_eq_refl(m_ctx, x_1);
new_rhs = instantiate(abstract_local(new_rhs, major), x1_refl);
expr minor = mk_congr_proof(i+1, lhs, new_rhs, eqs);
return m_builder.mk_eq_drec(motive, minor, major);
return mk_eq_drec(m_ctx, motive, minor, major);
}
}
@ -158,6 +179,7 @@ struct congr_lemma_manager::imp {
how the resulting term looks like. */
optional<result> mk_congr_simp(expr const & fn, buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
try {
type_context::tmp_locals locals(m_ctx);
expr fn_type = relaxed_whnf(infer(fn));
name e_name("e");
buffer<expr> lhss;
@ -169,15 +191,15 @@ struct congr_lemma_manager::imp {
trace_too_many_arguments(fn, pinfos.size());
return optional<result>();
}
expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
expr lhs = locals.push_local_from_binding(fn_type);
lhss.push_back(lhs);
hyps.push_back(lhs);
switch (kinds[i]) {
case congr_arg_kind::Eq: {
expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(fn_type));
expr eq_type = m_builder.mk_eq(lhs, rhs);
expr rhs = locals.push_local_from_binding(fn_type);
expr eq_type = mk_eq(m_ctx, lhs, rhs);
rhss.push_back(rhs);
expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type);
expr eq = locals.push_local(e_name.append_after(eqs.size()+1), eq_type);
eqs.push_back(some_expr(eq));
hyps.push_back(rhs);
hyps.push_back(eq);
@ -193,9 +215,10 @@ struct congr_lemma_manager::imp {
lean_unreachable(); // TODO(Leo): not implemented yet
break;
case congr_arg_kind::Cast: {
expr rhs_type = mlocal_type(lhs);
rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()), rhss.size(), rhss.data());
expr rhs = cast(lhs, rhs_type, pinfos[i].get_dependencies(), eqs);
expr rhs_type = m_ctx.infer(lhs);
rhs_type = instantiate_rev(abstract_locals(rhs_type, lhss.size()-1, lhss.data()),
rhss.size(), rhss.data());
expr rhs = cast(lhs, rhs_type, pinfos[i].get_back_deps(), eqs);
rhss.push_back(rhs);
eqs.push_back(none_expr());
break;
@ -204,15 +227,15 @@ struct congr_lemma_manager::imp {
}
expr lhs = mk_app(fn, lhss);
expr rhs = mk_app(fn, rhss);
expr eq = m_builder.mk_eq(lhs, rhs);
expr congr_type = Pi(hyps, eq);
expr eq = mk_eq(m_ctx, lhs, rhs);
expr congr_type = m_ctx.mk_pi(hyps, eq);
expr congr_proof;
if (has_cast(kinds)) {
congr_proof = mk_congr_proof(0, lhs, rhs, eqs);
} else {
congr_proof = mk_simple_congr_proof(fn, lhss, eqs, kinds);
}
congr_proof = Fun(hyps, congr_proof);
congr_proof = m_ctx.mk_lambda(hyps, congr_proof);
return optional<result>(congr_type, congr_proof, to_list(kinds));
} catch (app_builder_exception &) {
trace_app_builder_failure(fn);
@ -230,6 +253,7 @@ struct congr_lemma_manager::imp {
optional<result> mk_congr(expr const & fn, optional<result> const & simp_lemma,
buffer<param_info> const & pinfos, buffer<congr_arg_kind> const & kinds) {
try {
type_context::tmp_locals locals(m_ctx);
expr fn_type1 = whnf(infer(fn));
expr fn_type2 = fn_type1;
name e_name("e");
@ -243,7 +267,7 @@ struct congr_lemma_manager::imp {
trace_too_many_arguments(fn, pinfos.size());
return optional<result>();
}
expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type1), binding_domain(fn_type1));
expr lhs = locals.push_local_from_binding(fn_type1);
expr rhs;
lhss.push_back(lhs);
hyps.push_back(lhs);
@ -251,10 +275,10 @@ struct congr_lemma_manager::imp {
switch (kinds[i]) {
case congr_arg_kind::Eq: {
lean_assert(m_ctx.is_def_eq(binding_domain(fn_type1), binding_domain(fn_type2)));
rhs = m_ctx.mk_tmp_local(binding_name(fn_type2), binding_domain(fn_type2));
expr eq_type = m_builder.mk_eq(lhs, rhs);
rhs = locals.push_local_from_binding(fn_type2);
expr eq_type = mk_eq(m_ctx, lhs, rhs);
rhss.push_back(rhs);
expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type);
expr eq = locals.push_local(e_name.append_after(eqs.size()+1), eq_type);
eqs.push_back(some_expr(eq));
hyps.push_back(rhs);
hyps.push_back(eq);
@ -273,7 +297,7 @@ struct congr_lemma_manager::imp {
lean_unreachable(); // TODO(Leo): not implemented yet
break;
case congr_arg_kind::Cast: {
rhs = m_ctx.mk_tmp_local(binding_name(fn_type2), binding_domain(fn_type2));
rhs = locals.push_local_from_binding(fn_type2);
rhss.push_back(rhs);
eqs.push_back(none_expr());
hyps.push_back(rhs);
@ -291,8 +315,8 @@ struct congr_lemma_manager::imp {
lean_verify(is_eq(type1, lhs1, rhs1));
// build proof2
expr rhs2 = mk_app(fn, rhss);
expr eq = m_builder.mk_eq(lhs1, rhs2);
expr congr_type = Pi(hyps, eq);
expr eq = mk_eq(m_ctx, lhs1, rhs2);
expr congr_type = m_ctx.mk_pi(hyps, eq);
// build proof that rhs1 = rhs2
unsigned i;
for (i = 0; i < kinds.size(); i++) {
@ -301,26 +325,26 @@ struct congr_lemma_manager::imp {
}
if (i == kinds.size()) {
// rhs1 and rhs2 are definitionally equal
expr congr_proof = Fun(hyps, pr1);
expr congr_proof = m_ctx.mk_lambda(hyps, pr1);
return optional<result>(congr_type, congr_proof, to_list(kinds));
}
buffer<expr> rhss1;
get_app_args_at_most(rhs1, rhss.size(), rhss1);
lean_assert(rhss.size() == rhss1.size());
expr a = mk_app(fn, i, rhss1.data());
expr pr2 = m_builder.mk_eq_refl(a);
expr pr2 = mk_eq_refl(m_ctx, a);
for (; i < kinds.size(); i++) {
if (kinds[i] == congr_arg_kind::Cast && !pinfos[i].is_prop()) {
lean_assert(pinfos[i].is_subsingleton());
expr r1 = rhss1[i];
expr r2 = rhss[i];
expr r1_eq_r2 = m_builder.mk_app(get_subsingleton_elim_name(), r1, r2);
pr2 = m_builder.mk_congr(pr2, r1_eq_r2);
expr r1_eq_r2 = mk_app(m_ctx, get_subsingleton_elim_name(), r1, r2);
pr2 = ::lean::mk_congr(m_ctx, pr2, r1_eq_r2);
} else {
pr2 = m_builder.mk_congr_fun(pr2, rhss[i]);
pr2 = mk_congr_fun(m_ctx, pr2, rhss[i]);
}
}
expr congr_proof = Fun(hyps, m_builder.mk_eq_trans(pr1, pr2));
expr congr_proof = m_ctx.mk_lambda(hyps, mk_eq_trans(m_ctx, pr1, pr2));
return optional<result>(congr_type, congr_proof, to_list(kinds));
} catch (app_builder_exception &) {
trace_app_builder_failure(fn);
@ -329,10 +353,10 @@ struct congr_lemma_manager::imp {
}
optional<result> mk_congr_simp(expr const & fn, unsigned nargs, fun_info const & finfo) {
auto r = m_simp_cache.find(key(fn, nargs));
if (r != m_simp_cache.end())
auto r = m_cache.m_simp_cache.find(key(fn, nargs));
if (r != m_cache.m_simp_cache.end())
return optional<result>(r->second);
list<unsigned> const & result_deps = finfo.get_result_dependencies();
list<unsigned> const & result_deps = finfo.get_result_deps();
buffer<congr_arg_kind> kinds;
buffer<param_info> pinfos;
to_buffer(finfo.get_params_info(), pinfos);
@ -342,7 +366,7 @@ struct congr_lemma_manager::imp {
kinds[i] = congr_arg_kind::Fixed;
} else if (pinfos[i].is_subsingleton()) {
// See comment at mk_congr.
if (!pinfos[i].is_prop() && pinfos[i].is_dep())
if (!pinfos[i].is_prop() && pinfos[i].has_fwd_deps())
kinds[i] = congr_arg_kind::Fixed;
else
kinds[i] = congr_arg_kind::Cast;
@ -353,7 +377,7 @@ struct congr_lemma_manager::imp {
}
for (unsigned i = 0; i < pinfos.size(); i++) {
for (unsigned j = i+1; j < pinfos.size(); j++) {
auto j_deps = pinfos[j].get_dependencies();
auto j_deps = pinfos[j].get_back_deps();
if (std::find(j_deps.begin(), j_deps.end(), i) != j_deps.end() &&
kinds[j] == congr_arg_kind::Eq) {
// We must fix i because there is a j that depends on i,
@ -365,7 +389,7 @@ struct congr_lemma_manager::imp {
}
auto new_r = mk_congr_simp(fn, pinfos, kinds);
if (new_r) {
m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r));
m_cache.m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r));
return new_r;
} else if (has_cast(kinds)) {
// remove casts and try again
@ -375,7 +399,7 @@ struct congr_lemma_manager::imp {
}
auto new_r = mk_congr_simp(fn, pinfos, kinds);
if (new_r) {
m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r));
m_cache.m_simp_cache.insert(mk_pair(key(fn, nargs), *new_r));
return new_r;
} else {
return new_r;
@ -385,9 +409,14 @@ struct congr_lemma_manager::imp {
}
}
optional<result> mk_congr_simp(expr const & fn, unsigned nargs) {
fun_info finfo = get_fun_info(m_ctx, fn, nargs);
return mk_congr_simp(fn, nargs, finfo);
}
optional<result> mk_congr(expr const & fn, unsigned nargs, fun_info const & finfo) {
auto r = m_cache.find(key(fn, nargs));
if (r != m_cache.end())
auto r = m_cache.m_cache.find(key(fn, nargs));
if (r != m_cache.m_cache.end())
return optional<result>(r->second);
optional<result> simp_lemma = mk_congr_simp(fn, nargs);
if (!simp_lemma)
@ -404,24 +433,24 @@ struct congr_lemma_manager::imp {
lean_assert(kinds.size() == pinfos.size());
bool has_cast = false;
for (unsigned i = 0; i < kinds.size(); i++) {
if (!pinfos[i].is_prop() && pinfos[i].is_subsingleton() && pinfos[i].is_dep()) {
if (!pinfos[i].is_prop() && pinfos[i].is_subsingleton() && pinfos[i].has_fwd_deps()) {
kinds[i] = congr_arg_kind::Fixed;
}
if (kinds[i] == congr_arg_kind::Cast)
has_cast = true;
}
if (!has_cast) {
m_cache.insert(mk_pair(key(fn, nargs), *simp_lemma));
m_cache.m_cache.insert(mk_pair(key(fn, nargs), *simp_lemma));
return simp_lemma; // simp_lemma will be identical to regular congr lemma
}
auto new_r = mk_congr(fn, simp_lemma, pinfos, kinds);
if (new_r)
m_cache.insert(mk_pair(key(fn, nargs), *new_r));
m_cache.m_cache.insert(mk_pair(key(fn, nargs), *new_r));
return new_r;
}
void pre_specialize(expr const & a, expr & g, unsigned & prefix_sz, unsigned & num_rest_args) {
fun_info finfo = m_fmanager.get_specialized(a);
fun_info finfo = get_specialized_fun_info(m_ctx, a);
prefix_sz = 0;
for (param_info const & pinfo : finfo.get_params_info()) {
if (!pinfo.specialized())
@ -445,31 +474,33 @@ struct congr_lemma_manager::imp {
expr mk_hcongr_proof(expr type) {
expr A, B, a, b;
if (is_eq(type, a, b)) {
return m_builder.mk_eq_refl(a);
return mk_eq_refl(m_ctx, a);
} else if (is_heq(type, A, a, B, b)) {
return m_builder.mk_heq_refl(a);
return mk_heq_refl(m_ctx, a);
} else {
type_context::tmp_locals locals(m_ctx);
lean_assert(is_pi(type) && is_pi(binding_body(type)) && is_pi(binding_body(binding_body(type))));
expr a = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type));
expr a = locals.push_local_from_binding(type);
type = instantiate(binding_body(type), a);
expr b = m_ctx.mk_tmp_local(binding_name(type), binding_domain(type));
expr b = locals.push_local_from_binding(type);
expr motive = instantiate(binding_body(type), b);
type = instantiate(binding_body(type), a);
expr eq_pr = m_ctx.mk_tmp_local(binding_name(motive), binding_domain(motive));
expr eq_pr = locals.push_local_from_binding(motive);
type = binding_body(type);
motive = binding_body(motive);
lean_assert(closed(type) && closed(motive));
expr minor = mk_hcongr_proof(type);
expr major = eq_pr;
if (is_heq(mlocal_type(eq_pr)))
major = m_builder.mk_eq_of_heq(eq_pr);
major = mk_eq_of_heq(m_ctx, eq_pr);
motive = Fun(b, motive);
return Fun({a, b, eq_pr}, m_builder.mk_eq_rec(motive, minor, major));
return m_ctx.mk_lambda({a, b, eq_pr}, mk_eq_rec(m_ctx, motive, minor, major));
}
}
optional<result> mk_hcongr_core(expr const & fn, unsigned nargs) {
try {
type_context::tmp_locals locals(m_ctx);
expr fn_type_lhs = relaxed_whnf(infer(fn));
expr fn_type_rhs = fn_type_lhs;
name e_name("e");
@ -483,19 +514,19 @@ struct congr_lemma_manager::imp {
trace_too_many_arguments(fn, nargs);
return optional<result>();
}
expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type_lhs), binding_domain(fn_type_lhs));
expr lhs = locals.push_local_from_binding(fn_type_lhs);
lhss.push_back(lhs); hyps.push_back(lhs);
expr rhs = m_ctx.mk_tmp_local(binding_name(fn_type_rhs).append_after("'"), binding_domain(fn_type_rhs));
expr rhs = locals.push_local(binding_name(fn_type_rhs).append_after("'"), binding_domain(fn_type_rhs));
rhss.push_back(rhs); hyps.push_back(rhs);
expr eq_type;
if (binding_domain(fn_type_lhs) == binding_domain(fn_type_rhs)) {
eq_type = m_builder.mk_eq(lhs, rhs);
eq_type = mk_eq(m_ctx, lhs, rhs);
kinds.push_back(congr_arg_kind::Eq);
} else {
eq_type = m_builder.mk_heq(lhs, rhs);
eq_type = mk_heq(m_ctx, lhs, rhs);
kinds.push_back(congr_arg_kind::HEq);
}
expr h_eq = m_ctx.mk_tmp_local(e_name.append_after(i), eq_type);
expr h_eq = locals.push_local(e_name.append_after(i), eq_type);
eqs.push_back(h_eq); hyps.push_back(h_eq);
fn_type_lhs = relaxed_whnf(instantiate(binding_body(fn_type_lhs), lhs));
fn_type_rhs = relaxed_whnf(instantiate(binding_body(fn_type_rhs), rhs));
@ -504,11 +535,11 @@ struct congr_lemma_manager::imp {
expr rhs = mk_app(fn, rhss);
expr eq_type;
if (fn_type_lhs == fn_type_rhs) {
eq_type = m_builder.mk_eq(lhs, rhs);
eq_type = mk_eq(m_ctx, lhs, rhs);
} else {
eq_type = m_builder.mk_heq(lhs, rhs);
eq_type = mk_heq(m_ctx, lhs, rhs);
}
expr result_type = Pi(hyps, eq_type);
expr result_type = m_ctx.mk_pi(hyps, eq_type);
expr result_proof = mk_hcongr_proof(result_type);
return optional<result>(result_type, result_proof, to_list(kinds));
} catch (app_builder_exception &) {
@ -517,20 +548,8 @@ struct congr_lemma_manager::imp {
}
}
public:
imp(app_builder & b, fun_info_manager & fm):
m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()),
m_relation_info_getter(mk_relation_info_getter(fm.ctx().env())) {}
old_type_context & ctx() { return m_ctx; }
optional<result> mk_congr_simp(expr const & fn, unsigned nargs) {
fun_info finfo = m_fmanager.get(fn, nargs);
return mk_congr_simp(fn, nargs, finfo);
}
optional<result> mk_congr_simp(expr const & fn) {
fun_info finfo = m_fmanager.get(fn);
fun_info finfo = get_fun_info(m_ctx, fn);
return mk_congr_simp(fn, finfo.get_arity(), finfo);
}
@ -539,24 +558,24 @@ public:
expr g; unsigned prefix_sz, num_rest_args;
pre_specialize(a, g, prefix_sz, num_rest_args);
key k(g, num_rest_args);
auto it = m_simp_cache_spec.find(k);
if (it != m_simp_cache_spec.end())
auto it = m_cache.m_simp_cache_spec.find(k);
if (it != m_cache.m_simp_cache_spec.end())
return optional<result>(it->second);
auto r = mk_congr_simp(g, num_rest_args);
if (!r)
return optional<result>();
result new_r = mk_specialize_result(*r, prefix_sz);
m_simp_cache_spec.insert(mk_pair(k, new_r));
m_cache.m_simp_cache_spec.insert(mk_pair(k, new_r));
return optional<result>(new_r);
}
optional<result> mk_congr(expr const & fn, unsigned nargs) {
fun_info finfo = m_fmanager.get(fn, nargs);
fun_info finfo = get_fun_info(m_ctx, fn, nargs);
return mk_congr(fn, nargs, finfo);
}
optional<result> mk_congr(expr const & fn) {
fun_info finfo = m_fmanager.get(fn);
fun_info finfo = get_fun_info(m_ctx, fn);
return mk_congr(fn, finfo.get_arity(), finfo);
}
@ -565,30 +584,30 @@ public:
expr g; unsigned prefix_sz, num_rest_args;
pre_specialize(a, g, prefix_sz, num_rest_args);
key k(g, num_rest_args);
auto it = m_cache_spec.find(k);
if (it != m_cache_spec.end())
auto it = m_cache.m_cache_spec.find(k);
if (it != m_cache.m_cache_spec.end())
return optional<result>(it->second);
auto r = mk_congr(g, num_rest_args);
if (!r) {
return optional<result>();
}
result new_r = mk_specialize_result(*r, prefix_sz);
m_cache_spec.insert(mk_pair(k, new_r));
m_cache.m_cache_spec.insert(mk_pair(k, new_r));
return optional<result>(new_r);
}
optional<result> mk_hcongr(expr const & fn, unsigned nargs) {
auto r = m_hcache.find(key(fn, nargs));
if (r != m_hcache.end())
auto r = m_cache.m_hcache.find(key(fn, nargs));
if (r != m_cache.m_hcache.end())
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));
m_cache.m_hcache.insert(mk_pair(key(fn, nargs), *new_r));
return new_r;
}
optional<result> mk_hcongr(expr const & fn) {
fun_info finfo = m_fmanager.get(fn);
fun_info finfo = get_fun_info(m_ctx, fn);
return mk_hcongr(fn, finfo.get_arity());
}
@ -606,14 +625,15 @@ public:
if (!is_constant(R))
return optional<result>();
name const & R_name = const_name(R);
auto info = m_relation_info_getter(R_name);
auto info = m_cache.m_relation_info_getter(R_name);
if (!info)
return optional<result>();
unsigned arity = info->get_arity();
key k(R, arity);
auto r = m_rel_cache[is_iff].find(k);
if (r != m_rel_cache[is_iff].end())
auto r = m_cache.m_rel_cache[is_iff].find(k);
if (r != m_cache.m_rel_cache[is_iff].end())
return optional<result>(r->second);
type_context::tmp_locals locals(m_ctx);
buffer<expr> hyps;
buffer<congr_arg_kind> kinds;
expr a1, b1, a2, b2;
@ -623,19 +643,19 @@ public:
R_type = relaxed_whnf(R_type);
if (!is_pi(R_type))
return optional<result>();
expr h = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type));
expr h = locals.push_local_from_binding(R_type);
if (i == info->get_lhs_pos()) {
a1 = h;
a2 = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type));
H1 = m_ctx.mk_tmp_local("H1", m_builder.mk_rel(R_name, a1, a2));
a2 = locals.push_local_from_binding(R_type);
H1 = locals.push_local("H1", mk_rel(m_ctx, R_name, a1, a2));
hyps.push_back(a1);
hyps.push_back(a2);
hyps.push_back(H1);
kinds.push_back(congr_arg_kind::Eq);
} else if (i == info->get_rhs_pos()) {
b1 = h;
b2 = m_ctx.mk_tmp_local(binding_name(R_type), binding_domain(R_type));
H2 = m_ctx.mk_tmp_local("H2", m_builder.mk_rel(R_name, b1, b2));
b2 = locals.push_local_from_binding(R_type);
H2 = locals.push_local("H2", mk_rel(m_ctx, R_name, b1, b2));
hyps.push_back(b1);
hyps.push_back(b2);
hyps.push_back(H2);
@ -646,27 +666,29 @@ public:
}
R_type = instantiate(binding_body(R_type), h);
}
expr lhs = m_builder.mk_rel(R_name, a1, b1);
expr rhs = m_builder.mk_rel(R_name, a2, b2);
expr lhs = mk_rel(m_ctx, R_name, a1, b1);
expr rhs = mk_rel(m_ctx, R_name, a2, b2);
// (H1 : R a1 a2) -> (H2 : R b1 b2) -> (R a1 b1 <-> R a2 b2)
expr type = is_iff ? m_builder.mk_iff(lhs, rhs) : m_builder.mk_eq(lhs, rhs);
type = Pi(hyps, type);
expr type = is_iff ? mk_iff(m_ctx, lhs, rhs) : mk_eq(m_ctx, lhs, rhs);
type = m_ctx.mk_pi(hyps, type);
/* Proof:
iff.intro
(λ H : R a1 b1, trans (symm H1) (trans H H2))
(λ H : R a2 b2, trans H1 (trans H (symm H2)))
*/
expr H;
H = m_ctx.mk_tmp_local(lhs);
expr p1 = Fun(H, m_builder.mk_trans(R_name, m_builder.mk_symm(R_name, H1), m_builder.mk_trans(R_name, H, H2)));
H = m_ctx.mk_tmp_local(rhs);
expr p2 = Fun(H, m_builder.mk_trans(R_name, H1, m_builder.mk_trans(R_name, H, m_builder.mk_symm(R_name, H2))));
expr pr = m_builder.mk_app(get_iff_intro_name(), p1, p2);
H = locals.push_local("lhs", lhs);
expr p1 = m_ctx.mk_lambda({H}, mk_trans(m_ctx, R_name, mk_symm(m_ctx, R_name, H1),
mk_trans(m_ctx, R_name, H, H2)));
H = locals.push_local("rhs", rhs);
expr p2 = m_ctx.mk_lambda({H}, mk_trans(m_ctx, R_name, H1, mk_trans(m_ctx, R_name, H,
mk_symm(m_ctx, R_name, H2))));
expr pr = mk_app(m_ctx, get_iff_intro_name(), p1, p2);
if (!is_iff)
pr = m_builder.mk_app(get_propext_name(), pr);
pr = Fun(hyps, pr);
pr = mk_app(m_ctx, get_propext_name(), pr);
pr = m_ctx.mk_lambda(hyps, pr);
result res(type, pr, to_list(kinds));
m_rel_cache[is_iff].insert(mk_pair(k, res));
m_cache.m_rel_cache[is_iff].insert(mk_pair(k, res));
return optional<result>(res);
} catch (app_builder_exception &) {
trace_app_builder_failure(R);
@ -681,59 +703,45 @@ public:
optional<result> mk_rel_eq_congr(expr const & R) {
return mk_rel_congr(R, false);
}
unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs) {
return m_fmanager.get_specialization_prefix_size(fn, nargs);
}
};
congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm):
m_ptr(new imp(b, fm)) {
optional<congr_lemma> mk_congr_simp(type_context & ctx, expr const & fn) {
return congr_lemma_manager(ctx).mk_congr_simp(fn);
}
congr_lemma_manager::~congr_lemma_manager() {
optional<congr_lemma> mk_congr_simp(type_context & ctx, expr const & fn, unsigned nargs) {
return congr_lemma_manager(ctx).mk_congr_simp(fn, nargs);
}
old_type_context & congr_lemma_manager::ctx() { return m_ptr->ctx(); }
auto congr_lemma_manager::mk_congr_simp(expr const & fn) -> optional<result> {
return m_ptr->mk_congr_simp(fn);
}
auto congr_lemma_manager::mk_congr_simp(expr const & fn, unsigned nargs) -> optional<result> {
return m_ptr->mk_congr_simp(fn, nargs);
}
auto congr_lemma_manager::mk_specialized_congr_simp(expr const & a) -> optional<result> {
return m_ptr->mk_specialized_congr_simp(a);
}
auto congr_lemma_manager::mk_congr(expr const & fn) -> optional<result> {
return m_ptr->mk_congr(fn);
}
auto congr_lemma_manager::mk_congr(expr const & fn, unsigned nargs) -> optional<result> {
return m_ptr->mk_congr(fn, nargs);
}
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<result> {
return m_ptr->mk_hcongr(fn);
}
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> {
return m_ptr->mk_rel_iff_congr(R);
}
auto congr_lemma_manager::mk_rel_eq_congr(expr const & R) -> optional<result> {
return m_ptr->mk_rel_eq_congr(R);
}
unsigned congr_lemma_manager::get_specialization_prefix_size(expr const & fn, unsigned nargs) {
return m_ptr->get_specialization_prefix_size(fn, nargs);
optional<congr_lemma> mk_specialized_congr_simp(type_context & ctx, expr const & a) {
return congr_lemma_manager(ctx).mk_specialized_congr_simp(a);
}
void initialize_congr_lemma_manager() {
register_trace_class("congruence_manager");
optional<congr_lemma> mk_congr(type_context & ctx, expr const & fn) {
return congr_lemma_manager(ctx).mk_congr(fn);
}
void finalize_congr_lemma_manager() {
optional<congr_lemma> mk_congr(type_context & ctx, expr const & fn, unsigned nargs) {
return congr_lemma_manager(ctx).mk_congr(fn, nargs);
}
optional<congr_lemma> mk_specialized_congr(type_context & ctx, expr const & a) {
return congr_lemma_manager(ctx).mk_specialized_congr(a);
}
optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn) {
return congr_lemma_manager(ctx).mk_hcongr(fn);
}
optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn, unsigned nargs) {
return congr_lemma_manager(ctx).mk_hcongr(fn, nargs);
}
optional<congr_lemma> mk_rel_iff_congr(type_context & ctx, expr const & R) {
return congr_lemma_manager(ctx).mk_rel_iff_congr(R);
}
optional<congr_lemma> mk_rel_eq_congr(type_context & ctx, expr const & R) {
return congr_lemma_manager(ctx).mk_rel_eq_congr(R);
}
}

54
src/library/congr_lemma_manager.h → src/library/congr_lemma.h
View file

@ -1,13 +1,11 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#pragma once
#include <memory>
#include "library/app_builder.h"
#include "library/fun_info_manager.h"
#include "library/type_context.h"
namespace lean {
enum class congr_arg_kind {
@ -40,41 +38,27 @@ public:
bool all_eq_kind() const;
};
class congr_lemma_manager {
struct imp;
std::unique_ptr<imp> m_ptr;
public:
congr_lemma_manager(app_builder & b, fun_info_manager & fm);
~congr_lemma_manager();
typedef congr_lemma result;
optional<congr_lemma> mk_congr_simp(type_context & ctx, expr const & fn);
optional<congr_lemma> mk_congr_simp(type_context & ctx, expr const & fn, unsigned nargs);
/* Create a specialized theorem using (a prefix of) the arguments of the given application. */
optional<congr_lemma> mk_specialized_congr_simp(type_context & ctx, expr const & a);
old_type_context & ctx();
unsigned get_specialization_prefix_size(expr const & fn, unsigned nargs);
optional<congr_lemma> mk_congr(type_context & ctx, expr const & fn);
optional<congr_lemma> mk_congr(type_context & ctx, expr const & fn, unsigned nargs);
/* Create a specialized theorem using (a prefix of) the arguments of the given application. */
optional<congr_lemma> mk_specialized_congr(type_context & ctx, expr const & a);
optional<result> mk_congr_simp(expr const & fn);
optional<result> mk_congr_simp(expr const & fn, unsigned nargs);
/* Create a specialized theorem using (a prefix of) the arguments of the given application. */
optional<result> mk_specialized_congr_simp(expr const & a);
optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn);
optional<congr_lemma> mk_hcongr(type_context & ctx, expr const & fn, unsigned nargs);
optional<result> mk_congr(expr const & fn);
optional<result> mk_congr(expr const & fn, unsigned nargs);
/* Create a specialized theorem using (a prefix of) the arguments of the given application. */
optional<result> mk_specialized_congr(expr const & a);
/** \brief If R is an equivalence relation, construct the congruence lemma
optional<result> mk_hcongr(expr const & fn);
optional<result> mk_hcongr(expr const & fn, unsigned nargs);
R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) */
optional<congr_lemma> mk_rel_iff_congr(type_context & ctx, expr const & R);
/** \brief If R is an equivalence relation, construct the congruence lemma
/** \brief Similar to previous one.
It returns none if propext is not available.
R a1 a2 -> R b1 b2 -> (R a1 b1) <-> (R a2 b2) */
optional<result> mk_rel_iff_congr(expr const & R);
/** \brief Similar to previous one.
It returns none if propext is not available.
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();
R a1 a2 -> R b1 b2 -> (R a1 b1) = (R a2 b2) */
optional<congr_lemma> mk_rel_eq_congr(type_context & ctx, expr const & R);
}