feat(library/tactic): add 'subst' tactic

see issue #500

hott/init/tactic.hlean

@@ -109,6 +109,8 @@ opaque definition right                        : tactic := builtin
 
 opaque definition injection (e : expr) (ids : opt_identifier_list) : tactic := builtin
 
+opaque definition subst (ids : identifier_list) : tactic := builtin
+
 definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0

library/init/tactic.lean

@@ -109,6 +109,8 @@ opaque definition right                        : tactic := builtin
 
 opaque definition injection (e : expr) (ids : opt_identifier_list) : tactic := builtin
 
+opaque definition subst (ids : identifier_list) : tactic := builtin
+
 definition try         (t : tactic) : tactic := or_else t id
 definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
 definition focus       (t : tactic) : tactic := focus_at t 0

src/library/tactic/rewrite_tactic.cpp

@@ -30,6 +30,8 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/constants.h"
 #include "library/generic_exception.h"
+#include "library/tactic/clear_tactic.h"
+#include "library/tactic/trace_tactic.h"
 #include "library/tactic/rewrite_tactic.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/tactic/class_instance_synth.h"
@@ -1505,6 +1507,81 @@ tactic mk_rewrite_tactic(elaborate_fn const & elab, buffer<expr> const & elems)
         });
 }
 
+tactic mk_simple_rewrite_tactic(buffer<expr> const & rw_elems) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+        // dummy elaborator
+        auto elab = [](goal const &, name_generator const &, expr const & H,
+                       optional<expr> const &, bool) -> pair<expr, constraints> {
+            return mk_pair(H, constraints());
+        };
+        return rewrite_fn(env, ios, elab, s)(rw_elems);
+    };
+    return tactic(fn);
+}
+
+tactic mk_simple_rewrite_tactic(expr const & rw_elem) {
+    buffer<expr> rw_elems;
+    rw_elems.push_back(rw_elem);
+    return mk_simple_rewrite_tactic(rw_elems);
+}
+
+tactic mk_subst_tactic(list<name> const & ids) {
+    auto fn = [=](environment const & env, io_state const & ios, proof_state const & s) {
+        if (!ids)
+            return proof_state_seq(s);
+        goals const & gs = s.get_goals();
+        if (empty(gs))
+            return proof_state_seq();
+        goal const & g  = head(gs);
+        name const & id = head(ids);
+
+        auto apply_rewrite = [&](expr const & H, bool symm) {
+            tactic tac = then(mk_simple_rewrite_tactic(mk_rewrite_once(none_expr(), H, symm, location::mk_everywhere())),
+                              then(clear_tactic(local_pp_name(H)),
+                                   mk_subst_tactic(tail(ids))));
+            return tac(env, ios, s);
+        };
+
+        optional<pair<expr, unsigned>> p = g.find_hyp(id);
+        if (!p) {
+            throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, there is no hypothesis named '"
+                                              << id << "'");
+            return proof_state_seq();
+        }
+        expr const & H = p->first;
+        expr lhs, rhs;
+        if (is_eq(mlocal_type(H), lhs, rhs)) {
+            if (is_local(lhs)) {
+                return apply_rewrite(H, false);
+            } else if (is_local(rhs)) {
+                return apply_rewrite(H, true);
+            } else {
+                throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
+                                                  << id << "' is not of the form (x = t) or (t = x)");
+                return proof_state_seq();
+            }
+        } else if (is_local(H)) {
+            expr const & x = H;
+            buffer<expr> hyps;
+            g.get_hyps(hyps);
+            for (expr const & H : hyps) {
+                expr lhs, rhs;
+                if (is_eq(mlocal_type(H), lhs, rhs)) {
+                    if (is_local(lhs) && mlocal_name(lhs) == mlocal_name(x)) {
+                        return apply_rewrite(H, false);
+                    } else if (is_local(rhs) && mlocal_name(rhs) == mlocal_name(x)) {
+                        return apply_rewrite(H, true);
+                    }
+                }
+            }
+        }
+        throw_tactic_exception_if_enabled(s, sstream() << "invalid 'subst' tactic, hypothesis '"
+                                          << id << "' is not a variable nor an equation of the form (x = t) or (t = x)");
+        return proof_state_seq();
+    };
+    return tactic(fn);
+}
+
 void initialize_rewrite_tactic() {
     g_rewriter_max_iterations = new name{"rewriter", "max_iter"};
     register_unsigned_option(*g_rewriter_max_iterations, LEAN_DEFAULT_REWRITER_MAX_ITERATIONS,
@@ -1573,6 +1650,13 @@ void initialize_rewrite_tactic() {
                      }
                      return mk_rewrite_tactic(elab, args);
                  });
+    register_tac(name{"tactic", "subst"},
+                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
+                     buffer<name> ns;
+                     get_tactic_id_list_elements(app_arg(e), ns, "invalid 'subst' tactic, list of identifiers expected");
+                     return mk_subst_tactic(to_list(ns));
+                 });
+
 }
 
 void finalize_rewrite_tactic() {

tests/lean/hott/subst_tac.hlean

@@ -0,0 +1,33 @@
+open nat
+
+example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
+begin
+  intro a0 b1 ab,
+  subst a0 b1,
+  state,
+  contradiction
+end
+
+example (a b c : nat) : a = 0 → b = 1 + a → a = b → empty :=
+begin
+  intro a0 b1 ab,
+  subst a0, subst b1,
+  state,
+  contradiction
+end
+
+example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty :=
+begin
+  intro a0 b1 ab,
+  subst a0 b1,
+  state,
+  contradiction
+end
+
+example (a b c : nat) : a = 0 → 1 + a = b → a = b → empty :=
+begin
+  intros,
+  subst a b,
+  state,
+  contradiction
+end

tests/lean/run/subst_tact.lean

@@ -0,0 +1,33 @@
+open nat
+
+example (a b c : nat) : a = 0 → b = 1 + a → a = b → false :=
+begin
+  intro a0 b1 ab,
+  subst a0 b1,
+  state,
+  contradiction
+end
+
+example (a b c : nat) : a = 0 → b = 1 + a → a = b → false :=
+begin
+  intro a0 b1 ab,
+  subst a0, subst b1,
+  state,
+  contradiction
+end
+
+example (a b c : nat) : a = 0 → 1 + a = b → a = b → false :=
+begin
+  intro a0 b1 ab,
+  subst a0 b1,
+  state,
+  contradiction
+end
+
+example (a b c : nat) : a = 0 → 1 + a = b → a = b → false :=
+begin
+  intros,
+  subst a b,
+  state,
+  contradiction
+end