From ba477a0e9869a7e2e8f5d44a349d01d739e96a10 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 Nov 2015 15:00:18 -0800 Subject: [PATCH] feat(library/congr_lemma_manager): handle simple congruence lemmas --- src/library/app_builder.cpp | 32 +++++++++++++++++ src/library/app_builder.h | 4 +++ src/library/congr_lemma_manager.cpp | 55 +++++++++++++++++++++++++---- src/library/congr_lemma_manager.h | 9 ++++- src/library/constants.cpp | 8 +++++ src/library/constants.h | 2 ++ src/library/constants.txt | 2 ++ tests/lean/extra/congr.lean | 10 ++++++ 8 files changed, 114 insertions(+), 8 deletions(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index b7a49263e..a619ab8d4 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -260,6 +260,10 @@ struct app_builder::imp { return some_expr(m_ctx->instantiate_uvars_mvars(e->m_app)); } + optional mk_app(name const & c, std::initializer_list const & it) { + return mk_app(c, it.size(), it.begin()); + } + static unsigned get_nargs(unsigned mask_sz, bool const * mask) { unsigned nargs = 0; for (unsigned i = 0; i < mask_sz; i++) { @@ -447,6 +451,22 @@ struct app_builder::imp { name const & eqrec = is_standard(m_ctx->env()) ? get_eq_drec_name() : get_eq_rec_name(); return some_expr(::lean::mk_app({mk_constant(eqrec, {l_1, *A_lvl}), A, lhs, motive, H1, rhs, H2})); } + + optional mk_congr_arg(expr const & f, expr const & H) { + // TODO(Leo): efficient version + + return mk_app(get_congr_arg_name(), {f, H}); + } + + optional mk_congr_fun(expr const & H, expr const & a) { + // TODO(Leo): efficient version + return mk_app(get_congr_fun_name(), {H, a}); + } + + optional mk_congr(expr const & H1, expr const & H2) { + // TODO(Leo): efficient version + return mk_app(get_congr_name(), {H1, H2}); + } }; app_builder::app_builder(environment const & env, io_state const & ios, reducible_behavior b): @@ -527,6 +547,18 @@ optional app_builder::mk_eq_drec(expr const & C, expr const & H1, expr con return m_ptr->mk_eq_drec(C, H1, H2); } +optional app_builder::mk_congr_arg(expr const & f, expr const & H) { + return m_ptr->mk_congr_arg(f, H); +} + +optional app_builder::mk_congr_fun(expr const & H, expr const & a) { + return m_ptr->mk_congr_fun(H, a); +} + +optional app_builder::mk_congr(expr const & H1, expr const & H2) { + return m_ptr->mk_congr(H1, H2); +} + optional app_builder::mk_sorry(expr const & type) { return mk_app(get_sorry_name(), type); } diff --git a/src/library/app_builder.h b/src/library/app_builder.h index ac724e374..554bea2ac 100644 --- a/src/library/app_builder.h +++ b/src/library/app_builder.h @@ -106,6 +106,10 @@ public: because eq.rec is a dependent eliminator in HoTT. */ optional mk_eq_drec(expr const & C, expr const & H1, expr const & H2); + optional mk_congr_arg(expr const & f, expr const & H); + optional mk_congr_fun(expr const & H, expr const & a); + optional mk_congr(expr const & H1, expr const & H2); + /** \brief Create (@sorry type) */ optional mk_sorry(expr const & type); diff --git a/src/library/congr_lemma_manager.cpp b/src/library/congr_lemma_manager.cpp index 389967ee7..77c3fd852 100644 --- a/src/library/congr_lemma_manager.cpp +++ b/src/library/congr_lemma_manager.cpp @@ -16,6 +16,7 @@ class congr_lemma_manager::imp { app_builder & m_builder; fun_info_manager & m_fmanager; type_context & m_ctx; + bool m_ignore_inst_implicit; struct key { expr const & m_fn; unsigned m_nargs; @@ -94,6 +95,37 @@ class congr_lemma_manager::imp { } } + bool has_cast(buffer const & kinds) { + return std::find(kinds.begin(), kinds.end(), congr_arg_kind::Cast) != kinds.end(); + } + + optional mk_simple_congr_proof(expr const & fn, buffer const & lhss, + buffer> const & eqs, buffer const & kinds) { + unsigned i = 0; + for (; i < kinds.size(); i++) { + if (kinds[i] != congr_arg_kind::Fixed) + break; + } + expr g = mk_app(fn, i, lhss.data()); + if (i == kinds.size()) + return m_builder.mk_eq_refl(g); + lean_assert(kinds[i] == congr_arg_kind::Eq); + lean_assert(eqs[i]); + optional pr = m_builder.mk_congr_arg(g, *eqs[i]); + if (!pr) return none_expr(); + i++; + for (; i < kinds.size(); i++) { + if (kinds[i] == congr_arg_kind::Eq) { + pr = m_builder.mk_congr(*pr, *eqs[i]); + } else { + lean_assert(kinds[i] == congr_arg_kind::Fixed); + pr = m_builder.mk_congr_fun(*pr, lhss[i]); + } + if (!pr) return none_expr(); + } + return pr; + } + optional mk_congr_simp(expr const & fn, buffer const & pinfos, buffer const & kinds) { expr fn_type = whnf(infer(fn)); name e_name("e"); @@ -146,15 +178,21 @@ class congr_lemma_manager::imp { if (!eq) return optional(); expr congr_type = Pi(hyps, *eq); - auto congr_proof = m_builder.mk_sorry(congr_type); - if (!congr_proof) - return optional(); + optional congr_proof; + if (has_cast(kinds)) { + // TODO(Leo): + congr_proof = m_builder.mk_sorry(congr_type); + } else { + congr_proof = mk_simple_congr_proof(fn, lhss, eqs, kinds); + } + if (!congr_proof) return optional(); + congr_proof = Fun(hyps, *congr_proof); return optional(congr_type, *congr_proof, to_list(kinds)); } public: - imp(app_builder & b, fun_info_manager & fm): - m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()) {} + imp(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit): + m_builder(b), m_fmanager(fm), m_ctx(fm.ctx()), m_ignore_inst_implicit(ignore_inst_implicit) {} optional mk_congr_simp(expr const & fn) { fun_info finfo = m_fmanager.get(fn); @@ -179,6 +217,9 @@ public: kinds[i] = congr_arg_kind::Fixed; else kinds[i] = congr_arg_kind::Cast; + } else if (pinfos[i].is_inst_implicit()) { + lean_assert(!pinfos[i].is_subsingleton()); + kinds[i] = congr_arg_kind::Fixed; } } for (unsigned i = 0; i < pinfos.size(); i++) { @@ -206,8 +247,8 @@ public: } }; -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(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit): + m_ptr(new imp(b, fm, ignore_inst_implicit)) { } congr_lemma_manager::~congr_lemma_manager() { diff --git a/src/library/congr_lemma_manager.h b/src/library/congr_lemma_manager.h index 6b17b0cf8..9236734a4 100644 --- a/src/library/congr_lemma_manager.h +++ b/src/library/congr_lemma_manager.h @@ -14,7 +14,14 @@ class congr_lemma_manager { struct imp; std::unique_ptr m_ptr; public: - congr_lemma_manager(app_builder & b, fun_info_manager & fm); + /** \brief When ignore_inst_implicit is set to true, then + for type class instance implicit arguments that are *not* subsingletons, + the mananger will create congruence lemmas where these arguments remain fixed. + This is the behavior we want most of the time. For example, when creating a + congruence for + add : Pi {A : Type} [s : has_add A], A -> A -> A + we want the argumet s to remain fixed. */ + congr_lemma_manager(app_builder & b, fun_info_manager & fm, bool ignore_inst_implicit = true); ~congr_lemma_manager(); enum class congr_arg_kind { Fixed, Eq, Cast }; diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 8aa7caed0..109dde065 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -16,6 +16,8 @@ name const * g_bool_tt = nullptr; name const * g_char = nullptr; name const * g_char_mk = nullptr; name const * g_congr = nullptr; +name const * g_congr_arg = nullptr; +name const * g_congr_fun = nullptr; name const * g_dite = nullptr; name const * g_div = nullptr; name const * g_empty = nullptr; @@ -174,6 +176,8 @@ void initialize_constants() { g_char = new name{"char"}; g_char_mk = new name{"char", "mk"}; g_congr = new name{"congr"}; + g_congr_arg = new name{"congr_arg"}; + g_congr_fun = new name{"congr_fun"}; g_dite = new name{"dite"}; g_div = new name{"div"}; g_empty = new name{"empty"}; @@ -333,6 +337,8 @@ void finalize_constants() { delete g_char; delete g_char_mk; delete g_congr; + delete g_congr_arg; + delete g_congr_fun; delete g_dite; delete g_div; delete g_empty; @@ -491,6 +497,8 @@ name const & get_bool_tt_name() { return *g_bool_tt; } name const & get_char_name() { return *g_char; } name const & get_char_mk_name() { return *g_char_mk; } name const & get_congr_name() { return *g_congr; } +name const & get_congr_arg_name() { return *g_congr_arg; } +name const & get_congr_fun_name() { return *g_congr_fun; } name const & get_dite_name() { return *g_dite; } name const & get_div_name() { return *g_div; } name const & get_empty_name() { return *g_empty; } diff --git a/src/library/constants.h b/src/library/constants.h index bbbee7933..445ce7fd2 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -18,6 +18,8 @@ name const & get_bool_tt_name(); name const & get_char_name(); name const & get_char_mk_name(); name const & get_congr_name(); +name const & get_congr_arg_name(); +name const & get_congr_fun_name(); name const & get_dite_name(); name const & get_div_name(); name const & get_empty_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 76cefda92..c4f5f432c 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -11,6 +11,8 @@ bool.tt char char.mk congr +congr_arg +congr_fun dite div empty diff --git a/tests/lean/extra/congr.lean b/tests/lean/extra/congr.lean index 8d1068753..d2782de67 100644 --- a/tests/lean/extra/congr.lean +++ b/tests/lean/extra/congr.lean @@ -2,8 +2,18 @@ section variables p : nat → Prop variables q : nat → nat → Prop variables f : Π (x y : nat), p x → q x y → nat +example : (0:nat) = 0 := sorry + +#congr @add + +#congr p + +#congr iff + end +exit + section variables p : nat → Prop