From d2c7b5c31928c98f545b16420d37842c43b4ae9a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 28 Apr 2015 17:20:39 -0700 Subject: [PATCH] feat(library/tactic): add 'let' tactic closes #555 --- hott/init/tactic.hlean | 2 + library/init/tactic.lean | 2 + src/frontends/lean/builtin_tactics.cpp | 10 +++ src/library/constants.cpp | 4 ++ src/library/constants.h | 1 + src/library/constants.txt | 1 + src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/init_module.cpp | 3 + src/library/tactic/let_tactic.cpp | 62 +++++++++++++++++++ src/library/tactic/let_tactic.h | 14 +++++ .../lean/interactive/alias.input.expected.out | 2 + tests/lean/run/let_tac.lean | 18 ++++++ 12 files changed, 120 insertions(+), 1 deletion(-) create mode 100644 src/library/tactic/let_tactic.cpp create mode 100644 src/library/tactic/let_tactic.h create mode 100644 tests/lean/run/let_tac.lean diff --git a/hott/init/tactic.hlean b/hott/init/tactic.hlean index 09f5139a9..2c1110164 100644 --- a/hott/init/tactic.hlean +++ b/hott/init/tactic.hlean @@ -96,6 +96,8 @@ opaque definition change (e : expr) : tactic := builtin opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin +opaque definition lettac (id : identifier) (e : expr) : tactic := builtin + definition try (t : tactic) : tactic := or_else t id definition repeat1 (t : tactic) : tactic := and_then t (repeat t) definition focus (t : tactic) : tactic := focus_at t 0 diff --git a/library/init/tactic.lean b/library/init/tactic.lean index b86f6ca6d..ec6e5dd3f 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -96,6 +96,8 @@ opaque definition change (e : expr) : tactic := builtin opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin +opaque definition lettac (id : identifier) (e : expr) : tactic := builtin + definition try (t : tactic) : tactic := or_else t id definition repeat1 (t : tactic) : tactic := and_then t (repeat t) definition focus (t : tactic) : tactic := focus_at t 0 diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp index 0b6ee54d9..c43e8b1b2 100644 --- a/src/frontends/lean/builtin_tactics.cpp +++ b/src/frontends/lean/builtin_tactics.cpp @@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include "library/tactic/let_tactic.h" +#include "frontends/lean/tokens.h" #include "frontends/lean/parser.h" #include "frontends/lean/parse_rewrite_tactic.h" @@ -29,6 +31,13 @@ static expr parse_rparen(parser &, unsigned, expr const * args, pos_info const & return args[0]; } +static expr parse_let_tactic(parser & p, unsigned, expr const *, pos_info const & pos) { + name id = p.check_atomic_id_next("invalid 'let' tactic, identifier expected"); + p.check_token_next(get_assign_tk(), "invalid 'let' tactic, ':=' expected"); + expr value = p.parse_expr(); + return p.save_pos(mk_let_tactic_expr(id, value), pos); +} + parse_table init_tactic_nud_table() { action Expr(mk_expr_action()); expr x0 = mk_var(0); @@ -38,6 +47,7 @@ parse_table init_tactic_nud_table() { r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0); r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0); r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0); + r = r.add({transition("let", mk_ext_action(parse_let_tactic))}, x0); return r; } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index fe744fca3..76ad7d3d3 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -95,6 +95,7 @@ name const * g_tactic_generalize = nullptr; name const * g_tactic_generalizes = nullptr; name const * g_tactic_id = nullptr; name const * g_tactic_interleave = nullptr; +name const * g_tactic_lettac = nullptr; name const * g_tactic_now = nullptr; name const * g_tactic_opt_expr_list = nullptr; name const * g_tactic_or_else = nullptr; @@ -213,6 +214,7 @@ void initialize_constants() { g_tactic_generalizes = new name{"tactic", "generalizes"}; g_tactic_id = new name{"tactic", "id"}; g_tactic_interleave = new name{"tactic", "interleave"}; + g_tactic_lettac = new name{"tactic", "lettac"}; g_tactic_now = new name{"tactic", "now"}; g_tactic_opt_expr_list = new name{"tactic", "opt_expr_list"}; g_tactic_or_else = new name{"tactic", "or_else"}; @@ -332,6 +334,7 @@ void finalize_constants() { delete g_tactic_generalizes; delete g_tactic_id; delete g_tactic_interleave; + delete g_tactic_lettac; delete g_tactic_now; delete g_tactic_opt_expr_list; delete g_tactic_or_else; @@ -450,6 +453,7 @@ name const & get_tactic_generalize_name() { return *g_tactic_generalize; } name const & get_tactic_generalizes_name() { return *g_tactic_generalizes; } name const & get_tactic_id_name() { return *g_tactic_id; } name const & get_tactic_interleave_name() { return *g_tactic_interleave; } +name const & get_tactic_lettac_name() { return *g_tactic_lettac; } name const & get_tactic_now_name() { return *g_tactic_now; } name const & get_tactic_opt_expr_list_name() { return *g_tactic_opt_expr_list; } name const & get_tactic_or_else_name() { return *g_tactic_or_else; } diff --git a/src/library/constants.h b/src/library/constants.h index 340229cd1..4709ad49d 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -97,6 +97,7 @@ name const & get_tactic_generalize_name(); name const & get_tactic_generalizes_name(); name const & get_tactic_id_name(); name const & get_tactic_interleave_name(); +name const & get_tactic_lettac_name(); name const & get_tactic_now_name(); name const & get_tactic_opt_expr_list_name(); name const & get_tactic_or_else_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index d95a84a95..bb0be82c8 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -90,6 +90,7 @@ tactic.generalize tactic.generalizes tactic.id tactic.interleave +tactic.lettac tactic.now tactic.opt_expr_list tactic.or_else diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index bc846ed2b..18a024c23 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -4,6 +4,6 @@ exact_tactic.cpp generalize_tactic.cpp inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp -change_tactic.cpp check_expr_tactic.cpp) +change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp) target_link_libraries(tactic ${LEAN_LIBS}) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 3f27b5737..b725f1484 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -22,6 +22,7 @@ Author: Leonardo de Moura #include "library/tactic/rewrite_tactic.h" #include "library/tactic/change_tactic.h" #include "library/tactic/check_expr_tactic.h" +#include "library/tactic/let_tactic.h" namespace lean { void initialize_tactic_module() { @@ -43,9 +44,11 @@ void initialize_tactic_module() { initialize_rewrite_tactic(); initialize_change_tactic(); initialize_check_expr_tactic(); + initialize_let_tactic(); } void finalize_tactic_module() { + finalize_let_tactic(); finalize_check_expr_tactic(); finalize_change_tactic(); finalize_rewrite_tactic(); diff --git a/src/library/tactic/let_tactic.cpp b/src/library/tactic/let_tactic.cpp new file mode 100644 index 000000000..8fb457cfe --- /dev/null +++ b/src/library/tactic/let_tactic.cpp @@ -0,0 +1,62 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "kernel/abstract.h" +#include "library/constants.h" +#include "library/reducible.h" +#include "library/tactic/tactic.h" +#include "library/tactic/elaborate.h" +#include "library/tactic/expr_to_tactic.h" + +namespace lean { +expr mk_let_tactic_expr(name const & id, expr const & e) { + return mk_app(mk_constant(get_tactic_lettac_name()), + mk_constant(id), e); +} + +tactic let_tactic(elaborate_fn const & elab, name const & id, expr const & e) { + return tactic01([=](environment const & env, io_state const &, proof_state const & s) { + proof_state new_s = s; + goals const & gs = new_s.get_goals(); + if (!gs) { + throw_no_goal_if_enabled(s); + return none_proof_state(); + } + goal const & g = head(gs); + name_generator ngen = s.get_ngen(); + bool report_unassigned = true; + auto ecs = elab(g, ngen.mk_child(), e, none_expr(), report_unassigned); + if (ecs.second) + throw_tactic_exception_if_enabled(s, "invalid 'let' tactic, fail to resolve generated constraints"); + expr new_e = ecs.first; + auto tc = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque()); + expr new_e_type = tc->infer(new_e).first; + expr new_local = mk_local(ngen.next(), id, new_e_type, binder_info()); + buffer hyps; + g.get_hyps(hyps); + hyps.push_back(new_local); + expr new_mvar = mk_metavar(ngen.next(), Pi(hyps, g.get_type())); + hyps.pop_back(); + expr new_meta_core = mk_app(new_mvar, hyps); + expr new_meta = mk_app(new_meta_core, new_local); + goal new_goal(new_meta, g.get_type()); + substitution new_subst = new_s.get_subst(); + assign(new_subst, g, mk_app(new_meta_core, new_e)); + return some_proof_state(proof_state(s, cons(new_goal, tail(gs)), new_subst, ngen)); + }); +} + +void initialize_let_tactic() { + register_tac(get_tactic_lettac_name(), + [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) { + name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'let' tactic, argument must be an identifier"); + check_tactic_expr(app_arg(e), "invalid 'let' tactic, argument must be an expression"); + return let_tactic(fn, id, get_tactic_expr_expr(app_arg(e))); + }); +} +void finalize_let_tactic() { +} +} diff --git a/src/library/tactic/let_tactic.h b/src/library/tactic/let_tactic.h new file mode 100644 index 000000000..98d14c8c1 --- /dev/null +++ b/src/library/tactic/let_tactic.h @@ -0,0 +1,14 @@ +/* +Copyright (c) 2015 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +#include "kernel/expr.h" + +namespace lean { +expr mk_let_tactic_expr(name const & id, expr const & e); +void initialize_let_tactic(); +void finalize_let_tactic(); +} diff --git a/tests/lean/interactive/alias.input.expected.out b/tests/lean/interactive/alias.input.expected.out index 7f6fa7ecd..65e026a2d 100644 --- a/tests/lean/interactive/alias.input.expected.out +++ b/tests/lean/interactive/alias.input.expected.out @@ -6,6 +6,7 @@ bool.bor_tt|∀ (a : bool), eq (bool.bor a bool.tt) bool.tt bool.band_tt|∀ (a : bool), eq (bool.band a bool.tt) a bool.tt|bool +tactic.lettac|tactic.identifier → tactic.expr → tactic bool.absurd_of_eq_ff_of_eq_tt|eq ?a bool.ff → eq ?a bool.tt → ?B bool.eq_tt_of_ne_ff|ne ?a bool.ff → eq ?a bool.tt bool.tt_band|∀ (a : bool), eq (bool.band bool.tt a) a @@ -22,6 +23,7 @@ tt_bor|∀ (a : bool), eq (bor tt a) tt tt_band|∀ (a : bool), eq (band tt a) a bor_tt|∀ (a : bool), eq (bor a tt) tt band_tt|∀ (a : bool), eq (band a tt) a +tactic.lettac|tactic.identifier → tactic.expr → tactic absurd_of_eq_ff_of_eq_tt|eq ?a ff → eq ?a tt → ?B eq_tt_of_ne_ff|ne ?a ff → eq ?a tt cond_tt|∀ (t e : ?A), eq (cond tt t e) t diff --git a/tests/lean/run/let_tac.lean b/tests/lean/run/let_tac.lean new file mode 100644 index 000000000..f4c63f817 --- /dev/null +++ b/tests/lean/run/let_tac.lean @@ -0,0 +1,18 @@ +import data.nat + +example (a b : Prop) : a → b → a ∧ b := +begin + intro Ha, intro Hb, + let aux := and.intro Ha Hb, + exact aux +end + +open nat + +example (a b : nat) : a > 0 → b > 0 → a + b + 0 > 0 := +begin + intro agt0, intro bgt0, + let H := add_pos agt0 bgt0, + change a + b > 0, + exact H +end