From b18b49dd6bd3323fe2f5affdaca28f0ac07f433c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Jan 2017 15:47:58 -0800 Subject: [PATCH] feat(library/tactic/smt/smt_state): add tactic for adding equational lemmas for a definition --- library/init/meta/smt/interactive.lean | 15 +++++++++++ library/init/meta/smt/smt_tactic.lean | 16 ++++++++++++ src/library/tactic/eqn_lemmas.cpp | 35 ++++++++++++++++++++++++++ src/library/tactic/eqn_lemmas.h | 3 +++ src/library/tactic/smt/smt_state.cpp | 32 +++++++++++++++++++++++ tests/lean/run/smt_tests.lean | 32 +++++++++++++++++++++-- 6 files changed, 131 insertions(+), 2 deletions(-) diff --git a/library/init/meta/smt/interactive.lean b/library/init/meta/smt/interactive.lean index 8193441df2..3a7f800453 100644 --- a/library/init/meta/smt/interactive.lean +++ b/library/init/meta/smt/interactive.lean @@ -129,5 +129,20 @@ add_lemma_pexprs reducible ff l meta def add_lhs_lemma (l : qexpr_list_or_qexpr0) : smt_tactic unit := add_lemma_pexprs reducible tt l +private meta def add_eqn_lemmas_for_core (md : transparency) : list name → smt_tactic unit +| [] := return () +| (c::cs) := do + e ← resolve_name c, + match e with + | expr.const n _ := add_ematch_eqn_lemmas_for_core md n >> add_eqn_lemmas_for_core cs + | _ := fail $ "'" ++ to_string c ++ "' is not a constant" + end + +meta def add_eqn_lemmas_for (ids : raw_ident_list) : smt_tactic unit := +add_eqn_lemmas_for_core reducible ids + +meta def add_eqn_lemmas (ids : raw_ident_list) : smt_tactic unit := +add_eqn_lemmas_for ids + end interactive end smt_tactic diff --git a/library/init/meta/smt/smt_tactic.lean b/library/init/meta/smt/smt_tactic.lean index dcc12dd48e..4f245b5d7d 100644 --- a/library/init/meta/smt/smt_tactic.lean +++ b/library/init/meta/smt/smt_tactic.lean @@ -103,6 +103,7 @@ meta constant close : smt_tactic unit meta constant ematch_core : (expr → bool) → smt_tactic unit meta constant add_ematch_lemma_core : transparency → bool → expr → smt_tactic unit meta constant add_ematch_lemma_from_decl_core : transparency → bool → name → smt_tactic unit +meta constant add_ematch_eqn_lemmas_for_core : transparency → name → smt_tactic unit meta constant to_cc_state : smt_tactic cc_state meta constant to_em_state : smt_tactic ematch_state meta constant preprocess : expr → smt_tactic (expr × expr) @@ -262,6 +263,21 @@ meta def get_refuted_facts : smt_tactic (list expr) := do cc ← to_cc_state, return $ cc^.eqc_of expr.mk_false +meta def add_ematch_lemma : expr → smt_tactic unit := +add_ematch_lemma_core reducible ff + +meta def add_ematch_lhs_lemma : expr → smt_tactic unit := +add_ematch_lemma_core reducible tt + +meta def add_ematch_lemma_from_decl : name → smt_tactic unit := +add_ematch_lemma_from_decl_core reducible ff + +meta def add_ematch_lhs_lemma_from_decl : name → smt_tactic unit := +add_ematch_lemma_from_decl_core reducible ff + +meta def add_ematch_eqn_lemmas_for : name → smt_tactic unit := +add_ematch_eqn_lemmas_for_core reducible + meta def add_lemmas_from_facts_core : list expr → smt_tactic unit | [] := return () | (f::fs) := do diff --git a/src/library/tactic/eqn_lemmas.cpp b/src/library/tactic/eqn_lemmas.cpp index a5b67ac9b9..904437bed2 100644 --- a/src/library/tactic/eqn_lemmas.cpp +++ b/src/library/tactic/eqn_lemmas.cpp @@ -5,9 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "kernel/for_each_fn.h" #include "library/attribute_manager.h" #include "library/kernel_serializer.h" #include "library/trace.h" +#include "library/util.h" #include "library/constants.h" #include "library/module.h" #include "library/tactic/eqn_lemmas.h" @@ -93,6 +95,39 @@ void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_o } } +void get_eqn_lemmas_for(environment const & env, name const & cname, buffer & result) { + name base(name(cname, "equations"), "eqn"); + unsigned idx = 1; + while (true) { + name eqn = base.append_after(idx); + if (env.find(eqn)) { + result.push_back(eqn); + idx++; + } else { + break; + } + } +} + +void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer & result) { + name_set visited; + unsigned i = result.size(); + get_eqn_lemmas_for(env, cname, result); + for (; i < result.size(); i++) { + expr type = env.get(result[i]).get_type(); + for_each(type, [&](expr const & e, unsigned) { + if (is_constant(e)) { + name const & n = const_name(e); + if (n != cname && is_prefix_of(cname, n) && !visited.contains(n) && is_internal_name(n)) { + get_eqn_lemmas_for(env, n, result); + visited.insert(n); + } + } + return true; + }); + } +} + bool has_eqn_lemmas(environment const & env, name const & cname) { eqn_lemmas_ext const & ext = get_extension(env); return ext.m_lemmas.contains(cname); diff --git a/src/library/tactic/eqn_lemmas.h b/src/library/tactic/eqn_lemmas.h index 2cb3953a2c..839fc21323 100644 --- a/src/library/tactic/eqn_lemmas.h +++ b/src/library/tactic/eqn_lemmas.h @@ -11,6 +11,9 @@ namespace lean { environment add_eqn_lemma(environment const & env, name const & eqn_lemma); bool has_eqn_lemmas(environment const & env, name const & cname); void get_eqn_lemmas_for(environment const & env, name const & cname, bool refl_only, buffer & result); +void get_eqn_lemmas_for(environment const & env, name const & cname, buffer & result); +void get_ext_eqn_lemmas_for(environment const & env, name const & cname, buffer & result); + void initialize_eqn_lemmas(); void finalize_eqn_lemmas(); } diff --git a/src/library/tactic/smt/smt_state.cpp b/src/library/tactic/smt/smt_state.cpp index 9a29e7c7f7..625faaf857 100644 --- a/src/library/tactic/smt/smt_state.cpp +++ b/src/library/tactic/smt/smt_state.cpp @@ -23,6 +23,7 @@ Author: Leonardo de Moura #include "library/tactic/revert_tactic.h" #include "library/tactic/dsimplify.h" #include "library/tactic/simplify.h" +#include "library/tactic/eqn_lemmas.h" #include "library/tactic/change_tactic.h" #include "library/tactic/smt/congruence_tactics.h" #include "library/tactic/smt/ematch.h" @@ -706,6 +707,36 @@ vm_obj smt_tactic_add_ematch_lemma_from_decl_core(vm_obj const & md, vm_obj cons LEAN_TACTIC_CATCH(ts); } +vm_obj smt_tactic_add_ematch_eqn_lemmas_for_core(vm_obj const & md, vm_obj const & decl_name, vm_obj const & ss, vm_obj const & _ts) { + tactic_state ts = to_tactic_state(_ts); + if (is_nil(ss)) return mk_smt_state_empty_exception(ts); + lean_assert(ts.goals()); + LEAN_TACTIC_TRY; + type_context ctx = mk_type_context_for(ts); + smt_goal g = to_smt_goal(head(ss)); + smt S(ctx, g); + buffer eqns; + get_ext_eqn_lemmas_for(ts.env(), to_name(decl_name), eqns); + if (eqns.empty()) + return mk_tactic_exception(sstream() << "tactic failed, '" << to_name(decl_name) << "' does not have equation lemmas", ts); + for (name const & eqn : eqns) { + declaration eqn_decl = ctx.env().get(eqn); + if (eqn_decl.get_num_univ_params() == 0 && !is_pi(ctx.relaxed_whnf(ctx.env().get(eqn).get_type()))) { + expr h = mk_constant(eqn); + expr type = ctx.infer(h); + std::tie(type, h) = preprocess_forward(ctx, g, type, h); + S.add(type, h); + } else { + hinst_lemma lemma = mk_hinst_lemma(ctx, to_transparency_mode(md), eqn, true); + g.add_lemma(lemma); + } + } + vm_obj new_ss = mk_vm_cons(to_obj(g), tail(ss)); + tactic_state new_ts = set_env_mctx(ts, ctx.env(), ctx.mctx()); + return mk_smt_tactic_success(new_ss, new_ts); + LEAN_TACTIC_CATCH(ts); +} + vm_obj smt_tactic_to_cc_state(vm_obj const & ss, vm_obj const & ts) { if (is_nil(ss)) return mk_smt_state_empty_exception(ts); return mk_smt_tactic_success(to_obj(to_smt_goal(head(ss)).get_cc_state()), ss, ts); @@ -745,6 +776,7 @@ void initialize_smt_state() { DECLARE_VM_BUILTIN(name({"smt_tactic", "preprocess"}), smt_tactic_preprocess); DECLARE_VM_BUILTIN(name({"smt_tactic", "add_ematch_lemma_core"}), smt_tactic_add_ematch_lemma_core); DECLARE_VM_BUILTIN(name({"smt_tactic", "add_ematch_lemma_from_decl_core"}), smt_tactic_add_ematch_lemma_from_decl_core); + DECLARE_VM_BUILTIN(name({"smt_tactic", "add_ematch_eqn_lemmas_for_core"}), smt_tactic_add_ematch_eqn_lemmas_for_core); } void finalize_smt_state() { diff --git a/tests/lean/run/smt_tests.lean b/tests/lean/run/smt_tests.lean index a59eaf2c9f..c99578f05a 100644 --- a/tests/lean/run/smt_tests.lean +++ b/tests/lean/run/smt_tests.lean @@ -4,8 +4,6 @@ constant p : nat → nat → Prop constants a b : nat constant h : p (a + 1 * b + 0) (a + b) -set_option trace.app_builder true - open tactic smt_tactic def ex : p (a + b) (a + b) := @@ -18,3 +16,33 @@ begin [smt] exact new_h } end + +def foo : nat → nat +| 0 := 0 +| (n+1) := 2*n + +example (n : nat) : n = 0 → foo (n+1) = 2*0 := +begin [smt] + add_lemma [mul_zero, zero_mul], + add_eqn_lemmas foo, + ematch +end + +example (n : nat) : n = 0 → foo n = 0 := +begin [smt] + add_eqn_lemmas foo +end + +def boo : nat → nat +| 0 := 1 +| (n+1) := + match foo n with + | 0 := 2 + | _ := 3 + end + +example (n : nat) : n = 0 → boo (n+1) = 2 := +begin [smt] + add_eqn_lemmas boo foo, + ematch, +end