From d4e49a84347a3b863391900ee77e72ef02622ae3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2015 16:28:39 -0800 Subject: [PATCH] feat(library/tactic/intros_tactic): intro without argument should introduce a single variable see #695 --- hott/init/tactic.hlean | 2 +- library/init/tactic.lean | 2 +- src/library/tactic/intros_tactic.cpp | 36 ++++++++++++++++++++-------- src/library/tactic/intros_tactic.h | 2 +- tests/lean/run/intro0.lean | 5 ++++ 5 files changed, 34 insertions(+), 13 deletions(-) create mode 100644 tests/lean/run/intro0.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 33ec92cda..ad7ae41cf 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -74,7 +74,7 @@ definition apply (e : expr) : tactic := builtin definition eapply (e : expr) : tactic := builtin definition fapply (e : expr) : tactic := builtin definition rename (a b : identifier) : tactic := builtin -definition intro (e : identifier_list) : tactic := builtin +definition intro (e : opt_identifier_list) : tactic := builtin definition generalize_tac (e : expr) (id : identifier) : tactic := builtin definition clear (e : identifier_list) : tactic := builtin definition revert (e : identifier_list) : tactic := builtin diff --git a/library/init/tactic.lean b/library/init/tactic.lean index 3d7147eff..bc459a621 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -75,7 +75,7 @@ definition apply (e : expr) : tactic := builtin definition eapply (e : expr) : tactic := builtin definition fapply (e : expr) : tactic := builtin definition rename (a b : identifier) : tactic := builtin -definition intro (e : identifier_list) : tactic := builtin +definition intro (e : opt_identifier_list) : tactic := builtin definition generalize_tac (e : expr) (id : identifier) : tactic := builtin definition clear (e : identifier_list) : tactic := builtin definition revert (e : identifier_list) : tactic := builtin diff --git a/src/library/tactic/intros_tactic.cpp b/src/library/tactic/intros_tactic.cpp index 132bfcf95..a102b1f4e 100644 --- a/src/library/tactic/intros_tactic.cpp +++ b/src/library/tactic/intros_tactic.cpp @@ -11,7 +11,7 @@ Author: Leonardo de Moura #include "library/tactic/expr_to_tactic.h" namespace lean { -tactic intros_tactic(list _ns) { +static tactic intro_intros_tactic(list _ns, bool is_intros) { auto fn = [=](environment const & env, io_state const &, proof_state const & s) { list ns = _ns; goals const & gs = s.get_goals(); @@ -24,10 +24,12 @@ tactic intros_tactic(list _ns) { auto tc = mk_type_checker(env, ngen.mk_child()); expr t = g.get_type(); expr m = g.get_meta(); - bool gen_names = empty(ns); + bool gen_names = is_intros && empty(ns); + bool gen_one_name = !is_intros && empty(ns); + bool first = true; try { while (true) { - if (!gen_names && is_nil(ns)) + if (!gen_names && (!gen_one_name || !first) && is_nil(ns)) break; if (!is_pi(t)) { if (!is_nil(ns)) { @@ -49,6 +51,7 @@ tactic intros_tactic(list _ns) { expr new_local = mk_local(ngen.next(), new_name, binding_domain(t), binding_info(t)); t = instantiate(binding_body(t), new_local); m = mk_app(m, new_local); + first = false; } goal new_g(m, t); return some(proof_state(s, goals(new_g, tail(gs)), ngen)); @@ -59,14 +62,27 @@ tactic intros_tactic(list _ns) { return tactic01(fn); } +tactic intro_tactic(list const & ns) { + return intro_intros_tactic(ns, false); +} + +tactic intros_tactic(list const & ns) { + return intro_intros_tactic(ns, true); +} + void initialize_intros_tactic() { - auto fn = [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { - buffer ns; - get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intro' tactic, arguments must be identifiers"); - return intros_tactic(to_list(ns.begin(), ns.end())); - }; - register_tac(get_tactic_intro_name(), fn); - register_tac(get_tactic_intros_name(), fn); + register_tac(get_tactic_intro_name(), + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer ns; + get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intro' tactic, arguments must be identifiers"); + return intro_tactic(to_list(ns.begin(), ns.end())); + }); + register_tac(get_tactic_intros_name(), + [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) { + buffer ns; + get_tactic_id_list_elements(app_arg(e), ns, "invalid 'intros' tactic, arguments must be identifiers"); + return intros_tactic(to_list(ns.begin(), ns.end())); + }); } void finalize_intros_tactic() { diff --git a/src/library/tactic/intros_tactic.h b/src/library/tactic/intros_tactic.h index 83d5da17b..a5d34f578 100644 --- a/src/library/tactic/intros_tactic.h +++ b/src/library/tactic/intros_tactic.h @@ -7,7 +7,7 @@ Author: Leonardo de Moura #pragma once #include "library/tactic/tactic.h" namespace lean { -tactic intros_tactic(list ns); +tactic intros_tactic(list const & ns); void initialize_intros_tactic(); void finalize_intros_tactic(); } diff --git a/tests/lean/run/intro0.lean b/tests/lean/run/intro0.lean new file mode 100644 index 000000000..ad78ca670 --- /dev/null +++ b/tests/lean/run/intro0.lean @@ -0,0 +1,5 @@ +example (a b : nat) : a = b → a = b := +begin + intro, + assumption +end