From e379034b95b6010a818fbf251d39fc3402147bb4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 May 2015 17:32:03 -0700 Subject: [PATCH] feat(library/tactic): improve 'assumption' tactic - It uses the unifier in "conservative" mode - It only affects the current goal closes #570 --- src/library/tactic/apply_tactic.cpp | 26 +++++++++++++++++----- src/library/tactic/apply_tactic.h | 1 + src/library/tactic/expr_to_tactic.cpp | 2 -- src/library/tactic/tactic.cpp | 32 --------------------------- src/library/tactic/tactic.h | 2 -- tests/lean/hott/congr_tac.hlean | 2 +- tests/lean/hott/constr_tac.hlean | 5 +---- tests/lean/run/570.lean | 16 ++++++++++++++ tests/lean/run/570b.lean | 8 +++++++ tests/lean/run/congr_tac.lean | 4 ++-- tests/lean/run/constr_tac.lean | 7 ++---- tests/lean/run/eqv_tacs.lean | 6 ++--- tests/lean/run/match_tac2.lean | 4 ++-- tests/lean/run/tactic12.lean | 8 ++++--- tests/lean/run/tactic13.lean | 4 ++-- tests/lean/run/tactic14.lean | 3 ++- tests/lean/run/tactic17.lean | 3 +-- tests/lean/run/tactic24.lean | 2 +- tests/lean/run/tactic25.lean | 2 +- tests/lean/run/tactic7.lean | 2 +- tests/lean/run/tactic9.lean | 2 +- tests/lean/run/tactic_notation.lean | 4 ++-- tests/lean/run/using_expr.lean | 2 +- tests/lua/tactic1.lua | 6 ----- 24 files changed, 73 insertions(+), 80 deletions(-) create mode 100644 tests/lean/run/570.lean create mode 100644 tests/lean/run/570b.lean diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 1c9826f386..2db78982de 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -71,7 +71,8 @@ enum add_meta_kind { DoNotAdd, AddDiff, AddAll }; static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & _e, buffer & cs, - add_meta_kind add_meta, subgoals_action_kind subgoals_action) { + add_meta_kind add_meta, subgoals_action_kind subgoals_action, + optional const & uk = optional()) { goals const & gs = s.get_goals(); if (empty(gs)) { throw_no_goal_if_enabled(s); @@ -92,6 +93,8 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const local_context ctx; bool initialized_ctx = false; unifier_config cfg(ios.get_options()); + if (uk) + cfg.m_kind = *uk; if (add_meta != DoNotAdd) { unsigned num_e_t = get_expect_num_args(*tc, e_t); if (add_meta == AddDiff) { @@ -178,9 +181,9 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const } static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, - add_meta_kind add_meta, subgoals_action_kind subgoals_action) { + add_meta_kind add_meta, subgoals_action_kind subgoals_action, optional const & uk = optional()) { buffer cs; - return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action); + return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action, uk); } proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) { @@ -195,7 +198,7 @@ tactic apply_tactic_core(expr const & e, constraint_seq const & cs) { }); } -tactic eassumption_tactic() { +static tactic assumption_tactic_core(optional uk) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); if (empty(gs)) { @@ -206,14 +209,22 @@ tactic eassumption_tactic() { proof_state_seq r; goal g = head(gs); buffer hs; - get_app_args(g.get_meta(), hs); + g.get_hyps(hs); for (expr const & h : hs) { - r = append(r, apply_tactic_core(env, ios, new_s, h, DoNotAdd, IgnoreSubgoals)); + r = append(r, apply_tactic_core(env, ios, new_s, h, DoNotAdd, IgnoreSubgoals, uk)); } return r; }); } +tactic eassumption_tactic() { + return assumption_tactic_core(optional()); +} + +tactic assumption_tactic() { + return assumption_tactic_core(optional(unifier_kind::Conservative)); +} + tactic apply_tactic_core(elaborate_fn const & elab, expr const & e, add_meta_kind add_meta, subgoals_action_kind k) { return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); @@ -277,6 +288,9 @@ void initialize_apply_tactic() { register_simple_tac(get_tactic_eassumption_name(), []() { return eassumption_tactic(); }); + + register_simple_tac(get_tactic_assumption_name(), + []() { return assumption_tactic(); }); } void finalize_apply_tactic() { diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 8211a97a03..ea73d23e9c 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -13,6 +13,7 @@ tactic apply_tactic_core(expr const & e, constraint_seq const & cs = constraint_ tactic apply_tactic(elaborate_fn const & fn, expr const & e); tactic fapply_tactic(elaborate_fn const & fn, expr const & e); tactic eassumption_tactic(); +tactic assumption_tactic(); void open_apply_tactic(lua_State * L); void initialize_apply_tactic(); void finalize_apply_tactic(); diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index bc56c35171..44084eeb28 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -367,8 +367,6 @@ void initialize_expr_to_tactic() { []() { return id_tactic(); }); register_simple_tac(get_tactic_now_name(), []() { return now_tactic(); }); - register_simple_tac(get_tactic_assumption_name(), - []() { return assumption_tactic(); }); register_simple_tac(get_tactic_fail_name(), []() { return fail_tactic(); }); register_simple_tac(get_tactic_beta_name(), diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 8f704f1e7e..3812adc448 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -220,36 +220,6 @@ tactic discard(tactic const & t, unsigned k) { }); } -tactic assumption_tactic() { - return tactic01([](environment const &, io_state const &, proof_state const & s) -> optional { - substitution subst = s.get_subst(); - bool solved = false; - goals new_gs = map_goals(s, [&](goal const & g) -> optional { - expr const & t = g.get_type(); - optional h; - buffer hyps; - g.get_hyps(hyps); - for (auto const & l : hyps) { - if (mlocal_type(l) == t) { - h = l; - break; - } - } - if (h) { - assign(subst, g, *h); - solved = true; - return optional(); - } else { - return some(g); - } - }); - if (solved) - return some(proof_state(s, new_gs, subst)); - else - return none_proof_state(); - }); -} - tactic beta_tactic() { return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional { bool reduced = false; @@ -421,7 +391,6 @@ static int mk_lua_when_tactic(lua_State * L) { return mk_lua_cond_tactic(L, to_t static int mk_id_tactic(lua_State * L) { return push_tactic(L, id_tactic()); } static int mk_now_tactic(lua_State * L) { return push_tactic(L, now_tactic()); } static int mk_fail_tactic(lua_State * L) { return push_tactic(L, fail_tactic()); } -static int mk_assumption_tactic(lua_State * L) { return push_tactic(L, assumption_tactic()); } static int mk_beta_tactic(lua_State * L) { return push_tactic(L, beta_tactic()); } static const struct luaL_Reg tactic_m[] = { {"__gc", tactic_gc}, // never throws @@ -460,7 +429,6 @@ void open_tactic(lua_State * L) { SET_GLOBAL_FUN(mk_id_tactic, "id_tac"); SET_GLOBAL_FUN(mk_now_tactic, "now_tac"); SET_GLOBAL_FUN(mk_fail_tactic, "fail_tac"); - SET_GLOBAL_FUN(mk_assumption_tactic, "assumption_tac"); SET_GLOBAL_FUN(mk_beta_tactic, "beta_tac"); SET_GLOBAL_FUN(mk_lua_tactic01, "tactic01"); diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index d8e2fe945e..685fa539f6 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -56,8 +56,6 @@ tactic id_tactic(); tactic fail_tactic(); /** \brief Return a tactic that fails if there are unsolved goals. */ tactic now_tactic(); -/** \brief Return a tactic that solves any goal of the form ..., H : A, ... |- A. */ -tactic assumption_tactic(); /** \brief Return a tactic that performs \c t1 followed by \c t2. */ tactic then(tactic const & t1, tactic const & t2); inline tactic operator<<(tactic const & t1, tactic const & t2) { return then(t1, t2); } diff --git a/tests/lean/hott/congr_tac.hlean b/tests/lean/hott/congr_tac.hlean index 77714eb8eb..af5b06da3c 100644 --- a/tests/lean/hott/congr_tac.hlean +++ b/tests/lean/hott/congr_tac.hlean @@ -14,7 +14,7 @@ begin end example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c := -by intros; congruence; assumption +by intros; congruence; repeat assumption inductive list (A : Type) := | nil {} : list A diff --git a/tests/lean/hott/constr_tac.hlean b/tests/lean/hott/constr_tac.hlean index 68545623ba..0f1903182d 100644 --- a/tests/lean/hott/constr_tac.hlean +++ b/tests/lean/hott/constr_tac.hlean @@ -3,10 +3,7 @@ open prod example (a b c : Type) : a → b → c → a × b × c := begin intro Ha Hb Hc, - split, - assumption, - split, - assumption + repeat (split | assumption) end example (a b : Type) : a → sum a b := diff --git a/tests/lean/run/570.lean b/tests/lean/run/570.lean new file mode 100644 index 0000000000..8bfbb72373 --- /dev/null +++ b/tests/lean/run/570.lean @@ -0,0 +1,16 @@ +open nat +variables (P : ℕ → Prop) + +example (H1 : ∃n, P n) : ∃n, P n := +begin + cases H1 with n p, + apply (exists.intro n), + assumption +end + +example (H1 : ∃n, P n) : ∃n, P n := +begin + cases H1 with n p, + existsi n, + assumption +end diff --git a/tests/lean/run/570b.lean b/tests/lean/run/570b.lean new file mode 100644 index 0000000000..7813617889 --- /dev/null +++ b/tests/lean/run/570b.lean @@ -0,0 +1,8 @@ +theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := +begin + apply and.intro, + assume Ha, or.elim H + (assume Hna, @absurd _ false Ha Hna) + (assume Hnb, @absurd _ false Hb Hnb), + assumption +end diff --git a/tests/lean/run/congr_tac.lean b/tests/lean/run/congr_tac.lean index a08f419dca..23b3a5a74e 100644 --- a/tests/lean/run/congr_tac.lean +++ b/tests/lean/run/congr_tac.lean @@ -16,7 +16,7 @@ begin end example (f g : nat → nat → nat) (a b c : nat) : f = g → b = c → f a b = g a c := -by intros; congruence; assumption +by intros; congruence; repeat assumption open list @@ -31,4 +31,4 @@ begin end example (a b : nat) : a = b → [a] ++ [b] = [b] ++ [a] := -by intros; repeat (congruence | assumption | apply eq.symm) +by intros; repeat (congruence | assumption | symmetry) diff --git a/tests/lean/run/constr_tac.lean b/tests/lean/run/constr_tac.lean index 3559a4053a..6d5b4b2982 100644 --- a/tests/lean/run/constr_tac.lean +++ b/tests/lean/run/constr_tac.lean @@ -6,16 +6,13 @@ begin split, assumption, split, - assumption + repeat assumption end example (a b c : Type) : a → b → c → a × b × c := begin intro Ha Hb Hc, - split, - assumption, - split, - assumption + repeat (split | assumption) end example (a b : Type) : a → sum a b := diff --git a/tests/lean/run/eqv_tacs.lean b/tests/lean/run/eqv_tacs.lean index e6eadfbe0e..54dbe1f86f 100644 --- a/tests/lean/run/eqv_tacs.lean +++ b/tests/lean/run/eqv_tacs.lean @@ -14,7 +14,7 @@ begin intros, symmetry, transitivity b, - assumption + repeat assumption end example (a b c : Prop) : (a ↔ b) → (b ↔ c) → (c ↔ a) := @@ -22,7 +22,7 @@ begin intros, symmetry, transitivity b, - assumption + repeat assumption end example {A B C : Type} (a : A) (b : B) (c : C) : a == b → b == c → c == a := @@ -30,5 +30,5 @@ begin intros, symmetry, transitivity b, - assumption + repeat assumption end diff --git a/tests/lean/run/match_tac2.lean b/tests/lean/run/match_tac2.lean index 06d2b3f9b1..a09e5d3f8d 100644 --- a/tests/lean/run/match_tac2.lean +++ b/tests/lean/run/match_tac2.lean @@ -3,10 +3,10 @@ begin apply iff.intro, {intro H, match H with - | and.intro H₁ H₂ := by apply and.intro; assumption + | and.intro H₁ H₂ := by apply and.intro; repeat assumption end}, {intro H, match H with - | and.intro H₁ H₂ := by apply and.intro; assumption + | and.intro H₁ H₂ := by apply and.intro; repeat assumption end}, end diff --git a/tests/lean/run/tactic12.lean b/tests/lean/run/tactic12.lean index 8a1a5d7eb0..13d33a88e7 100644 --- a/tests/lean/run/tactic12.lean +++ b/tests/lean/run/tactic12.lean @@ -2,9 +2,11 @@ import logic open tactic theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b -:= by apply and.intro; - assumption; +:= begin + apply and.intro, exact (assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) - (assume Hnb, @absurd _ false Hb Hnb)) + (assume Hnb, @absurd _ false Hb Hnb)), + assumption + end diff --git a/tests/lean/run/tactic13.lean b/tests/lean/run/tactic13.lean index bf28801f72..d77e498123 100644 --- a/tests/lean/run/tactic13.lean +++ b/tests/lean/run/tactic13.lean @@ -4,8 +4,8 @@ open tactic theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := begin apply and.intro, - assumption, assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) - (assume Hnb, @absurd _ false Hb Hnb) + (assume Hnb, @absurd _ false Hb Hnb), + assumption end diff --git a/tests/lean/run/tactic14.lean b/tests/lean/run/tactic14.lean index e0defea4e5..adcc2113b2 100644 --- a/tests/lean/run/tactic14.lean +++ b/tests/lean/run/tactic14.lean @@ -12,5 +12,6 @@ theorem tst (a b : Prop) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b := begin assume Ha, or.elim H (assume Hna, @absurd _ false Ha Hna) - (assume Hnb, @absurd _ false Hb Hnb) + (assume Hnb, @absurd _ false Hb Hnb), + now end diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean index a6b6df6a29..aa4d76bb6a 100644 --- a/tests/lean/run/tactic17.lean +++ b/tests/lean/run/tactic17.lean @@ -7,7 +7,6 @@ constant f : A → A → A theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c := begin apply (@congr A A (f a) (f b)), - assumption, apply (congr_arg f), - assumption + repeat assumption end diff --git a/tests/lean/run/tactic24.lean b/tests/lean/run/tactic24.lean index 3c09f9bf16..65049d7b39 100644 --- a/tests/lean/run/tactic24.lean +++ b/tests/lean/run/tactic24.lean @@ -5,7 +5,7 @@ notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r infixl `;`:15 := tactic.and_then definition my_tac1 := apply @eq.refl -definition my_tac2 := repeat (apply @and.intro; assumption) +definition my_tac2 := repeat (apply @and.intro | assumption) tactic_hint my_tac1 tactic_hint my_tac2 diff --git a/tests/lean/run/tactic25.lean b/tests/lean/run/tactic25.lean index dfbd29bac5..60f3258c28 100644 --- a/tests/lean/run/tactic25.lean +++ b/tests/lean/run/tactic25.lean @@ -2,7 +2,7 @@ import logic open tactic definition my_tac1 := apply @eq.refl -definition my_tac2 := repeat (and_then (apply and.intro) assumption) +definition my_tac2 := repeat (or_else (apply and.intro) assumption) tactic_hint my_tac1 tactic_hint my_tac2 diff --git a/tests/lean/run/tactic7.lean b/tests/lean/run/tactic7.lean index c0a1fd57ce..4f96b49953 100644 --- a/tests/lean/run/tactic7.lean +++ b/tests/lean/run/tactic7.lean @@ -2,7 +2,7 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A -:= by apply and.intro; state; assumption; apply and.intro; assumption +:= by apply and.intro; state; assumption; apply and.intro; repeat assumption check tst theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A diff --git a/tests/lean/run/tactic9.lean b/tests/lean/run/tactic9.lean index ea0c237901..1d365fb966 100644 --- a/tests/lean/run/tactic9.lean +++ b/tests/lean/run/tactic9.lean @@ -2,4 +2,4 @@ import logic open tactic theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A -:= by apply and.intro; beta; assumption; apply and.intro; assumption +:= by repeat (split | assumption) diff --git a/tests/lean/run/tactic_notation.lean b/tests/lean/run/tactic_notation.lean index df3caa5667..25d72169d0 100644 --- a/tests/lean/run/tactic_notation.lean +++ b/tests/lean/run/tactic_notation.lean @@ -4,8 +4,8 @@ theorem tst1 (a b c : Prop) : a → b → a ∧ b := begin intros, apply and.intro, - assumption + repeat assumption end theorem tst2 (a b c : Prop) : a → b → a ∧ b := -by intros; apply and.intro; assumption +by intros; apply and.intro; repeat assumption diff --git a/tests/lean/run/using_expr.lean b/tests/lean/run/using_expr.lean index 8c0ba81739..2b67b830fc 100644 --- a/tests/lean/run/using_expr.lean +++ b/tests/lean/run/using_expr.lean @@ -4,5 +4,5 @@ have Hq : q, from and.elim_right H, using Hp Hq, begin apply and.intro, assumption, - apply and.intro, assumption + apply and.intro, repeat assumption end diff --git a/tests/lua/tactic1.lua b/tests/lua/tactic1.lua index b20284203c..ab5fc40864 100644 --- a/tests/lua/tactic1.lua +++ b/tests/lua/tactic1.lua @@ -7,9 +7,3 @@ local b = Local("b", A) local H = Local("H", eq(A, a, b)) local m = mk_metavar("m", Pi(A, a, b, H, eq(A, a, b)))(A, a, b, H) local s = to_proof_state(m, eq(A, a, b)) -local t = assumption_tac() -for r in t(env, s) do - print("Solution:") - print(r) - print("---------") -end