feat(library/tactic): add replace tactic

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

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)
+norm_num_tactic.cpp replace_tactic.cpp)

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();
 }
 }

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<expr> 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<expr> 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<constraint> 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<proof_state>(rseq, [=](pair<substitution, constraints> 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;
+}
+
+}

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();
+}

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

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