feat(library/tactic/rewrite_tactic): add xrewrite and krewrite tactic variants

closes #511

hott/init/tactic.hlean

@@ -87,7 +87,9 @@ definition trace      (s : string)          : tactic := builtin
 
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.
-definition rewrite_tac (e : expr_list) : 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 cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
 

library/init/tactic.lean

@@ -87,7 +87,9 @@ definition trace      (s : string)       : tactic := builtin
 
 -- rewrite_tac is just a marker for the builtin 'rewrite' notation
 -- used to create instances of this tactic.
-definition rewrite_tac (e : expr_list) : 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 cases (id : identifier) (ids : opt_identifier_list) : tactic := builtin
 

src/emacs/lean-syntax.el

@@ -137,9 +137,10 @@
             (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply"
                 "apply" "fapply" "eapply" "rename" "intro" "intros" "all_goals" "fold" "focus" "focus_at"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
-                "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
-                "unfold" "change" "check_expr" "contradiction" "exfalso" "split" "existsi" "constructor" "left" "right"
-                "injection" "congruence" "reflexivity" "symmetry" "transitivity" "state" "induction" "induction_using"
+                "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite"
+                "xrewrite" "krewrite" "esimp" "unfold" "change" "check_expr" "contradiction"
+                "exfalso" "split" "existsi" "constructor" "left" "right" "injection" "congruence" "reflexivity"
+                "symmetry" "transitivity" "state" "induction" "induction_using"
                 "substvars"))
            word-end)
       (1 'font-lock-constant-face))

src/frontends/lean/builtin_tactics.cpp

@@ -16,6 +16,14 @@ static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_in
     return p.save_pos(parse_rewrite_tactic(p), pos);
 }
 
+static expr parse_xrewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_xrewrite_tactic(p), pos);
+}
+
+static expr parse_krewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_krewrite_tactic(p), pos);
+}
+
 static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.save_pos(parse_esimp_tactic(p), pos);
 }
@@ -62,6 +70,8 @@ parse_table init_tactic_nud_table() {
     parse_table r;
     r = r.add({transition("(", Expr), transition(")", mk_ext_action(parse_rparen))}, x0);
     r = r.add({transition("rewrite",    mk_ext_action(parse_rewrite_tactic_expr))}, x0);
+    r = r.add({transition("krewrite",   mk_ext_action(parse_krewrite_tactic_expr))}, x0);
+    r = r.add({transition("xrewrite",   mk_ext_action(parse_xrewrite_tactic_expr))}, x0);
     r = r.add({transition("esimp",      mk_ext_action(parse_esimp_tactic_expr))}, x0);
     r = r.add({transition("generalize", mk_ext_action(parse_generalize_tactic))}, x0);
     r = r.add({transition("unfold",     mk_ext_action(parse_unfold_tactic_expr))}, x0);

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -120,8 +120,7 @@ static expr parse_rewrite_element(parser & p, bool use_paren) {
     }
 }
 
-expr parse_rewrite_tactic(parser & p) {
-    buffer<expr> elems;
+void parse_rewrite_tactic_elems(parser & p, buffer<expr> & elems) {
     if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
         while (true) {
@@ -136,9 +135,26 @@ expr parse_rewrite_tactic(parser & p) {
         auto pos = p.pos();
         elems.push_back(p.save_pos(parse_rewrite_element(p, true), pos));
     }
+}
+
+expr parse_rewrite_tactic(parser & p) {
+    buffer<expr> elems;
+    parse_rewrite_tactic_elems(p, elems);
     return mk_rewrite_tactic_expr(elems);
 }
 
+expr parse_xrewrite_tactic(parser & p) {
+    buffer<expr> elems;
+    parse_rewrite_tactic_elems(p, elems);
+    return mk_xrewrite_tactic_expr(elems);
+}
+
+expr parse_krewrite_tactic(parser & p) {
+    buffer<expr> elems;
+    parse_rewrite_tactic_elems(p, elems);
+    return mk_krewrite_tactic_expr(elems);
+}
+
 expr parse_esimp_tactic(parser & p) {
     buffer<expr> elems;
     auto pos = p.pos();

src/frontends/lean/parse_rewrite_tactic.h

@@ -10,6 +10,8 @@ Author: Leonardo de Moura
 namespace lean {
 class parser;
 expr parse_rewrite_tactic(parser & p);
+expr parse_krewrite_tactic(parser & p);
+expr parse_xrewrite_tactic(parser & p);
 expr parse_esimp_tactic(parser & p);
 expr parse_unfold_tactic(parser & p);
 expr parse_fold_tactic(parser & p);

src/frontends/lean/token_table.cpp

@@ -94,10 +94,11 @@ void init_token_table(token_table & t) {
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0},
-         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 0}, {"unfold", 0},
-         {"generalize", 0}, {"as", 0},
-         {":=", 0}, {"--", 0}, {"#", 0},
-         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
+         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"xrewrite", 0}, {"krewrite", 0},
+         {"esimp", 0}, {"fold", 0}, {"unfold", 0},
+         {"generalize", 0}, {"as", 0}, {":=", 0}, {"--", 0}, {"#", 0},
+         {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"begin+", g_max_prec},
+         {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {"?(", g_max_prec}, {"⌞", g_max_prec}, {"⌟", 0}, {"match", 0},
          {"<d", g_decreasing_prec}, {"renaming", 0}, {"extends", 0}, {nullptr, 0}};
@@ -114,7 +115,8 @@ void init_token_table(token_table & t) {
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
          "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation",
-         "exit", "set_option", "open", "export", "override", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
+         "exit", "set_option", "open", "export", "override", "calc_subst", "calc_refl", "calc_trans",
+         "calc_symm", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",
          "include", "omit", "migrate", "init_quotient", "init_hits", "#erase_cache", "#projections", "#telescope_eq",

src/library/tactic/rewrite_tactic.cpp

@@ -188,6 +188,8 @@ public:
 };
 
 static expr * g_rewrite_tac                   = nullptr;
+static expr * g_xrewrite_tac                  = nullptr;
+static expr * g_krewrite_tac                  = nullptr;
 
 static name * g_rewrite_elem_name             = nullptr;
 static std::string * g_rewrite_elem_opcode    = nullptr;
@@ -384,14 +386,31 @@ rewrite_info const & get_rewrite_info(expr const & e) {
     return static_cast<rewrite_element_macro_cell const*>(macro_def(e).raw())->get_info();
 }
 
-expr mk_rewrite_tactic_expr(buffer<expr> const & elems) {
-    lean_assert(std::all_of(elems.begin(), elems.end(), [](expr const & e) {
+bool check_tactic_elems(buffer<expr> const & elems) {
+    if (std::all_of(elems.begin(), elems.end(), [](expr const & e) {
                 return is_rewrite_step(e) || is_rewrite_unfold_step(e) ||
-                    is_rewrite_reduce_step(e) || is_rewrite_fold_step(e);
-            }));
+                    is_rewrite_reduce_step(e) || is_rewrite_fold_step(e); })) {
+        lean_unreachable();
+        return false;
+    }
+    return true;
+}
+
+expr mk_rewrite_tactic_expr(buffer<expr> const & elems) {
+    lean_assert(check_tactic_elems(elems));
     return mk_app(*g_rewrite_tac, mk_expr_list(elems.size(), elems.data()));
 }
 
+expr mk_krewrite_tactic_expr(buffer<expr> const & elems) {
+    lean_assert(check_tactic_elems(elems));
+    return mk_app(*g_krewrite_tac, mk_expr_list(elems.size(), elems.data()));
+}
+
+expr mk_xrewrite_tactic_expr(buffer<expr> const & elems) {
+    lean_assert(check_tactic_elems(elems));
+    return mk_app(*g_xrewrite_tac, mk_expr_list(elems.size(), elems.data()));
+}
+
 /**
    \brief make sure hypothesis h occur after hs (if possible).
    This procedure assumes that all hypotheses in \c hs occur in g, and it has no duplicates.
@@ -548,6 +567,7 @@ class rewrite_fn {
     expr                 m_expr_loc; // auxiliary expression used for error localization
 
     bool                 m_use_trace;
+    bool                 m_keyed;
     unsigned             m_max_iter;
 
     buffer<optional<level>> m_lsubst; // auxiliary buffer for pattern matching
@@ -902,9 +922,11 @@ class rewrite_fn {
     }
 
     // Given the rewrite step \c e, return a pattern to be used to locate the term to be rewritten.
-    expr get_pattern(expr const & e) {
+    expr get_pattern_core(expr const & e) {
         lean_assert(is_rewrite_step(e));
         if (has_rewrite_pattern(e)) {
+            if (m_keyed)
+                throw_rewrite_exception("invalid krewrite tactic, keyed-matching does not support user-defined patterns");
             return to_meta_idx(get_rewrite_pattern(e));
         } else {
             // Remark: we discard constraints generated producing the pattern.
@@ -933,6 +955,20 @@ class rewrite_fn {
         }
     }
 
+    expr get_pattern(expr const & e) {
+        expr r = get_pattern_core(e);
+        if (m_keyed) {
+            expr const & f = get_app_fn(r);
+            if (is_constant(f) || is_local(f))
+                return f;
+            else
+                throw_rewrite_exception("invalid krewrite tactic, "
+                                        "left-hand-side of equation must be headed by a constant or local");
+        } else {
+            return r;
+        }
+    }
+
     // Set m_esubst and m_lsubst elements to none
     void reset_subst() {
         for (optional<level> & l : m_lsubst)
@@ -1004,7 +1040,8 @@ class rewrite_fn {
                 return format();
             if (!m_failures) {
                 if (m_is_hypothesis)
-                    return line() + format("no subterm in the hypothesis '") + fmt(m_target) + format("' matched the pattern");
+                    return line() + format("no subterm in the hypothesis '") +
+                        fmt(m_target) + format("' matched the pattern");
                 else
                     return line() + format("no subterm in the goal matched the pattern");
             }
@@ -1196,10 +1233,16 @@ class rewrite_fn {
                     return false; // stop search
                 if (closed(t)) {
                     lean_assert(std::all_of(m_esubst.begin(), m_esubst.end(), [&](optional<expr> const & e) { return !e; }));
-                    bool assigned = false;
-                    bool r = match(pattern, t, m_lsubst, m_esubst, nullptr, nullptr, &m_mplugin, &assigned);
-                    if (assigned)
-                        reset_subst();
+                    bool r;
+                    if (m_keyed) {
+                        expr const & f = get_app_fn(t);
+                        r = f == pattern;
+                    } else {
+                        bool assigned = false;
+                        r = match(pattern, t, m_lsubst, m_esubst, nullptr, nullptr, &m_mplugin, &assigned);
+                        if (assigned)
+                            reset_subst();
+                    }
                     if (r) {
                         if (auto p = unify_target(t, orig_elem, is_goal)) {
                             result = std::make_tuple(t, p->second, p->first);
@@ -1424,12 +1467,12 @@ class rewrite_fn {
         }
     }
 
-    type_checker_ptr mk_matcher_tc() {
+    type_checker_ptr mk_matcher_tc(bool full) {
         if (get_rewriter_syntactic(m_ios.get_options())) {
             // use an everything opaque converter
             return mk_opaque_type_checker(m_env, m_ngen.mk_child());
         } else {
-            auto aux_pred = mk_not_reducible_pred(m_env);
+            auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env);
             return mk_type_checker(m_env, m_ngen.mk_child(), [=](name const & n) {
                     return is_projection(m_env, n) || aux_pred(n);
                 });
@@ -1482,13 +1525,15 @@ class rewrite_fn {
     }
 
 public:
-    rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps):
+    rewrite_fn(environment const & env, io_state const & ios, elaborate_fn const & elab, proof_state const & ps,
+               bool full, bool keyed):
         m_env(env), m_ios(ios), m_elab(elab), m_ps(ps), m_ngen(ps.get_ngen()),
-        m_tc(mk_type_checker(m_env, m_ngen.mk_child(), UnfoldQuasireducible)),
-        m_matcher_tc(mk_matcher_tc()),
+        m_tc(mk_type_checker(m_env, m_ngen.mk_child(), full ? UnfoldSemireducible : UnfoldQuasireducible)),
+        m_matcher_tc(mk_matcher_tc(full)),
         m_relaxed_tc(mk_type_checker(m_env, m_ngen.mk_child())),
         m_mplugin(m_ios, *m_matcher_tc) {
-        m_ps = apply_substitution(m_ps);
+        m_keyed = keyed;
+        m_ps    = apply_substitution(m_ps);
         goals const & gs = m_ps.get_goals();
         lean_assert(gs);
         update_goal(head(gs));
@@ -1517,17 +1562,29 @@ public:
     }
 };
 
-tactic mk_rewrite_tactic(elaborate_fn const & elab, buffer<expr> const & elems) {
+tactic mk_rewrite_tactic_core(elaborate_fn const & elab, buffer<expr> const & elems, bool full, bool keyed) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) {
             goals const & gs = s.get_goals();
             if (empty(gs)) {
                 throw_no_goal_if_enabled(s);
                 return proof_state_seq();
             }
-            return rewrite_fn(env, ios, elab, s)(elems);
+            return rewrite_fn(env, ios, elab, s, full, keyed)(elems);
         });
 }
 
+tactic mk_rewrite_tactic(elaborate_fn const & elab, expr const & e, bool full, bool keyed) {
+    buffer<expr> args;
+    get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument");
+    for (expr const & arg : args) {
+        if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg) &&
+            !is_rewrite_reduce_step(arg) && !is_rewrite_fold_step(arg))
+            throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument");
+    }
+    bool fail_if_metavars = true;
+    return then(mk_rewrite_tactic_core(elab, args, full, keyed), try_tactic(refl_tactic(elab, fail_if_metavars)));
+}
+
 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,
@@ -1540,6 +1597,8 @@ void initialize_rewrite_tactic() {
                          "(rewriter tactic) if true tactic will generate a trace for rewrite step failures");
     name rewrite_tac_name{"tactic", "rewrite_tac"};
     g_rewrite_tac           = new expr(Const(rewrite_tac_name));
+    g_xrewrite_tac          = new expr(Const(name{"tactic", "xrewrite_tac"}));
+    g_krewrite_tac          = new expr(Const(name{"tactic", "krewrite_tac"}));
     g_rewrite_reduce_name   = new name("rewrite_reduce");
     g_rewrite_reduce_opcode = new std::string("RWR");
     g_rewrite_unfold_name   = new name("rewrite_unfold");
@@ -1587,15 +1646,15 @@ void initialize_rewrite_tactic() {
                                 });
     register_tac(rewrite_tac_name,
                  [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
-                     buffer<expr> args;
-                     get_tactic_expr_list_elements(app_arg(e), args, "invalid 'rewrite' tactic, invalid argument");
-                     for (expr const & arg : args) {
-                         if (!is_rewrite_step(arg) && !is_rewrite_unfold_step(arg) &&
-                             !is_rewrite_reduce_step(arg) && !is_rewrite_fold_step(arg))
-                             throw expr_to_tactic_exception(e, "invalid 'rewrite' tactic, invalid argument");
-                     }
-                     bool fail_if_metavars = true;
-                     return then(mk_rewrite_tactic(elab, args), try_tactic(refl_tactic(elab, fail_if_metavars)));
+                     return mk_rewrite_tactic(elab, e, false, false);
+                 });
+    register_tac(name{"tactic", "xrewrite_tac"},
+                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                     return mk_rewrite_tactic(elab, e, true, false);
+                 });
+    register_tac(name{"tactic", "krewrite_tac"},
+                 [](type_checker &, elaborate_fn const & elab, expr const & e, pos_info_provider const *) {
+                     return mk_rewrite_tactic(elab, e, true, true);
                  });
 }
 
@@ -1604,6 +1663,8 @@ void finalize_rewrite_tactic() {
     delete g_rewriter_syntactic;
     delete g_rewriter_trace;
     delete g_rewrite_tac;
+    delete g_krewrite_tac;
+    delete g_xrewrite_tac;
     delete g_rewrite_reduce_name;
     delete g_rewrite_reduce_opcode;
     delete g_rewrite_unfold_name;

src/library/tactic/rewrite_tactic.h

@@ -23,6 +23,8 @@ bool is_rewrite_step(expr const & e);
 
 /** \brief Create a rewrite tactic expression, where elems was created using \c mk_rewrite_* procedures. */
 expr mk_rewrite_tactic_expr(buffer<expr> const & elems);
+expr mk_xrewrite_tactic_expr(buffer<expr> const & elems);
+expr mk_krewrite_tactic_expr(buffer<expr> const & elems);
 
 void initialize_rewrite_tactic();
 void finalize_rewrite_tactic();

tests/lean/run/511a.lean

@@ -0,0 +1,14 @@
+import data.nat
+open nat
+
+example (a b : nat) (f : nat → nat) (h : f (succ a) = 0) : f (a+1) = 0 :=
+by rewrite [add_one, h]
+
+example (a b : nat) (f : nat → nat) (h : f (succ a) = 0) : f (a+1) = 0 :=
+by xrewrite h
+
+definition g (a : nat) := a + 1
+definition h (a : nat) := a
+
+example (a b : nat) (f : nat → nat) (h : f (g (h a)) = 0) : f (a+1) = 0 :=
+by krewrite h