From fa98c1358f8d8192f860435e2c362f4734d2fcb6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Dec 2013 04:41:08 -0800 Subject: [PATCH] feat(library/tactic): add disj_tactic Signed-off-by: Leonardo de Moura --- src/library/tactic/boolean.cpp | 92 ++++++++++++++++++++++++++++++ src/library/tactic/boolean.h | 3 + src/library/tactic/proof_state.cpp | 10 ++++ src/library/tactic/proof_state.h | 9 +++ src/library/tactic/tactic.cpp | 11 ++-- tests/lean/disj1.lean | 19 ++++++ tests/lean/disj1.lean.expected.out | 6 ++ 7 files changed, 143 insertions(+), 7 deletions(-) create mode 100644 tests/lean/disj1.lean create mode 100644 tests/lean/disj1.lean.expected.out diff --git a/src/library/tactic/boolean.cpp b/src/library/tactic/boolean.cpp index 1736ce314..7e6185fe1 100644 --- a/src/library/tactic/boolean.cpp +++ b/src/library/tactic/boolean.cpp @@ -239,6 +239,87 @@ tactic disj_hyp_tactic() { }); } +typedef std::pair proof_state_pair; + +optional disj_tactic(proof_state const & s, name gname) { + precision prec = s.get_precision(); + if (prec != precision::Precise && prec != precision::Over) { + // it is pointless to apply this tactic, since it will produce UnderOver + optional(); + } + buffer> new_goals_buf1, new_goals_buf2; + expr conclusion; + for (auto const & p : s.get_goals()) { + check_interrupted(); + goal const & g = p.second; + expr const & c = g.get_conclusion(); + if (!conclusion && ((gname.is_anonymous() && is_or(c)) || p.first == gname)) { + gname = p.first; + conclusion = c; + expr c1, c2; + if (is_or(c, c1, c2)) { + new_goals_buf1.emplace_back(gname, update(g, c1)); + new_goals_buf2.emplace_back(gname, update(g, c2)); + } else { + return optional(); // failed + } + } else { + new_goals_buf1.push_back(p); + new_goals_buf2.push_back(p); + } + } + if (!conclusion) { + return optional(); // failed + } else { + goals new_gs1 = to_list(new_goals_buf1.begin(), new_goals_buf1.end()); + goals new_gs2 = to_list(new_goals_buf2.begin(), new_goals_buf2.end()); + proof_builder pb = s.get_proof_builder(); + proof_builder new_pb1 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { + proof_map new_m(m); + new_m.insert(gname, Disj1(arg(conclusion, 1), arg(conclusion, 2), find(m, gname))); + return pb(new_m, a); + }); + proof_builder new_pb2 = mk_proof_builder([=](proof_map const & m, assignment const & a) -> expr { + proof_map new_m(m); + new_m.insert(gname, Disj2(arg(conclusion, 2), arg(conclusion, 1), find(m, gname))); + return pb(new_m, a); + }); + proof_state s1(precision::Over, new_gs1, s.get_menv(), new_pb1, s.get_cex_builder()); + proof_state s2(precision::Over, new_gs2, s.get_menv(), new_pb2, s.get_cex_builder()); + return some(mk_pair(s1, s2)); + } +} + +proof_state_seq disj_tactic_core(proof_state const & s, name const & gname) { + return mk_proof_state_seq([=]() { + auto p = disj_tactic(s, gname); + if (p) { + return some(mk_pair(p->first, proof_state_seq(p->second))); + } else { + return proof_state_seq::maybe_pair(); + } + }); +} + +tactic disj_tactic(name const & gname) { + return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + return disj_tactic_core(s, gname); + }); +} + +tactic disj_tactic() { + return disj_tactic(name()); +} + +tactic disj_tactic(unsigned i) { + return mk_tactic([=](environment const &, io_state const &, proof_state const & s) -> proof_state_seq { + if (optional n = s.get_ith_goal_name(i)) + return disj_tactic_core(s, *n); + else + return proof_state_seq(); + }); +} + tactic absurd_tactic() { return mk_tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { list> proofs; @@ -291,6 +372,16 @@ static int mk_disj_hyp_tactic(lua_State * L) { return push_tactic(L, disj_hyp_tactic(to_name_ext(L, 1), to_name_ext(L, 2))); } +static int mk_disj_tactic(lua_State * L) { + int nargs = lua_gettop(L); + if (nargs == 0) + return push_tactic(L, disj_tactic()); + else if (lua_isnumber(L, 1)) + return push_tactic(L, disj_tactic(lua_tointeger(L, 1))); + else + return push_tactic(L, disj_tactic(to_name_ext(L, 1))); +} + static int mk_absurd_tactic(lua_State * L) { return push_tactic(L, absurd_tactic()); } @@ -300,6 +391,7 @@ void open_boolean(lua_State * L) { SET_GLOBAL_FUN(mk_imp_tactic, "imp_tactic"); SET_GLOBAL_FUN(mk_conj_hyp_tactic, "conj_hyp_tactic"); SET_GLOBAL_FUN(mk_disj_hyp_tactic, "disj_hyp_tactic"); + SET_GLOBAL_FUN(mk_disj_tactic, "disj_tactic"); SET_GLOBAL_FUN(mk_absurd_tactic, "absurd_tactic"); } } diff --git a/src/library/tactic/boolean.h b/src/library/tactic/boolean.h index 4b34bf1ac..141324fbf 100644 --- a/src/library/tactic/boolean.h +++ b/src/library/tactic/boolean.h @@ -13,6 +13,9 @@ tactic imp_tactic(name const & H_name = name("H"), bool all = true); tactic disj_hyp_tactic(name const & goal_name, name const & hyp_name); tactic disj_hyp_tactic(name const & hyp_name); tactic disj_hyp_tactic(); +tactic disj_tactic(); +tactic disj_tactic(unsigned i); +tactic disj_tactic(name const & gname); tactic absurd_tactic(); void open_boolean(lua_State * L); } diff --git a/src/library/tactic/proof_state.cpp b/src/library/tactic/proof_state.cpp index 917a81004..8cfe7e60e 100644 --- a/src/library/tactic/proof_state.cpp +++ b/src/library/tactic/proof_state.cpp @@ -10,6 +10,16 @@ Author: Leonardo de Moura #include "library/tactic/proof_state.h" namespace lean { +optional get_ith_goal_name(goals const & gs, unsigned i) { + unsigned j = 1; + for (auto const & p : gs) { + if (i == j) + return some(p.first); + j++; + } + return optional(); +} + precision mk_union(precision p1, precision p2) { if (p1 == p2) return p1; else if (p1 == precision::Precise) return p2; diff --git a/src/library/tactic/proof_state.h b/src/library/tactic/proof_state.h index 2cf876849..b3e1ee28f 100644 --- a/src/library/tactic/proof_state.h +++ b/src/library/tactic/proof_state.h @@ -19,6 +19,12 @@ Author: Leonardo de Moura namespace lean { typedef list> goals; +/** + \brief Return the name of the i-th goal. + + \remark Return none if i == 0 or i > size(g) +*/ +optional get_ith_goal_name(goals const & gs, unsigned i); enum class precision { Precise, @@ -84,6 +90,9 @@ public: \brief Store in \c r the goal names */ void get_goal_names(name_set & r) const; + + optional get_ith_goal_name(unsigned i) const { return ::lean::get_ith_goal_name(get_goals(), i); } + format pp(formatter const & fmt, options const & opts) const; }; diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index d80bb8569..23f288371 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -342,13 +342,10 @@ tactic focus(tactic const & t, name const & gname) { tactic focus(tactic const & t, int i) { return mk_tactic([=](environment const & env, io_state const & io, proof_state const & s) -> proof_state_seq { - int j = 1; - for (auto const & p : s.get_goals()) { - if (i == j) - return focus_core(t, p.first, env, io, s); - j++; - } - return proof_state_seq(); + if (optional n = s.get_ith_goal_name(i)) + return focus_core(t, *n, env, io, s); + else + return proof_state_seq(); }); } diff --git a/tests/lean/disj1.lean b/tests/lean/disj1.lean new file mode 100644 index 000000000..9d8662e55 --- /dev/null +++ b/tests/lean/disj1.lean @@ -0,0 +1,19 @@ +Theorem T1 (a b : Bool) : a \/ b => b \/ a. + apply imp_tactic + apply disj_hyp_tactic + apply disj_tactic + back + apply assumption_tactic + apply disj_tactic + apply assumption_tactic + done + +(** +simple_tac = REPEAT(ORELSE(imp_tactic, assumption_tactic, disj_hyp_tactic, disj_tactic)) .. now_tactic +**) + +Theorem T2 (a b : Bool) : a \/ b => b \/ a. + apply simple_tac + done + +Show Environment 1. \ No newline at end of file diff --git a/tests/lean/disj1.lean.expected.out b/tests/lean/disj1.lean.expected.out new file mode 100644 index 000000000..03e073b15 --- /dev/null +++ b/tests/lean/disj1.lean.expected.out @@ -0,0 +1,6 @@ + Set: pp::colors + Set: pp::unicode + Proved: T1 + Proved: T2 +Theorem T2 (a b : Bool) : a ∨ b ⇒ b ∨ a := + Discharge (λ H : a ∨ b, DisjCases H (λ H : a, Disj2 b H) (λ H : b, Disj1 a H))