max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/tactic/assert_tactic): add 'pose' tactic

Browse source
This commit is contained in:
Leonardo de Moura 2016-06-18 14:28:28 -07:00
parent 9371aa0e99
commit dc180dcd15
2 changed files with 30 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/meta/tactic.lean
View file

@ -126,6 +126,8 @@ meta_constant defeq_simp : expr → tactic expr
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
/- (pose H T P), adds the hypothesis (H : T) in the current goal if P has type T. -/
meta_constant pose : name → expr → expr → tactic unit
/- rotate goals to the left -/
meta_constant rotate_left : nat → tactic unit
meta_constant get_goals : tactic (list expr)

29
src/library/tactic/assert_tactic.cpp
View file

@ -34,8 +34,35 @@ 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));
}
vm_obj pose(name const & n, expr const & e, expr const & pr, tactic_state const & s) {
optional<metavar_decl> 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);
expr pr_type = ctx.infer(pr);
if (!ctx.is_def_eq(e, pr_type)) {
format msg("invalid pose tactic, proof has type");
msg += pp_indented_expr(s, pr_type);
msg += line() + format("but is expected to have type");
msg += pp_indented_expr(s, e);
return mk_tactic_exception(msg, s);
}
local_context lctx = g->get_context();
expr l = lctx.mk_local_decl(n, e);
expr new_M = mctx.mk_metavar_decl(lctx, g->get_type());
expr new_val = mk_app(mk_lambda(n, e, mk_lazy_abstraction(new_M, mlocal_name(l))), pr);
mctx.assign(head(s.goals()), new_val);
list<expr> new_gs = cons(new_M, tail(s.goals()));
return mk_tactic_success(set_mctx_goals(s, mctx, new_gs));
}
vm_obj tactic_pose(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
return pose(to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
}
void initialize_assert_tactic() {
DECLARE_VM_BUILTIN(name({"tactic", "assert"}), tactic_assert);
DECLARE_VM_BUILTIN(name({"tactic", "assert"}), tactic_assert);
DECLARE_VM_BUILTIN(name({"tactic", "pose"}), tactic_pose);
}
void finalize_assert_tactic() {