From c5f92f08b8885580bbbe5d980dc6f40f396f54cc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jun 2016 14:37:54 -0700 Subject: [PATCH] feat(library/tactic): add 'assert' tactic Remark: the new assert tactic does have the problem described in issue #621 --- library/init/meta/tactic.lean | 2 ++ src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/assert_tactic.cpp | 43 ++++++++++++++++++++++++++++ src/library/tactic/assert_tactic.h | 11 +++++++ src/library/tactic/init_module.cpp | 3 ++ tests/lean/run/assert_tac1.lean | 10 +++++++ 6 files changed, 70 insertions(+), 1 deletion(-) create mode 100644 src/library/tactic/assert_tactic.cpp create mode 100644 src/library/tactic/assert_tactic.h create mode 100644 tests/lean/run/assert_tac1.lean diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean index 28af54f441..926f3c48ef 100644 --- a/library/init/meta/tactic.lean +++ b/library/init/meta/tactic.lean @@ -110,6 +110,8 @@ meta_constant defeq_simp : expr → tactic expr /- Change the target of the main goal. The input expression must be definitionally equal to the current target. -/ meta_constant change : expr → tactic unit +/- (assert H T), adds a new goal for T, and the hypothesis (H : T := ?M) in the current goal -/ +meta_constant assert : name → expr → tactic unit open list nat meta_definition intros : tactic unit := diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index 8877e4ca44..cc445844f4 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -1,4 +1,4 @@ add_library(tactic OBJECT tactic_state.cpp intro_tactic.cpp revert_tactic.cpp rename_tactic.cpp clear_tactic.cpp app_builder_tactics.cpp subst_tactic.cpp exact_tactic.cpp - change_tactic.cpp elaborate.cpp init_module.cpp) + change_tactic.cpp assert_tactic.cpp elaborate.cpp init_module.cpp) diff --git a/src/library/tactic/assert_tactic.cpp b/src/library/tactic/assert_tactic.cpp new file mode 100644 index 0000000000..0fc1a588cb --- /dev/null +++ b/src/library/tactic/assert_tactic.cpp @@ -0,0 +1,43 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#include "library/lazy_abstraction.h" +#include "library/vm/vm_name.h" +#include "library/vm/vm_expr.h" +#include "library/tactic/tactic_state.h" + +namespace lean { +vm_obj assert_core(name const & n, expr const & e, tactic_state const & s) { + optional g = s.get_main_goal_decl(); + if (!g) return mk_no_goals_exception(s); + metavar_context mctx = s.mctx(); + type_context ctx = mk_type_context_for(s, mctx); + if (!is_sort(ctx.whnf(ctx.infer(e)))) { + format msg("invalid assert tactic, expression is not a type"); + msg += pp_indented_expr(s, e); + return mk_tactic_exception(msg, s); + } + local_context lctx = g->get_context(); + expr new_M_1 = mctx.mk_metavar_decl(lctx, e); + expr l = lctx.mk_local_decl(n, e, new_M_1); + expr new_M_2 = mctx.mk_metavar_decl(lctx, g->get_type()); + expr new_val = mk_let(n, e, new_M_1, mk_lazy_abstraction(new_M_2, mlocal_name(l))); + mctx.assign(head(s.goals()), new_val); + list new_gs = cons(new_M_1, cons(new_M_2, tail(s.goals()))); + return mk_tactic_success(set_mctx_goals(s, mctx, new_gs)); +} + +vm_obj tactic_assert(vm_obj const & n, vm_obj const & e, vm_obj const & s) { + return assert_core(to_name(n), to_expr(e), to_tactic_state(s)); +} + +void initialize_assert_tactic() { + DECLARE_VM_BUILTIN(name({"tactic", "assert"}), tactic_assert); +} + +void finalize_assert_tactic() { +} +} diff --git a/src/library/tactic/assert_tactic.h b/src/library/tactic/assert_tactic.h new file mode 100644 index 0000000000..007130940d --- /dev/null +++ b/src/library/tactic/assert_tactic.h @@ -0,0 +1,11 @@ +/* +Copyright (c) 2016 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Leonardo de Moura +*/ +#pragma once +namespace lean { +void initialize_assert_tactic(); +void finalize_assert_tactic(); +} diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 77b806926a..b9e48c5d4c 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -13,6 +13,7 @@ Author: Leonardo de Moura #include "library/tactic/subst_tactic.h" #include "library/tactic/exact_tactic.h" #include "library/tactic/change_tactic.h" +#include "library/tactic/assert_tactic.h" #include "library/tactic/elaborate.h" namespace lean { @@ -26,10 +27,12 @@ void initialize_tactic_module() { initialize_subst_tactic(); initialize_exact_tactic(); initialize_change_tactic(); + initialize_assert_tactic(); initialize_elaborate(); } void finalize_tactic_module() { finalize_elaborate(); + finalize_assert_tactic(); finalize_change_tactic(); finalize_exact_tactic(); finalize_subst_tactic(); diff --git a/tests/lean/run/assert_tac1.lean b/tests/lean/run/assert_tac1.lean new file mode 100644 index 0000000000..f53d26d5c2 --- /dev/null +++ b/tests/lean/run/assert_tac1.lean @@ -0,0 +1,10 @@ +open tactic + +definition tst1 (a : nat) : a = a := +by do + assert "x" (expr.const "nat" []), + trace_state, + a ← get_local "a", + exact a, + x ← get_local "x", + mk_app ("eq" <.> "refl") [x] >>= exact