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

feat(library/init/meta/smt_tactic): add assert/assertv/define/definev/pose/note for smt_tactic

Browse source
This commit is contained in:
Leonardo de Moura 2017-01-03 17:12:00 -08:00
parent b636f03bb9
commit 3adcf30d2f
7 changed files with 167 additions and 70 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
library/init/meta/smt_tactic.lean
View file

@ -83,8 +83,13 @@ meta instance : alternative smt_tactic :=
map := @fmap _ _}
namespace smt_tactic
meta constant intros : smt_tactic unit
meta constant close : smt_tactic unit
/-- (intros_core fresh_names), if fresh_names is tt, then create fresh names for new hypotheses.
Otherwise, it just uses the given names. -/
meta constant intros_core : bool → smt_tactic unit
meta constant close : smt_tactic unit
meta def intros : smt_tactic unit :=
intros_core tt
meta def try {α : Type} (t : smt_tactic α) : smt_tactic unit :=
λ ss ts, tactic_result.cases_on (t ss ts)
@ -146,6 +151,39 @@ do (s::ss, t::ts) ← get_goals | failed,
(new_ss, new_ts) ← get_goals,
set_goals (new_ss ++ ss) (new_ts ++ ts)
meta def swap : smt_tactic unit :=
do (ss, ts) ← get_goals,
match ss, ts with
| (s₁ :: s₂ :: ss), (t₁ :: t₂ :: ts) := set_goals (s₂ :: s₁ :: ss) (t₂ :: t₁ :: ts)
| _, _ := failed
end
/- (assert h t), adds a new goal for t, and the hypothesis (h : t) in the current goal. -/
meta def assert (h : name) (t : expr) : smt_tactic unit :=
tactic.assert_core h t >> swap >> intros_core ff >> swap >> try close
/- (assertv h t v), adds the hypothesis (h : t) in the current goal if v has type t. -/
meta def assertv (h : name) (t : expr) (v : expr) : smt_tactic unit :=
tactic.assertv_core h t v >> intros_core ff >> return ()
/- (define h t), adds a new goal for t, and the hypothesis (h : t := ?M) in the current goal. -/
meta def define (h : name) (t : expr) : smt_tactic unit :=
tactic.define_core h t >> swap >> intros_core ff >> swap >> try close
/- (definev h t v), adds the hypothesis (h : t := v) in the current goal if v has type t. -/
meta def definev (h : name) (t : expr) (v : expr) : smt_tactic unit :=
tactic.definev_core h t v >> intros_core ff >> return ()
/- Add (h : t := pr) to the current goal -/
meta def pose (h : name) (pr : expr) : smt_tactic unit :=
do t ← tactic.infer_type pr,
definev h t pr
/- Add (h : t) to the current goal, given a proof (pr : t) -/
meta def note (n : name) (pr : expr) : smt_tactic unit :=
do t ← tactic.infer_type pr,
assertv n t pr
meta def destruct (e : expr) : smt_tactic unit :=
smt_tactic.seq (tactic.destruct e) smt_tactic.intros

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

@ -305,14 +305,14 @@ meta constant mk_instance : 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) in the current goal. -/
meta constant assert : name → expr → tactic unit
/- (assertv H T P), adds the hypothesis (H : T) in the current goal if P has type T. -/
meta constant assertv : name → expr → expr → tactic unit
/- (define H T), adds a new goal for T, and the hypothesis (H : T := ?M) in the current goal. -/
meta constant define : name → expr → tactic unit
/- (definev H T P), adds the hypothesis (H : T := P) in the current goal if P has type T. -/
meta constant definev : name → expr → expr → tactic unit
/- (assert_core H T), adds a new goal for T, and change target to (T -> target). -/
meta constant assert_core : name → expr → tactic unit
/- (assertv_core H T P), change target to (T -> target) if P has type T. -/
meta constant assertv_core : name → expr → expr → tactic unit
/- (define_core H T), adds a new goal for T, and change target to (let H : T := ?M in target) in the current goal. -/
meta constant define_core : name → expr → tactic unit
/- (definev_core H T P), change target to (Let H : T := P in target) if P has type T. -/
meta constant definev_core : name → expr → expr → tactic unit
/- rotate goals to the left -/
meta constant rotate_left : nat → tactic unit
meta constant get_goals : tactic (list expr)
@ -393,16 +393,6 @@ get_goals >>= set_goals
meta def step {α : Type u} (t : tactic α) : tactic unit :=
t >>[tactic] cleanup
/- Add (H : T := pr) to the current goal -/
meta def pose (n : name) (pr : expr) : tactic unit :=
do t ← infer_type pr,
definev n t pr
/- Add (H : T) to the current goal, given a proof (pr : T) -/
meta def note (n : name) (pr : expr) : tactic unit :=
do t ← infer_type pr,
assertv n t pr
meta def is_prop (e : expr) : tactic bool :=
do t ← infer_type e,
return (to_bool (t = expr.prop))
@ -537,6 +527,32 @@ do gs ← get_goals,
| e := skip
end
/- (assert h t), adds a new goal for t, and the hypothesis (h : t) in the current goal. -/
meta def assert (h : name) (t : expr) : tactic unit :=
assert_core h t >> swap >> intro h >> swap
/- (assertv h t v), adds the hypothesis (h : t) in the current goal if v has type t. -/
meta def assertv (h : name) (t : expr) (v : expr) : tactic unit :=
assertv_core h t v >> intro h >> return ()
/- (define h t), adds a new goal for t, and the hypothesis (h : t := ?M) in the current goal. -/
meta def define (h : name) (t : expr) : tactic unit :=
define_core h t >> swap >> intro h >> swap
/- (definev h t v), adds the hypothesis (h : t := v) in the current goal if v has type t. -/
meta def definev (h : name) (t : expr) (v : expr) : tactic unit :=
definev_core h t v >> intro h >> return ()
/- Add (h : t := pr) to the current goal -/
meta def pose (h : name) (pr : expr) : tactic unit :=
do t ← infer_type pr,
definev h t pr
/- Add (h : t) to the current goal, given a proof (pr : t) -/
meta def note (n : name) (pr : expr) : tactic unit :=
do t ← infer_type pr,
assertv n t pr
/- Return the number of goals that need to be solved -/
meta def num_goals : tactic nat :=
do gs ← get_goals,

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

@ -8,9 +8,10 @@ Author: Leonardo de Moura
#include "library/vm/vm_name.h"
#include "library/vm/vm_expr.h"
#include "library/tactic/tactic_state.h"
#include "library/tactic/intro_tactic.h"
namespace lean {
vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_state const & s) {
vm_obj assert_define_core(bool is_assert, name const & n, expr const & t, tactic_state const & s) {
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
type_context ctx = mk_type_context_for(s);
@ -24,31 +25,30 @@ vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_stat
local_context lctx = g->get_context();
metavar_context mctx = ctx.mctx();
expr new_M_1 = mctx.mk_metavar_decl(lctx, t);
expr l;
if (is_assert)
l = lctx.mk_local_decl(n, t);
else
l = lctx.mk_local_decl(n, t, new_M_1);
expr new_M_2 = mctx.mk_metavar_decl(lctx, g->get_type());
expr new_val;
if (is_assert)
new_val = mk_app(mk_lambda(n, t, mk_delayed_abstraction(new_M_2, mlocal_name(l))), new_M_1);
else
new_val = mk_let(n, t, new_M_1, mk_delayed_abstraction(new_M_2, mlocal_name(l)));
expr new_M_2, new_val;
if (is_assert) {
expr new_target = mk_pi(n, t, g->get_type());
new_M_2 = mctx.mk_metavar_decl(lctx, new_target);
new_val = mk_app(new_M_2, new_M_1);
} else {
expr new_target = mk_let(n, t, new_M_1, g->get_type());
new_M_2 = mctx.mk_metavar_decl(lctx, new_target);
new_val = new_M_2;
}
mctx.assign(head(s.goals()), new_val);
list<expr> 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 & t, vm_obj const & s) {
return assert_define(true, to_name(n), to_expr(t), to_tactic_state(s));
vm_obj tactic_assert_core(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
return assert_define_core(true, to_name(n), to_expr(t), to_tactic_state(s));
}
vm_obj tactic_define(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
return assert_define(false, to_name(n), to_expr(t), to_tactic_state(s));
vm_obj tactic_define_core(vm_obj const & n, vm_obj const & t, vm_obj const & s) {
return assert_define_core(false, to_name(n), to_expr(t), to_tactic_state(s));
}
vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) {
vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) {
optional<metavar_decl> g = s.get_main_goal_decl();
if (!g) return mk_no_goals_exception(s);
type_context ctx = mk_type_context_for(s);
@ -67,35 +67,43 @@ vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr cons
}
local_context lctx = g->get_context();
metavar_context mctx = ctx.mctx();
expr l;
if (is_assert)
l = lctx.mk_local_decl(n, t);
else
l = lctx.mk_local_decl(n, t, v);
expr new_M = mctx.mk_metavar_decl(lctx, g->get_type());
expr new_val;
if (is_assert)
new_val = mk_app(mk_lambda(n, t, mk_delayed_abstraction(new_M, mlocal_name(l))), v);
else
new_val = mk_let(n, t, v, mk_delayed_abstraction(new_M, mlocal_name(l)));
expr new_M, new_val;
if (is_assert) {
expr new_target = mk_pi(n, t, g->get_type());
new_M = mctx.mk_metavar_decl(lctx, new_target);
new_val = mk_app(new_M, v);
} else {
expr new_target = mk_let(n, t, v, g->get_type());
new_M = mctx.mk_metavar_decl(lctx, new_target);
new_val = new_M;
}
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_assertv(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
return assertv_definev(true, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
vm_obj tactic_assertv_core(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
return assertv_definev_core(true, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
}
vm_obj tactic_definev(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
return assertv_definev(false, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
vm_obj tactic_definev_core(vm_obj const & n, vm_obj const & e, vm_obj const & pr, vm_obj const & s) {
return assertv_definev_core(false, to_name(n), to_expr(e), to_expr(pr), to_tactic_state(s));
}
vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s) {
vm_obj r = assertv_definev_core(is_assert, n, t, v, s);
if (optional<tactic_state> const & s2 = is_tactic_success(r)) {
return intro(n, *s2);
} else {
return r;
}
}
void initialize_assert_tactic() {
DECLARE_VM_BUILTIN(name({"tactic", "assert"}), tactic_assert);
DECLARE_VM_BUILTIN(name({"tactic", "assertv"}), tactic_assertv);
DECLARE_VM_BUILTIN(name({"tactic", "define"}), tactic_define);
DECLARE_VM_BUILTIN(name({"tactic", "definev"}), tactic_definev);
DECLARE_VM_BUILTIN(name({"tactic", "assert_core"}), tactic_assert_core);
DECLARE_VM_BUILTIN(name({"tactic", "assertv_core"}), tactic_assertv_core);
DECLARE_VM_BUILTIN(name({"tactic", "define_core"}), tactic_define_core);
DECLARE_VM_BUILTIN(name({"tactic", "definev_core"}), tactic_definev_core);
}
void finalize_assert_tactic() {

3
src/library/tactic/assert_tactic.h
View file

@ -7,7 +7,8 @@ Author: Leonardo de Moura
#pragma once
#include "library/tactic/tactic_state.h"
namespace lean {
vm_obj assert_define(bool is_assert, name const & n, expr const & t, tactic_state const & s);
vm_obj assert_define_core(bool is_assert, name const & n, expr const & t, tactic_state const & s);
vm_obj assertv_definev_core(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s);
vm_obj assertv_definev(bool is_assert, name const & n, expr const & t, expr const & v, tactic_state const & s);
void initialize_assert_tactic();
void finalize_assert_tactic();

2
src/library/tactic/intro_tactic.h
View file

@ -23,6 +23,8 @@ optional<expr> intron(environment const & env, options const & opts, metavar_con
optional<expr> intron(environment const & env, options const & opts, metavar_context & mctx,
expr const & mvar, unsigned n);
vm_obj intro(name const & n, tactic_state const & s);
void initialize_intro_tactic();
void finalize_intro_tactic();
}

36
src/library/tactic/smt/smt_state.cpp
View file

@ -152,7 +152,7 @@ tactic_state revert_all(tactic_state const & s) {
return revert(hs, s);
}
vm_obj preprocess(tactic_state const & s, smt_pre_config const & cfg) {
vm_obj preprocess(tactic_state s, smt_pre_config const & cfg) {
lean_assert(s.goals());
optional<metavar_decl> g = s.get_main_goal_decl();
type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
@ -163,28 +163,34 @@ vm_obj preprocess(tactic_state const & s, smt_pre_config const & cfg) {
simp_lemmas_for eq_lemmas;
if (auto r = cfg.m_simp_lemmas.find(get_eq_name()))
eq_lemmas = *r;
expr new_target = dsimplify_fn(ctx, max_steps, visit_instances, eq_lemmas)(target);
dsimplify_fn dsimp(ctx, max_steps, visit_instances, eq_lemmas);
expr new_target = dsimp(target);
ctx.set_env(dsimp.update_defeq_canonizer_state(ctx.env()));
bool contextual = false;
bool lift_eq = true;
bool canonize_instances = true;
bool canonize_proofs = false;
bool use_axioms = true;
simp_result r = simplify_fn(ctx, cfg.m_simp_lemmas, max_steps,
contextual, lift_eq, canonize_instances,
canonize_proofs, use_axioms)(get_eq_name(), new_target);
simplify_fn simp(ctx, cfg.m_simp_lemmas, max_steps,
contextual, lift_eq, canonize_instances,
canonize_proofs, use_axioms);
simp_result r = simp(get_eq_name(), new_target);
ctx.set_env(simp.update_defeq_canonizer_state(ctx.env()));
if (!r.has_proof()) {
s = set_env(s, ctx.env());
return change(r.get_new(), s);
} else {
expr new_M = ctx.mk_metavar_decl(ctx.lctx(), r.get_new());
expr h = mk_app(ctx, get_eq_mpr_name(), r.get_proof(), new_M);
metavar_context mctx = ctx.mctx();
mctx.assign(head(s.goals()), h);
tactic_state new_s = set_mctx_goals(s, mctx, cons(new_M, tail(s.goals())));
tactic_state new_s = set_env_mctx_goals(s, ctx.env(), mctx, cons(new_M, tail(s.goals())));
return mk_tactic_success(new_s);
}
}
expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, smt_goal & s_goal) {
expr intros(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, smt_goal & s_goal,
bool use_unused_names) {
optional<metavar_decl> decl = mctx.get_metavar_decl(mvar);
lean_assert(decl);
type_context ctx(env, opts, mctx, decl->get_context(), transparency_mode::Semireducible);
@ -201,7 +207,8 @@ expr intros(environment const & env, options const & opts, metavar_context & mct
}
if (is_pi(target)) {
expr type = instantiate_rev(binding_domain(target), to_inst.size(), to_inst.data());
name n = ctx.get_unused_name(binding_name(target));
name n = binding_name(target);
if (use_unused_names) n = ctx.get_unused_name(n);
expr h = locals.push_local(n, type);
to_inst.push_back(h);
new_Hs.push_back(h);
@ -211,7 +218,8 @@ expr intros(environment const & env, options const & opts, metavar_context & mct
} else if (is_let(target)) {
expr type = instantiate_rev(let_type(target), to_inst.size(), to_inst.data());
expr value = instantiate_rev(let_value(target), to_inst.size(), to_inst.data());
name n = ctx.get_unused_name(let_name(target));
name n = let_name(target);
if (use_unused_names) n = ctx.get_unused_name(n);
expr h = locals.push_let(n, type, value);
to_inst.push_back(h);
new_Hs.push_back(h);
@ -257,7 +265,8 @@ vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) {
s = to_tactic_state(get_tactic_result_state(r));
metavar_context mctx = s.mctx();
expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), new_goal);
bool use_unused_names = true;
expr new_M = intros(s.env(), s.get_options(), mctx, head(s.goals()), new_goal, use_unused_names);
s = set_mctx_goals(s, mctx, cons(new_M, tail(s.goals())));
return mk_tactic_success(mk_vm_cons(to_obj(new_goal), mk_vm_nil()), s);
}
@ -560,7 +569,7 @@ vm_obj smt_tactic_close(vm_obj const & ss, vm_obj const & _ts) {
return mk_tactic_exception("smt_tactic.close failed", ts);
}
vm_obj smt_tactic_intros(vm_obj const & ss, vm_obj const & _ts) {
vm_obj smt_tactic_intros_core(vm_obj const & use_unused_names, vm_obj const & ss, vm_obj const & _ts) {
tactic_state ts = to_tactic_state(_ts);
if (is_nil(ss))
return mk_smt_state_empty_exception(ts);
@ -573,7 +582,8 @@ vm_obj smt_tactic_intros(vm_obj const & ss, vm_obj const & _ts) {
ts = to_tactic_state(get_tactic_result_state(r));
metavar_context mctx = ts.mctx();
expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()), new_sgoal);
expr new_mvar = intros(ts.env(), ts.get_options(), mctx, head(ts.goals()), new_sgoal,
to_bool(use_unused_names));
tactic_state new_ts = set_mctx_goals(ts, mctx, cons(new_mvar, tail(ts.goals())));
vm_obj new_ss = mk_vm_cons(to_obj(new_sgoal), tail(ss));
@ -588,7 +598,7 @@ void initialize_smt_state() {
DECLARE_VM_BUILTIN(name({"smt_state", "to_format"}), smt_state_to_format);
DECLARE_VM_BUILTIN("tactic_to_smt_tactic", tactic_to_smt_tactic);
DECLARE_VM_BUILTIN(name({"smt_tactic", "close"}), smt_tactic_close);
DECLARE_VM_BUILTIN(name({"smt_tactic", "intros"}), smt_tactic_intros);
DECLARE_VM_BUILTIN(name({"smt_tactic", "intros_core"}), smt_tactic_intros_core);
}
void finalize_smt_state() {

22
tests/lean/run/smt_assert_define.lean Normal file
View file

@ -0,0 +1,22 @@
open smt_tactic
example (a b c : nat) : a = b + 0 → a + c = b + c :=
by using_smt $ do
pr ← tactic.to_expr `(add_zero b),
note `h pr,
trace_state, return ()
constant p : nat → nat → Prop
constant f : nat → nat
axiom pf (a : nat) : p (f a) (f a) → p a a
example (a b c : nat) : a = b → p (f a) (f b) → p a b :=
by using_smt $ do
t ← tactic.to_expr `(p (f a) (f a)),
assert `h t, -- assert automatically closed the new goal
trace_state,
tactic.trace "-----",
pr ← tactic.to_expr `(pf _ h),
note `h2 pr,
trace_state,
return ()