From 031831f1012c9ca9dd675b344e3237ea7cdbd0c3 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Mon, 4 Jan 2016 14:43:31 -0500 Subject: [PATCH] feat(library/tactic): add replace tactic --- library/init/tactic.lean | 2 + src/library/tactic/CMakeLists.txt | 2 +- src/library/tactic/init_module.cpp | 3 + src/library/tactic/replace_tactic.cpp | 127 +++++++++++++++++++++++ src/library/tactic/replace_tactic.h | 15 +++ tests/lean/replace_tac.lean | 38 +++++++ tests/lean/replace_tac.lean.expected.out | 35 +++++++ 7 files changed, 221 insertions(+), 1 deletion(-) create mode 100644 src/library/tactic/replace_tactic.cpp create mode 100644 src/library/tactic/replace_tactic.h create mode 100644 tests/lean/replace_tac.lean create mode 100644 tests/lean/replace_tac.lean.expected.out diff --git a/library/init/tactic.lean b/library/init/tactic.lean index e881c819e..3aaeb60ee 100644 --- a/library/init/tactic.lean +++ b/library/init/tactic.lean @@ -96,6 +96,7 @@ definition trace (s : string) : tactic := builtin definition rewrite_tac (e : expr_list) : tactic := builtin definition xrewrite_tac (e : expr_list) : tactic := builtin definition krewrite_tac (e : expr_list) : tactic := builtin +definition replace (old : expr) (new : with_expr) (loc : location) : tactic := builtin -- Arguments: -- - ls : lemmas to be used (if not provided, then blast will choose them) @@ -161,3 +162,4 @@ end tactic tactic_infixl `;`:15 := tactic.and_then tactic_notation T1 `:`:15 T2 := tactic.focus (tactic.and_then T1 (tactic.all_goals T2)) tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r +--tactic_notation `replace` s `with` t := tactic.replace_tac s t diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index b798a07f2..0724ebf86 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -7,4 +7,4 @@ init_module.cpp change_tactic.cpp check_expr_tactic.cpp note_tactic.cpp contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp -norm_num_tactic.cpp) \ No newline at end of file +norm_num_tactic.cpp replace_tactic.cpp) diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index de29720a7..759c1b383 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -33,6 +33,7 @@ Author: Leonardo de Moura #include "library/tactic/location.h" #include "library/tactic/with_options_tactic.h" #include "library/tactic/norm_num_tactic.h" +#include "library/tactic/replace_tactic.h" namespace lean { void initialize_tactic_module() { @@ -64,6 +65,7 @@ void initialize_tactic_module() { initialize_location(); initialize_with_options_tactic(); initialize_norm_num_tactic(); + initialize_replace_tactic(); } void finalize_tactic_module() { @@ -95,5 +97,6 @@ void finalize_tactic_module() { finalize_apply_tactic(); finalize_expr_to_tactic(); finalize_proof_state(); + finalize_replace_tactic(); } } diff --git a/src/library/tactic/replace_tactic.cpp b/src/library/tactic/replace_tactic.cpp new file mode 100644 index 000000000..cc465a446 --- /dev/null +++ b/src/library/tactic/replace_tactic.cpp @@ -0,0 +1,127 @@ + /* +Copyright (c) 2015 Robert Y. Lewis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Robert Y. Lewis +*/ + +#include "library/tactic/replace_tactic.h" +#include "util/lazy_list_fn.h" +#include "kernel/error_msgs.h" +#include "library/constants.h" +#include "library/reducible.h" +#include "library/unifier.h" +#include "library/tactic/expr_to_tactic.h" +#include "kernel/instantiate.h" + +namespace lean { + + +static expr * g_replace_tac = nullptr; + +expr substitute_at_occurrences(environment const & env, expr const & t, expr const & nexpr, expr const & oexpr, occurrence const & occ) { + bool has_dep_elim = inductive::has_dep_elim(env, get_eq_name()); + unsigned vidx = has_dep_elim ? 1 : 0; + optional nt = replace_occurrences(t, oexpr, occ, vidx); + if (!nt) { + return t; + } + expr t2 = instantiate(*nt, vidx, nexpr); + return t2; +} + +tactic mk_replace_tactic(elaborate_fn const & elab, expr const & e) { + return tactic([=](environment const & env, io_state const & ios, proof_state const & s) { + buffer e_args; + get_app_args(e, e_args); + expr t1, t2; // replace t2 with t1 + location loc; + if (e_args.size() == 3) { + t1 = get_tactic_expr_expr(e_args[1]); + t2 = get_tactic_expr_expr(e_args[0]); + if (is_location_expr(get_tactic_expr_expr(e_args[2]))) { + loc = get_location_expr_location(get_tactic_expr_expr(e_args[2])); + } else { + loc = location(); + } + } else { + throw_tactic_exception_if_enabled(s, "malformed arguments to replace"); + return proof_state_seq(); + } + proof_state new_s = s; + goals const & gs = new_s.get_goals(); + if (!gs) { + throw_no_goal_if_enabled(s); + return proof_state_seq(); + } + expr t = head(gs).get_type(); + bool report_unassigned = true; + auto new_t1 = elaborate_with_respect_to(env, ios, elab, new_s, t1, none_expr(), report_unassigned); + auto new_t2 = elaborate_with_respect_to(env, ios, elab, new_s, t2, none_expr(), report_unassigned); + if (new_t1 && new_t2) { + goals const & gs = new_s.get_goals(); + goal const & g = head(gs); + name_generator ngen = new_s.get_ngen(); + substitution subst = new_s.get_subst(); + auto tc = mk_type_checker(env, ngen.mk_child()); + constraint_seq cs; + if (tc->is_def_eq(*new_t1, *new_t2, justification(), cs)) { + auto nocc = loc.includes_goal(); + expr new_goal; + if (nocc) { + new_goal = substitute_at_occurrences(env, g.get_type(), *new_t1, *new_t2, *nocc); + } else { + throw_tactic_exception_if_enabled(s, "replacing in hypotheses not implemented"); + return proof_state_seq(); + } + if (cs) { + unifier_config cfg(ios.get_options()); + buffer cs_buf; + cs.linearize(cs_buf); + to_buffer(new_s.get_postponed(), cs_buf); + unify_result_seq rseq = unify(env, cs_buf.size(), cs_buf.data(), ngen.mk_child(), subst, cfg); + return map2(rseq, [=](pair const & p) -> proof_state { + substitution const & subst = p.first; + constraints const & postponed = p.second; + name_generator new_ngen(ngen); + substitution new_subst = subst; + expr M = g.mk_meta(new_ngen.next(), new_goal); + goal new_g(M, new_goal); + assign(new_subst, g, M); + return proof_state(new_s, cons(new_g, tail(gs)), new_subst, new_ngen, postponed); + }); + } + expr M = g.mk_meta(ngen.next(), new_goal); + goal new_g(M, new_goal); + assign(subst, g, M); + return proof_state_seq(proof_state(new_s, cons(new_g, tail(gs)), subst, ngen)); + } else { + throw_tactic_exception_if_enabled(new_s, [=](formatter const & fmt) { + format r = format("invalid 'replace' tactic, the new type"); + r += pp_indent_expr(fmt, *new_t1); + r += compose(line(), format("does not match the old type")); + r += pp_indent_expr(fmt, *new_t2); + return r; + }); + return proof_state_seq(); + } + } + return proof_state_seq(); + }); +} + +void initialize_replace_tactic() { + name replace_tac_name{"tactic", "replace"}; + g_replace_tac = new expr(Const(replace_tac_name)); + register_tac(replace_tac_name, + [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) { + return mk_replace_tactic(elab, e); + }); + +} + +void finalize_replace_tactic() { + delete g_replace_tac; +} + +} diff --git a/src/library/tactic/replace_tactic.h b/src/library/tactic/replace_tactic.h new file mode 100644 index 000000000..a0cc17a85 --- /dev/null +++ b/src/library/tactic/replace_tactic.h @@ -0,0 +1,15 @@ + /* +Copyright (c) 2015 Robert Y. Lewis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. + +Author: Robert Y. Lewis +*/ +#pragma once +#include "library/tactic/tactic.h" +#include "library/tactic/location.h" + +namespace lean { + +void initialize_replace_tactic(); +void finalize_replace_tactic(); +} diff --git a/tests/lean/replace_tac.lean b/tests/lean/replace_tac.lean new file mode 100644 index 000000000..dffc8d69a --- /dev/null +++ b/tests/lean/replace_tac.lean @@ -0,0 +1,38 @@ +import data.list +open nat list + +example (H : false) : (1 : ℕ) + 1 = (2 : ℕ) := +begin + replace (1 : ℕ) with (succ 0) at {1}, +end + +example (H : false) : (1 : ℕ) + 1 = (2 : ℕ) := +begin + replace (1 : ℕ) with (succ 1), +end + +definition foo (n : ℕ) : ℕ := n +definition bar := foo +example (h : true) : foo 2 = bar 2 := +begin + replace foo 2 with bar 2 at h, + reflexivity +end + +constants (P : ℕ → Type₁) (p : P (3 + 1)) (f : Πn, P n) +example : f (3 + 1) = p := +begin + replace ((3 : ℕ) + 1) with (4 : ℕ), +end + +variables {A B : Type} +lemma my_map_concat (f : A → B) (a : A) : Πl, map f (concat a l) = concat (f a) (map f l) +| nil := rfl +| (b::l) := begin + replace concat a (b :: l) with b :: concat a l, + replace concat (f a) (map f (b :: l)) with f b :: concat (f a) (map f l), + replace map f (b :: concat a l) with f b :: map f (concat a l), + congruence, + apply my_map_concat + + end diff --git a/tests/lean/replace_tac.lean.expected.out b/tests/lean/replace_tac.lean.expected.out new file mode 100644 index 000000000..0a4279f34 --- /dev/null +++ b/tests/lean/replace_tac.lean.expected.out @@ -0,0 +1,35 @@ +replace_tac.lean:7:0: error: 1 unsolved subgoal +H : false +⊢ succ 0 + 1 = 2 +replace_tac.lean:7:0: error: failed to add declaration 'example' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + ?M_1 +replace_tac.lean:11:2: error:invalid 'replace' tactic, the new type + succ 1 +does not match the old type + 1 +proof state: +H : false +⊢ 1 + 1 = 2 +replace_tac.lean:12:0: error: don't know how to synthesize placeholder +H : false +⊢ 1 + 1 = 2 +replace_tac.lean:12:0: error: failed to add declaration 'example' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + ?M_1 +replace_tac.lean:18:2: error:replacing in hypotheses not implemented +proof state: +h : true +⊢ foo 2 = bar 2 +replace_tac.lean:20:0: error: don't know how to synthesize placeholder +h : true +⊢ foo 2 = bar 2 +replace_tac.lean:20:0: error: failed to add declaration 'example' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + ?M_1 +replace_tac.lean:26:0: error: 1 unsolved subgoal + +⊢ f 4 = p +replace_tac.lean:26:0: error: failed to add declaration 'example' to environment, value has metavariables +remark: set 'formatter.hide_full_terms' to false to see the complete term + ?M_1 \ No newline at end of file