michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/tactic): add 'exact' tactic

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-07-02 18:32:44 -07:00
parent 37b5b7c4c2
commit 60c637fb9d
6 changed files with 61 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/standard/tactic.lean
View file

@ -27,6 +27,7 @@ definition id : tactic := tactic_value
definition beta : tactic := tactic_value
definition apply {B : Type} (b : B) : tactic := tactic_value
definition unfold {B : Type} (b : B) : tactic := tactic_value
definition exact {B : Type} (b : B) : tactic := tactic_value
definition trace (s : string) : tactic := tactic_value
infixl `;`:200 := and_then
infixl `|`:100 := or_else

14
src/library/tactic/apply_tactic.cpp
View file

@ -60,18 +60,6 @@ void collect_simple_meta(expr const & e, buffer<expr> & metas) {
});
}
/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
void check_has_no_local(expr const & v, expr const & e) {
if (has_local(v)) {
for_each(v, [&](expr const & l, unsigned) {
if (is_local(l))
throw tactic_exception(e, sstream() << "apply tactic contains reference to local '" << local_pp_name(l)
<< "' which is not marked as [fact], so it is not visible to tactics");
return has_local(l);
});
}
}
tactic apply_tactic(expr const & _e) {
return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
goals const & gs = s.get_goals();
@ -100,7 +88,7 @@ tactic apply_tactic(expr const & _e) {
type_checker tc(env, new_ngen.mk_child());
expr new_e = subst.instantiate(e);
expr new_p = g.abstract(new_e);
check_has_no_local(new_p, _e);
check_has_no_local(new_p, _e, "apply");
substitution new_subst = subst.assign(g.get_name(), new_p);
buffer<expr> metas;
collect_simple_meta(new_e, metas);

3
src/library/tactic/expr_to_tactic.cpp
View file

@ -110,6 +110,9 @@ static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr c
static register_tac reg_apply(name(g_tac, "apply"), [](type_checker &, expr const & e, pos_info_provider const *) {
return apply_tactic(app_arg(e));
});
static register_tac reg_exact(name(g_tac, "exact"), [](type_checker &, expr const & e, pos_info_provider const *) {
return exact_tactic(app_arg(e));
});
static register_tac reg_unfold(name(g_tac, "unfold"), [](type_checker &, expr const & e, pos_info_provider const *) {
expr id = get_app_fn(app_arg(e));
if (!is_constant(id))

35
src/library/tactic/tactic.cpp
View file

@ -13,12 +13,27 @@ Author: Leonardo de Moura
#include "util/lazy_list_fn.h"
#include "util/list_fn.h"
#include "kernel/instantiate.h"
#include "kernel/type_checker.h"
#include "kernel/for_each_fn.h"
#include "kernel/replace_visitor.h"
#include "library/kernel_bindings.h"
#include "library/tactic/tactic.h"
#include "library/io_state_stream.h"
namespace lean {
/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
void check_has_no_local(expr const & v, expr const & e, char const * tac_name) {
if (has_local(v)) {
for_each(v, [&](expr const & l, unsigned) {
if (is_local(l))
throw tactic_exception(e, sstream() << "tactic '" << tac_name << "' contains reference to local '" << local_pp_name(l)
<< "' which is not visible by this tactic "
<< "possible causes: it was not marked as [fact]; it was destructued");
return has_local(l);
});
}
}
tactic_exception::tactic_exception(expr const & e, char const * msg):exception(msg), m_expr(e) {}
tactic_exception::tactic_exception(expr const & e, sstream const & strm):exception(strm), m_expr(e) {}
@ -205,6 +220,26 @@ tactic assumption_tactic() {
});
}
tactic exact_tactic(expr const & _e) {
return tactic01([=](environment const & env, io_state const &, proof_state const & s) {
type_checker tc(env);
substitution subst = s.get_subst();
goals const & gs = s.get_goals();
goal const & g = head(gs);
expr e = subst.instantiate(_e);
expr e_t = subst.instantiate(tc.infer(e));
expr t = subst.instantiate(g.get_type());
if (tc.is_def_eq(e_t, t) && !tc.next_cnstr()) {
expr new_p = g.abstract(e);
check_has_no_local(new_p, _e, "exact");
substitution new_subst = subst.assign(g.get_name(), new_p);
return some(proof_state(s, tail(gs), new_subst));
} else {
return none_proof_state();
}
});
}
tactic beta_tactic() {
return tactic01([=](environment const &, io_state const &, proof_state const & s) -> optional<proof_state> {
bool reduced = false;

5
src/library/tactic/tactic.h
View file

@ -14,6 +14,9 @@ Author: Leonardo de Moura
#include "library/tactic/proof_state.h"
namespace lean {
/** \brief Throw an exception is \c v contains local constants, \c e is only used for position information. */
void check_has_no_local(expr const & v, expr const & e, char const * tac_name);
class tactic_exception : public exception {
expr m_expr;
public:
@ -132,6 +135,8 @@ inline tactic when(proof_state_pred p, tactic const & t) { return cond(p, t, id_
*/
tactic focus(tactic const & t, unsigned i);
inline tactic focus(tactic const & t) { return focus(t, 1); }
/** \brief Solve first goal iff it is definitionally equal to \c e */
tactic exact_tactic(expr const & e);
/** \brief Return a tactic that unfolds the definition named \c n. */
tactic unfold_tactic(name const & n);
/** \brief Return a tactic that unfolds all (non-opaque) definitions. */

16
tests/lean/run/tactic12.lean Normal file
View file

@ -0,0 +1,16 @@
import standard
using tactic
theorem tst (a b : Bool) (H : ¬ a ∨ ¬ b) (Hb : b) : ¬ a ∧ b
:= by apply and_intro;
apply not_intro;
exact
(assume Ha, or_elim H
(assume Hna, absurd Ha Hna)
(assume Hnb, absurd Hb Hnb));
assumption