From b9e3c474c93ec546394a4d05252139e4e93996db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Mar 2015 17:42:34 -0700 Subject: [PATCH] feat(library/tactic): add all_goals tactic closes #501 --- hott/init/tactic.hlean | 2 +- library/init/tactic.lean | 1 + src/emacs/lean-syntax.el | 2 +- src/library/constants.cpp | 4 ++++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/tactic/expr_to_tactic.cpp | 2 ++ src/library/tactic/tactic.cpp | 12 ++++++++++++ src/library/tactic/tactic.h | 4 +++- tests/lean/run/all_goals.lean | 12 ++++++++++++ 10 files changed, 38 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/all_goals.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 7fd2d9c91..508574ded 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -10,7 +10,6 @@ expression. We should view 'tactic' as automation that when execute produces a term. tactic.builtin is just a "dummy" for creating the definitions that are actually implemented in C++ -/ - prelude import init.datatypes init.reserved_notation init.num @@ -33,6 +32,7 @@ opaque definition at_most (t : tactic) (k : num) : tactic := builtin opaque definition discard (t : tactic) (k : num) : tactic := builtin opaque definition focus_at (t : tactic) (i : num) : tactic := builtin opaque definition try_for (t : tactic) (ms : num) : tactic := builtin +opaque definition all_goals (t : tactic) : tactic := builtin opaque definition now : tactic := builtin opaque definition assumption : tactic := builtin opaque definition eassumption : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index e30ed5fc5..bf5195651 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -32,6 +32,7 @@ opaque definition at_most (t : tactic) (k : num) : tactic := builtin opaque definition discard (t : tactic) (k : num) : tactic := builtin opaque definition focus_at (t : tactic) (i : num) : tactic := builtin opaque definition try_for (t : tactic) (ms : num) : tactic := builtin +opaque definition all_goals (t : tactic) : tactic := builtin opaque definition now : tactic := builtin opaque definition assumption : tactic := builtin opaque definition eassumption : tactic := builtin diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 61db99cf6..652e0d22b 100644 --- a/src/emacs/lean-syntax.el +++ b/src/emacs/lean-syntax.el @@ -130,7 +130,7 @@ (,(rx (not (any "\.")) word-start (group (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" - "apply" "fapply" "rename" "intro" "intros" + "apply" "fapply" "rename" "intro" "intros" "all_goals" "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp" "unfold" "change")) word-end) diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 74d6051a7..2b123c462 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -59,6 +59,7 @@ name const * g_string = nullptr; name const * g_string_empty = nullptr; name const * g_string_str = nullptr; name const * g_tactic = nullptr; +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; @@ -171,6 +172,7 @@ void initialize_constants() { g_string_empty = new name{"string", "empty"}; g_string_str = new name{"string", "str"}; g_tactic = new name{"tactic"}; + g_tactic_all_goals = new name{"tactic", "all_goals"}; g_tactic_apply = new name{"tactic", "apply"}; g_tactic_assert_hypothesis = new name{"tactic", "assert_hypothesis"}; g_tactic_fapply = new name{"tactic", "fapply"}; @@ -284,6 +286,7 @@ void finalize_constants() { delete g_string_empty; delete g_string_str; delete g_tactic; + delete g_tactic_all_goals; delete g_tactic_apply; delete g_tactic_assert_hypothesis; delete g_tactic_fapply; @@ -396,6 +399,7 @@ name const & get_string_name() { return *g_string; } name const & get_string_empty_name() { return *g_string_empty; } name const & get_string_str_name() { return *g_string_str; } name const & get_tactic_name() { return *g_tactic; } +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; } diff --git a/src/library/constants.h b/src/library/constants.h index cc706c778..506749bfa 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -61,6 +61,7 @@ name const & get_string_name(); name const & get_string_empty_name(); name const & get_string_str_name(); name const & get_tactic_name(); +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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index ccbe1cb8d..3331e2fce 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -54,6 +54,7 @@ string string.empty string.str tactic +tactic.all_goals tactic.apply tactic.assert_hypothesis tactic.fapply diff --git a/src/library/tactic/expr_to_tactic.cpp b/src/library/tactic/expr_to_tactic.cpp index 8df152ddc..8f33bfb70 100644 --- a/src/library/tactic/expr_to_tactic.cpp +++ b/src/library/tactic/expr_to_tactic.cpp @@ -368,6 +368,8 @@ void initialize_expr_to_tactic() { [](tactic const & t1, tactic const & t2) { return orelse(t1, t2); }); register_unary_tac(get_tactic_repeat_name(), [](tactic const & t1) { return repeat(t1); }); + register_unary_tac(get_tactic_all_goals_name(), + [](tactic const & t1) { return all_goals(t1); }); register_unary_num_tac(get_tactic_at_most_name(), [](tactic const & t, unsigned k) { return take(t, k); }); register_unary_num_tac(get_tactic_discard_name(), diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp index 2bb4edb04..8f704f1e7 100644 --- a/src/library/tactic/tactic.cpp +++ b/src/library/tactic/tactic.cpp @@ -289,6 +289,18 @@ tactic focus(tactic const & t, unsigned i) { }); } +tactic all_goals(tactic const & t) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq { + tactic r = id_tactic(); + unsigned i = length(s.get_goals()); + while (i > 0) { + --i; + r = then(r, focus(t, i)); + } + return r(env, ios, s); + }); +} + DECL_UDATA(proof_state_seq) static const struct luaL_Reg proof_state_seq_m[] = { {"__gc", proof_state_seq_gc}, // never throws diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index a6aebefa6..d8e2fe945 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -146,9 +146,11 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_ The tactic fails if the input state does have at least i goals. */ tactic focus(tactic const & t, unsigned i); -inline tactic focus(tactic const & t) { return focus(t, 1); } +inline tactic focus(tactic const & t) { return focus(t, 0); } /** \brief Return a tactic that applies beta-reduction. */ tactic beta_tactic(); +/** \brief Apply \c t to all goals in the proof state */ +tactic all_goals(tactic const & t); UDATA_DEFS_CORE(proof_state_seq) UDATA_DEFS_CORE(tactic); diff --git a/tests/lean/run/all_goals.lean b/tests/lean/run/all_goals.lean new file mode 100644 index 000000000..54b9df9be --- /dev/null +++ b/tests/lean/run/all_goals.lean @@ -0,0 +1,12 @@ +import data.nat +open nat + +attribute nat.add [unfold-c 2] +attribute nat.rec_on [unfold-c 2] + +example (a b c : nat) : a + 0 = 0 + a ∧ b + 0 = 0 + b := +begin + apply and.intro, + all_goals esimp{of_num}, + all_goals (state; rewrite zero_add) +end