From ca8943f45b0285faeb7c803f29dc9e3fc244eb87 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 27 Apr 2015 15:06:16 -0700 Subject: [PATCH] feat(library,hott): remove rapply tactic --- hott/init/tactic.hlean | 1 - library/init/tactic.lean | 1 - src/library/constants.cpp | 4 ---- src/library/constants.h | 1 - src/library/constants.txt | 1 - src/library/tactic/apply_tactic.cpp | 10 ---------- src/library/tactic/apply_tactic.h | 1 - tests/lean/run/intros.lean | 6 +++--- tests/lean/run/tactic10.lean | 8 ++++---- tests/lean/run/tactic11.lean | 16 ++++++++-------- 10 files changed, 15 insertions(+), 34 deletions(-) diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 1515ac415c..d5d903d45e 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -65,7 +65,6 @@ definition identifier_list := expr_list definition opt_identifier_list := expr_list opaque definition apply (e : expr) : tactic := builtin -opaque definition rapply (e : expr) : tactic := builtin opaque definition fapply (e : expr) : tactic := builtin opaque definition rename (a b : identifier) : tactic := builtin opaque definition intro (e : identifier) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 7f7afe9781..ed7d48e1f3 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -65,7 +65,6 @@ definition identifier_list := expr_list definition opt_identifier_list := expr_list opaque definition apply (e : expr) : tactic := builtin -opaque definition rapply (e : expr) : tactic := builtin opaque definition fapply (e : expr) : tactic := builtin opaque definition rename (a b : identifier) : tactic := builtin opaque definition intro (e : identifier) : tactic := builtin diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 7c77ba21f1..fe744fca3d 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -63,7 +63,6 @@ name const * g_tactic_all_goals = nullptr; name const * g_tactic_apply = nullptr; name const * g_tactic_assert_hypothesis = nullptr; name const * g_tactic_fapply = nullptr; -name const * g_tactic_rapply = nullptr; name const * g_tactic_eassumption = nullptr; name const * g_tactic_and_then = nullptr; name const * g_tactic_append = nullptr; @@ -182,7 +181,6 @@ void initialize_constants() { g_tactic_apply = new name{"tactic", "apply"}; g_tactic_assert_hypothesis = new name{"tactic", "assert_hypothesis"}; g_tactic_fapply = new name{"tactic", "fapply"}; - g_tactic_rapply = new name{"tactic", "rapply"}; g_tactic_eassumption = new name{"tactic", "eassumption"}; g_tactic_and_then = new name{"tactic", "and_then"}; g_tactic_append = new name{"tactic", "append"}; @@ -302,7 +300,6 @@ void finalize_constants() { delete g_tactic_apply; delete g_tactic_assert_hypothesis; delete g_tactic_fapply; - delete g_tactic_rapply; delete g_tactic_eassumption; delete g_tactic_and_then; delete g_tactic_append; @@ -421,7 +418,6 @@ name const & get_tactic_all_goals_name() { return *g_tactic_all_goals; } name const & get_tactic_apply_name() { return *g_tactic_apply; } name const & get_tactic_assert_hypothesis_name() { return *g_tactic_assert_hypothesis; } name const & get_tactic_fapply_name() { return *g_tactic_fapply; } -name const & get_tactic_rapply_name() { return *g_tactic_rapply; } name const & get_tactic_eassumption_name() { return *g_tactic_eassumption; } name const & get_tactic_and_then_name() { return *g_tactic_and_then; } name const & get_tactic_append_name() { return *g_tactic_append; } diff --git a/src/library/constants.h b/src/library/constants.h index 0818e77102..340229cd15 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -65,7 +65,6 @@ name const & get_tactic_all_goals_name(); name const & get_tactic_apply_name(); name const & get_tactic_assert_hypothesis_name(); name const & get_tactic_fapply_name(); -name const & get_tactic_rapply_name(); name const & get_tactic_eassumption_name(); name const & get_tactic_and_then_name(); name const & get_tactic_append_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index fee4f056ee..d95a84a956 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -58,7 +58,6 @@ tactic.all_goals tactic.apply tactic.assert_hypothesis tactic.fapply -tactic.rapply tactic.eassumption tactic.and_then tactic.append diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 88ecb3bdd7..2f41e4aac7 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -225,10 +225,6 @@ tactic fapply_tactic(elaborate_fn const & elab, expr const & e) { return apply_tactic_core(elab, e, AddAllSubgoals); } -tactic rapply_tactic(elaborate_fn const & elab, expr const & e) { - return apply_tactic_core(elab, e, AddRevSubgoals); -} - int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); } void open_apply_tactic(lua_State * L) { SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac"); @@ -246,12 +242,6 @@ void initialize_apply_tactic() { return apply_tactic(fn, get_tactic_expr_expr(app_arg(e))); }); - register_tac(get_tactic_rapply_name(), - [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { - check_tactic_expr(app_arg(e), "invalid 'rapply' tactic, invalid argument"); - return rapply_tactic(fn, get_tactic_expr_expr(app_arg(e))); - }); - register_tac(get_tactic_fapply_name(), [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { check_tactic_expr(app_arg(e), "invalid 'fapply' tactic, invalid argument"); diff --git a/src/library/tactic/apply_tactic.h b/src/library/tactic/apply_tactic.h index 88a75b5dd9..6da148b6e9 100644 --- a/src/library/tactic/apply_tactic.h +++ b/src/library/tactic/apply_tactic.h @@ -9,7 +9,6 @@ Author: Leonardo de Moura #include "library/tactic/elaborate.h" namespace lean { tactic apply_tactic(elaborate_fn const & fn, expr const & e); -tactic rapply_tactic(elaborate_fn const & fn, expr const & e); tactic fapply_tactic(elaborate_fn const & fn, expr const & e); tactic eassumption_tactic(); void open_apply_tactic(lua_State * L); diff --git a/tests/lean/run/intros.lean b/tests/lean/run/intros.lean index 9c977cbc9b..2f62056c65 100644 --- a/tests/lean/run/intros.lean +++ b/tests/lean/run/intros.lean @@ -5,7 +5,7 @@ theorem tst1 (a b : Prop) : a → b → b := by intro Ha; intro Hb; apply Hb theorem tst2 (a b : Prop) : a → b → a ∧ b := -by intro Ha; intro Hb; rapply and.intro; apply Hb; apply Ha +by intro Ha; intro Hb; apply and.intro; apply Ha; apply Hb theorem tst3 (a b : Prop) : a → b → a ∧ b := begin @@ -19,9 +19,9 @@ end theorem tst4 (a b : Prop) : a → b → a ∧ b := begin intros [Ha, Hb], - rapply and.intro, + apply and.intro, + apply Ha, apply Hb, - apply Ha end theorem tst5 (a b : Prop) : a → b → a ∧ b := diff --git a/tests/lean/run/tactic10.lean b/tests/lean/run/tactic10.lean index fa0daaf29b..3a782c6967 100644 --- a/tests/lean/run/tactic10.lean +++ b/tests/lean/run/tactic10.lean @@ -1,10 +1,10 @@ import logic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a -:= by rapply iff.intro; - intro Ha; - apply (iff.elim_left H Ha); +:= by apply iff.intro; intro Hb; - apply (iff.elim_right H Hb) + apply (iff.elim_right H Hb); + intro Ha; + apply (iff.elim_left H Ha) check tst diff --git a/tests/lean/run/tactic11.lean b/tests/lean/run/tactic11.lean index 32e9e1bedf..f5c0df5985 100644 --- a/tests/lean/run/tactic11.lean +++ b/tests/lean/run/tactic11.lean @@ -3,19 +3,19 @@ import logic theorem tst (a b : Prop) (H : a ↔ b) : b ↔ a := have H1 [visible] : a → b, -- We need to mark H1 as fact, otherwise it is not visible by tactics from iff.elim_left H, - by rapply iff.intro; - intro Ha; - apply (H1 Ha); + by apply iff.intro; intro Hb; - apply (iff.elim_right H Hb) + apply (iff.elim_right H Hb); + intro Ha; + apply (H1 Ha) theorem tst2 (a b : Prop) (H : a ↔ b) : b ↔ a := have H1 [visible] : a → b, from iff.elim_left H, begin - rapply iff.intro, - intro Ha; - apply (H1 Ha), + apply iff.intro, intro Hb; - apply (iff.elim_right H Hb) + apply (iff.elim_right H Hb), + intro Ha; + apply (H1 Ha) end