From 22dcf6825eb479d467a4ec857ea07fc1f0be4a3f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Nov 2015 19:12:22 -0800 Subject: [PATCH] feat(library/congr_lemma_manager): add congr_lemma_manager skeleton and compute type of congruence lemma proof is still missing --- src/library/CMakeLists.txt | 2 +- src/library/congr_lemma_manager.cpp | 198 ++++++++++++++++++++++++++++ src/library/congr_lemma_manager.h | 25 ++++ 3 files changed, 224 insertions(+), 1 deletion(-) create mode 100644 src/library/congr_lemma_manager.cpp create mode 100644 src/library/congr_lemma_manager.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 398cae5f0..50ce1b8a4 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -17,4 +17,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp composition_manager.cpp tc_multigraph.cpp noncomputable.cpp aux_recursors.cpp norm_num.cpp decl_stats.cpp meng_paulson.cpp norm_num.cpp class_instance_resolution.cpp type_context.cpp - tmp_type_context.cpp fun_info_manager.cpp) + tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp) diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp new file mode 100644 index 000000000..1b0b096e3 --- /dev/null +++ b/src/library/congr_lemma_manager.cpp @@ -0,0 +1,198 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/instantiate.h" +#include "kernel/abstract.h" +#include "library/util.h" +#include "library/locals.h" +#include "library/replace_visitor.h" +#include "library/congr_lemma_manager.h" + +namespace lean { +class congr_lemma_manager::imp { + app_builder & m_builder; + fun_info_manager & m_fmanager; + type_context & m_ctx; + expr_map m_cache; + + struct failure { + unsigned m_arg_idx; + failure(unsigned i):m_arg_idx(i) {} + }; + + expr infer(expr const & e) { return m_ctx.infer(e); } + expr whnf(expr const & e) { return m_ctx.whnf(e); } + + /** \brief (Try to) cast expression \c e to the given type using the equations \c eqs. + \c deps contains the indices of the relevant equalities. + \remark deps is sorted. */ + optional cast(expr const & e, expr const & type, list const & deps, buffer> const & eqs) { + if (!deps) + return some_expr(e); + unsigned d = head(deps); + auto major = eqs[d]; + if (!major) { + return cast(e, type, tail(deps), eqs); + } else { + expr lhs, rhs; + lean_verify(is_eq(mlocal_type(*major), lhs, rhs)); + lean_assert(is_local(lhs)); + lean_assert(is_local(rhs)); + // We compute the motive by replacing rhs with the fresh local x, + // and major with fresh local H. + // We compute the new type by replacing rhs with lhs, and major with (refl lhs). + expr motive, new_type; + bool use_drec; + if (depends_on(type, *major)) { + // 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)); + // We compute new_type by replacing rhs with lhs and *major with eq.refl(lhs) in type. + new_type = instantiate(abstract(type, rhs), lhs); + auto refl = m_builder.mk_eq_refl(lhs); + if (!refl) + return none_expr(); + new_type = instantiate(abstract(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); + new_type = instantiate(abstract(type, rhs), lhs); + } + auto minor = cast(e, new_type, tail(deps), eqs); + if (!minor) + return none_expr(); + if (use_drec) { + return m_builder.mk_eq_drec(motive, *minor, *major); + } else { + return m_builder.mk_eq_rec(motive, *minor, *major); + } + } + } + + optional mk_congr_simp(expr const & fn, buffer const & pinfos, buffer const & kinds) { + for (unsigned i = 0; i < kinds.size(); i++) + std::cout << (unsigned)kinds[i] << " "; + std::cout << "\n"; + + expr fn_type = whnf(infer(fn)); + name e_name("e"); + buffer lhss; + buffer rhss; // it contains the right-hand-side argument + buffer> eqs; // for Eq args, it contains the equality + buffer hyps; // contains lhss + rhss + eqs + for (unsigned i = 0; i < pinfos.size(); i++) { + if (!is_pi(fn_type)) { + return optional(); + } + expr lhs = m_ctx.mk_tmp_local(binding_name(fn_type), binding_domain(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; + if (auto it = m_builder.mk_eq(lhs, rhs)) + eq_type = *it; + else + return optional(); + rhss.push_back(rhs); + expr eq = m_ctx.mk_tmp_local(e_name.append_after(eqs.size()+1), eq_type); + eqs.push_back(some_expr(eq)); + hyps.push_back(rhs); + hyps.push_back(eq); + break; + } + case congr_arg_kind::Fixed: + rhss.push_back(lhs); + eqs.push_back(none_expr()); + 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()); + auto rhs = cast(lhs, rhs_type, pinfos[i].get_dependencies(), eqs); + if (!rhs) { + return optional(); + } + rhss.push_back(*rhs); + eqs.push_back(none_expr()); + break; + }} + // std::cout << lhss.back() << "\n"; + // std::cout << rhss.back() << "\n\n"; + fn_type = whnf(instantiate(binding_body(fn_type), lhs)); + } + expr lhs = mk_app(fn, lhss); + expr rhs = mk_app(fn, rhss); + auto eq = m_builder.mk_eq(lhs, rhs); + if (!eq) + return optional(); + expr congr_type = Pi(hyps, *eq); + std::cout << congr_type << "\n"; + // TODO(Leo): create proof + lean_unreachable(); + } + +public: + imp(app_builder & b, fun_info_manager & fm): + m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()) {} + + optional mk_congr_simp(expr const & fn) { + auto r = m_cache.find(fn); + if (r != m_cache.end()) + return optional(r->second); + fun_info finfo = m_fmanager.get(fn); + buffer kinds; + buffer pinfos; + to_buffer(finfo.get_params_info(), pinfos); + kinds.resize(pinfos.size(), congr_arg_kind::Eq); + for (unsigned i = 0; i < pinfos.size(); i++) { + if (pinfos[i].is_subsingleton()) { + if (empty(pinfos[i].get_dependencies())) + kinds[i] = congr_arg_kind::Fixed; + else + kinds[i] = congr_arg_kind::Cast; + } + } + for (unsigned i = 0; i < pinfos.size(); i++) { + for (unsigned j = i+1; j < pinfos.size(); j++) { + auto j_deps = pinfos[j].get_dependencies(); + 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, + // and j is not fixed nor a cast-fixed. + kinds[i] = congr_arg_kind::Fixed; + break; + } + } + } + while (true) { + try { + auto new_r = mk_congr_simp(fn, pinfos, kinds); + if (new_r) + m_cache.insert(mk_pair(fn, *new_r)); + return new_r; + } catch (failure & ex) { + kinds[ex.m_arg_idx] = congr_arg_kind::Fixed; + } + } + } +}; + +congr_lemma_manager::congr_lemma_manager(app_builder & b, fun_info_manager & fm): + m_ptr(new imp(b, fm)) { +} + +congr_lemma_manager::~congr_lemma_manager() { +} + +auto congr_lemma_manager::mk_congr_simp(expr const & fn) -> optional { + return m_ptr->mk_congr_simp(fn); +} +} diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h new file mode 100644 index 000000000..2c96052ab --- /dev/null +++ b/src/library/congr_lemma_manager.h @@ -0,0 +1,25 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include +#include "library/app_builder.h" +#include "library/fun_info_manager.h" + +namespace lean { +class congr_lemma_manager { + struct imp; + std::unique_ptr m_ptr; +public: + congr_lemma_manager(app_builder & b, fun_info_manager & fm); + ~congr_lemma_manager(); + + enum class congr_arg_kind { Fixed, Eq, Cast }; + + typedef pair> result; + optional mk_congr_simp(expr const & fn); +}; +}