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

feat(library/tactic/rewrite_tactic): add reduction step to rewrite tactic

Browse source
This commit is contained in:
Leonardo de Moura 2015-02-05 13:42:50 -08:00
parent 38ab4e7b3a
commit 116c65bff5
2 changed files with 23 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
src/library/tactic/rewrite_tactic.cpp
View file

@ -520,6 +520,17 @@ class rewrite_fn {
return process_reduce_step(optional<name>(info.get_name()), info.get_location()); return process_reduce_step(optional<name>(info.get_name()), info.get_location());
} }
bool process_reduce_step(expr const & elem) {
lean_assert(is_rewrite_reduce_step(elem));
if (macro_num_args(elem) == 0) {
auto info = get_rewrite_reduce_info(elem);
return process_reduce_step(optional<name>(), info.get_location());
} else {
// TODO
return false;
}
}
// Replace metavariables with special metavariables for the higher-order matcher. This is method is used when // Replace metavariables with special metavariables for the higher-order matcher. This is method is used when
// converting an expression into a pattern. // converting an expression into a pattern.
expr to_meta_idx(expr const & e) { expr to_meta_idx(expr const & e) {
@ -883,6 +894,8 @@ class rewrite_fn {
bool process_step(expr const & elem) { bool process_step(expr const & elem) {
if (is_rewrite_unfold_step(elem)) { if (is_rewrite_unfold_step(elem)) {
return process_unfold_step(elem); return process_unfold_step(elem);
} else if (is_rewrite_reduce_step(elem)) {
return process_reduce_step(elem);
} else { } else {
expr rule = get_rewrite_rule(elem); expr rule = get_rewrite_rule(elem);
expr new_elem; expr new_elem;
@ -973,7 +986,7 @@ void initialize_rewrite_tactic() {
[](deserializer & d, unsigned num, expr const * args) { [](deserializer & d, unsigned num, expr const * args) {
if (num > 1) if (num > 1)
throw corrupted_stream_exception(); throw corrupted_stream_exception();
unfold_info info; reduce_info info;
d >> info; d >> info;
if (num == 0) if (num == 0)
return mk_rewrite_reduce(info.get_location()); return mk_rewrite_reduce(info.get_location());
@ -1003,7 +1016,7 @@ void initialize_rewrite_tactic() {
buffer<expr> args; buffer<expr> args;
get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument"); get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument");
for (expr const & arg : args) { for (expr const & arg : args) {
if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg)) if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg) && !is_rewrite_reduce_step(arg))
throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument"); throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument");
} }
return mk_rewrite_tactic(elab, args); return mk_rewrite_tactic(elab, args);
@ -1015,6 +1028,8 @@ void finalize_rewrite_tactic() {
delete g_rewrite_tac; delete g_rewrite_tac;
delete g_rewrite_unfold_name; delete g_rewrite_unfold_name;
delete g_rewrite_unfold_opcode; delete g_rewrite_unfold_opcode;
delete g_rewrite_reduce_name;
delete g_rewrite_reduce_opcode;
delete g_rewrite_elem_name; delete g_rewrite_elem_name;
delete g_rewrite_elem_opcode; delete g_rewrite_elem_opcode;
} }

6
tests/lean/run/rewrite8.lean Normal file
View file

@ -0,0 +1,6 @@
import data.nat
open nat
constant f : nat → nat
theorem tst1 (x y : nat) (H1 : (λ z, z + 0) x = y) : f x = f y :=
by rewrite [▸* at H1, ^add at H1, ^nat.rec_on at H1, ^of_num at H1, H1]