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

feat(library/tactic/unfold_tactic): add unfold_projection tactic

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-12 13:43:32 -07:00
parent e6acd52fc2
commit 46eb7decde
3 changed files with 37 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
library/init/meta/simp_tactic.lean
View file

@ -93,6 +93,11 @@ dsimplify_core 1000000 ff pre post
meta constant dunfold_expr : expr → tactic expr
meta constant unfold_projection_core : transparency → expr → tactic expr
meta def unfold_projection : expr → tactic expr :=
unfold_projection_core reducible
meta def simplify (prove_fn : tactic unit) (extra_lemmas : list expr) (e : expr) : tactic (expr × expr) :=
do lemmas ← simp_lemmas.mk_default,
new_lemmas ← lemmas^.append extra_lemmas,

25
src/library/tactic/unfold_tactic.cpp
View file

@ -412,6 +412,22 @@ vm_obj tactic_unfold_expr(vm_obj const & force, vm_obj const & occs, vm_obj cons
}
}
vm_obj tactic_unfold_projection_core(vm_obj const & m, vm_obj const & _e, vm_obj const & _s) {
expr const & e = to_expr(_e);
tactic_state const & s = to_tactic_state(_s);
try {
expr const & fn = get_app_fn(e);
type_context ctx = mk_type_context_for(s, to_transparency_mode(m));
if (!is_constant(fn) || !is_projection(s.env(), const_name(fn)))
return mk_tactic_exception("unfold projection failed, expression is not a projection application", s);
if (auto new_e = ctx.reduce_projection(e))
return mk_tactic_success(to_obj(*new_e), s);
return mk_tactic_exception("unfold projection failed, failed to unfold", s);
} catch (exception & ex) {
return mk_tactic_exception(ex, s);
}
}
vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & _s) {
expr const & e = to_expr(_e);
tactic_state const & s = to_tactic_state(_s);
@ -441,12 +457,6 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & _s) {
buffer<expr> args;
get_app_args(e, args);
expr new_e = head_beta_reduce(mk_app(instantiate_value_univ_params(d, const_levels(fn)), args.size(), args.data()));
type_context ctx = mk_type_context_for(s);
expr const & new_fn = get_app_fn(new_e);
if (is_constant(new_fn) && is_projection(env, const_name(new_fn))) {
if (auto new_new_e = ctx.reduce_projection(new_e))
new_e = *new_new_e;
}
return mk_tactic_success(to_obj(new_e), s);
}
} catch (exception & ex) {
@ -456,7 +466,8 @@ vm_obj tactic_dunfold_expr(vm_obj const & _e, vm_obj const & _s) {
void initialize_unfold_tactic() {
DECLARE_VM_BUILTIN(name({"tactic", "unfold_expr_core"}), tactic_unfold_expr);
DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}), tactic_dunfold_expr);
DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection_core"}), tactic_unfold_projection_core);
DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr"}), tactic_dunfold_expr);
}
void finalize_unfold_tactic() {

17
tests/lean/run/dunfold1.lean
View file

@ -2,11 +2,22 @@ open tactic
set_option pp.all true
example (a b : nat) (p : nat → Prop) (h : p (nat.succ (nat.succ a))) : p (a + 2) :=
def g : nat → nat := λ x, x + 5
example (a b : nat) (p : nat → Prop) (h : p (g (nat.succ (nat.succ a)))) : p (g (a + 2)) :=
by do
t ← target,
new_t ← dsimplify (λ e, failed) (λ e, do new_e ← dunfold_expr e, trace e, trace "===>", trace new_e, trace "-------", return (new_e, tt)) t,
expected ← to_expr `(p (nat.succ (nat.succ a))),
new_t ← dsimplify (λ e, failed)
(λ e,
do { new_e ← unfold_projection e, return (new_e, tt) }
<|>
do {
guard ([`add, `nat.add, `one, `zero, `bit0, `bit1]^.any e^.is_app_of),
new_e ← dunfold_expr e, trace e,
trace "===>", trace new_e, trace "-------",
return (new_e, tt) })
t,
expected ← to_expr `(p (g (nat.succ (nat.succ a)))),
guard (new_t = expected),
trace new_t,
assumption