feat(library/init/meta/rewrite_tactic): improve rewrite tactic

`rewrite` tactic improvements
- Add support for `auto_param` and `opt_param`
- Order new goals using the same strategies available for `apply`
- Allow user to set configuration object in interactive mode.

@Armael This commit should address the issue you raised about the order
of new goals in the `rewrite` tactic.
See new test tests/lean/run/rw1.lean for examples.

doc/changes.md

@@ -38,7 +38,10 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 
 * `assume` and `suppose` are now real tactics that do not exit tactic mode.
 
-* Modified `apply` tactic configuration object, and implemented [RFC #1342](https://github.com/leanprover/lean/issues/1342). It also has support for `auto_param` and `opt_param`. The new `eapply` tactic only creates subgoals for non dependent premises, and it simulates the behavior of the `apply` tactic in version 3.2.0.
+* Modified `apply` tactic configuration object, and implemented [RFC #1342](https://github.com/leanprover/lean/issues/1342). It now has support for `auto_param` and `opt_param`. The new `eapply` tactic only creates subgoals for non dependent premises, and it simulates the behavior of the `apply` tactic in version 3.2.0.
+
+* Add configuration object `rewrite_cfg` to `rw`/`rewrite` tactic. It now has support for `auto_param` and `opt_param`.
+  The new goals are ordered using the same strategies available for `apply`.
 
 v3.2.0 (18 June 2017)
 -------------

library/init/meta/interactive.lean

@@ -309,27 +309,26 @@ match r.rule with
 | _                   := return []
 end
 
-private meta def rw_goal (m : transparency) (rs : list rw_rule) : tactic unit :=
+private meta def rw_goal (cfg : rewrite_cfg) (rs : list rw_rule) : tactic unit :=
 rs.mfor' $ λ r, do
  save_info r.pos,
  eq_lemmas ← get_rule_eqn_lemmas r,
  orelse'
-   (to_expr' r.rule >>= rewrite_core m tt tt occurrences.all r.symm)
-   (eq_lemmas.mfirst $ λ n, mk_const n >>= rewrite_core m tt tt occurrences.all r.symm)
+   (do e ← to_expr' r.rule, rewrite_target e {cfg with symm := r.symm})
+   (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_target e {cfg with symm := r.symm})
    (eq_lemmas.empty)
 
-private meta def rw_hyp (m : transparency) (rs : list rw_rule) (hname : name) : tactic unit :=
+private meta def rw_hyp (cfg : rewrite_cfg) (rs : list rw_rule) (hname : name) : tactic unit :=
 rs.mfor' $ λ r,
-do h ← get_local hname,
-   save_info r.pos,
+do save_info r.pos,
    eq_lemmas ← get_rule_eqn_lemmas r,
    orelse'
-     (do e ← to_expr' r.rule, rewrite_at_core m tt tt occurrences.all r.symm e h)
-     (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_at_core m tt tt occurrences.all r.symm e h)
+     (do e ← to_expr' r.rule, rewrite_hyp e hname {cfg with symm := r.symm})
+     (eq_lemmas.mfirst $ λ n, do e ← mk_const n, rewrite_hyp e hname {cfg with symm := r.symm})
      (eq_lemmas.empty)
 
-private meta def rw_hyps (m : transparency) (rs : list rw_rule) (hs : list name) : tactic unit :=
-hs.mfor' (rw_hyp m rs)
+private meta def rw_hyps (cfg : rewrite_cfg) (rs : list rw_rule) (hs : list name) : tactic unit :=
+hs.mfor' (rw_hyp cfg rs)
 
 meta def rw_rule_p (ep : parser pexpr) : parser rw_rule :=
 rw_rule.mk <$> cur_pos <*> (option.is_some <$> (tk "-")?) <*> ep
@@ -348,29 +347,29 @@ meta def rw_rules : parser rw_rules_t :=
                <*> (some <$> cur_pos <* set_goal_info_pos (tk "]")))
 <|> rw_rules_t.mk <$> (list.ret <$> rw_rule_p texpr) <*> return none
 
-private meta def rw_core (m : transparency) (rs : parse rw_rules) (loca : parse location) : tactic unit :=
+private meta def rw_core (rs : parse rw_rules) (loca : parse location) (cfg : rewrite_cfg) : tactic unit :=
 match loca with
 | loc.wildcard := fail "wildcard not allowed with rewrite"
-| loc.ns []    := rw_goal m rs.rules
-| loc.ns hs    := rw_hyps m rs.rules hs
+| loc.ns []    := rw_goal cfg rs.rules
+| loc.ns hs    := rw_hyps cfg rs.rules hs
 end >> try (reflexivity reducible)
     >> (returnopt rs.end_pos >>= save_info <|> skip)
 
-meta def rewrite : parse rw_rules → parse location → tactic unit :=
-rw_core reducible
+meta def rewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
+rw_core q l cfg
 
-meta def rw : parse rw_rules → parse location → tactic unit :=
-rewrite
+meta def rw (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
+rw_core q l cfg
 
 /- rewrite followed by assumption -/
-meta def rwa (q : parse rw_rules) (l : parse location) : tactic unit :=
-rewrite q l >> try assumption
+meta def rwa (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {}) : tactic unit :=
+rewrite q l cfg >> try assumption
 
-meta def erewrite : parse rw_rules → parse location → tactic unit :=
-rw_core semireducible
+meta def erewrite (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {md := semireducible}) : tactic unit :=
+rw_core q l cfg
 
-meta def erw : parse rw_rules → parse location → tactic unit :=
-erewrite
+meta def erw (q : parse rw_rules) (l : parse location) (cfg : rewrite_cfg := {md := semireducible}) : tactic unit :=
+rw_core q l cfg
 
 private meta def get_type_name (e : expr) : tactic name :=
 do e_type ← infer_type e >>= whnf,

library/init/meta/rewrite_tactic.lean

@@ -7,18 +7,38 @@ prelude
 import init.meta.relation_tactics init.meta.occurrences
 
 namespace tactic
-/- (rewrite_core m approx use_instances occs symm H) -/
-meta constant rewrite_core : transparency → bool → bool → occurrences → bool → expr → tactic unit
-meta constant rewrite_at_core : transparency → bool → bool → occurrences → bool → expr → expr → tactic unit
+/-- Configuration options for the `rewrite` tactic. -/
+structure rewrite_cfg extends apply_cfg :=
+(md            := reducible)
+(symm          := ff)
+(occs          := occurrences.all)
 
-meta def rewrite (th_name : name) : tactic unit :=
-do th ← mk_const th_name,
-   rewrite_core reducible tt tt occurrences.all ff th,
-   try (reflexivity reducible)
+/-- Rewrite the expression `e` using `h`.
+    The unification is performed using the transparency mode in `cfg`.
+    If `cfg.approx` is `tt`, then fallback to first-order unification, and approximate context during unification.
+    `cfg.new_goals` specifies which unassigned metavariables become new goals, and their order.
+    If `cfg.instances` is `tt`, then use type class resolution to instantiate unassigned meta-variables.
+    The fields `cfg.auto_param` and `cfg.opt_param` are ignored by this tactic (See `tactic.rewrite`).
+    It a triple `(new_e, prf, metas)` where `prf : e = new_e`, and `metas` is a list of all introduced meta variables,
+    even the assigned ones.
 
-meta def rewrite_at (th_name : name) (H_name : name) : tactic unit :=
-do th ← mk_const th_name,
-   H  ← get_local H_name,
-   rewrite_at_core reducible tt tt occurrences.all ff th H
+    TODO(Leo): improve documentation and explain symm/occs -/
+meta constant rewrite_core (h : expr) (e : expr) (cfg : rewrite_cfg := {}) : tactic (expr × expr × list expr)
+
+meta def rewrite (h : expr) (e : expr) (cfg : rewrite_cfg := {}) : tactic (expr × expr × list expr) :=
+do (new_t, prf, metas) ← rewrite_core h e cfg,
+   try_apply_opt_auto_param cfg.to_apply_cfg metas,
+   return (new_t, prf, metas)
+
+meta def rewrite_target (h : expr) (cfg : rewrite_cfg := {}) : tactic unit :=
+do t ← target,
+   (new_t, prf, _) ← rewrite h t cfg,
+   replace_target new_t prf
+
+meta def rewrite_hyp (h : expr) (hyp_name : name) (cfg : rewrite_cfg := {}) : tactic expr :=
+do hyp ← get_local hyp_name,
+   hyp_type ← infer_type hyp,
+   (new_hyp_type, prf, _) ← rewrite h hyp_type cfg,
+   replace_hyp hyp new_hyp_type prf
 
 end tactic

library/init/meta/simp_tactic.lean

@@ -246,14 +246,6 @@ meta def simplify (S : simp_lemmas) (e : expr) (cfg : simp_config := {}) : tacti
 do e_type       ← infer_type e >>= whnf,
    simplify_core cfg S `eq e
 
-meta def replace_target (new_target : expr) (pr : expr) : tactic unit :=
-do t ← target,
-   assert `htarget new_target, swap,
-   ht        ← get_local `htarget,
-   eq_type   ← mk_app `eq [t, new_target],
-   locked_pr ← return $ expr.app (expr.app (expr.const ``id_locked [level.zero]) eq_type) pr,
-   mk_eq_mpr locked_pr ht >>= exact
-
 meta def simplify_goal (S : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
 do t ← target,
    (new_t, pr) ← simplify S t cfg,

library/init/meta/tactic.lean

@@ -833,7 +833,7 @@ ms.mfoldl
             return $ r || type.is_napp_of `opt_param 2 || type.is_napp_of `auto_param 2)
  ff
 
-private meta def try_apply_opt_auto_param (cfg : apply_cfg) (ms : list expr) : tactic unit :=
+meta def try_apply_opt_auto_param (cfg : apply_cfg) (ms : list expr) : tactic unit :=
 when (cfg.auto_param || cfg.opt_param) $
 mwhen (has_opt_auto_param ms) $ do
   gs ← get_goals,
@@ -1168,3 +1168,14 @@ meta instance : monad task :=
 {map := @task.map, bind := @task.bind, pure := @task.pure,
  id_map := undefined, pure_bind := undefined, bind_assoc := undefined,
  bind_pure_comp_eq_map := undefined}
+
+namespace tactic
+meta def replace_target (new_target : expr) (pr : expr) : tactic unit :=
+do t ← target,
+   assert `htarget new_target, swap,
+   ht        ← get_local `htarget,
+   eq_type   ← mk_app `eq [t, new_target],
+   locked_pr ← return $ expr.app (expr.app (expr.const ``id_locked [level.zero]) eq_type) pr,
+   mk_eq_mpr locked_pr ht >>= exact
+
+end tactic

src/library/tactic/apply_tactic.cpp

@@ -45,7 +45,7 @@ static unsigned get_expect_num_args(type_context & ctx, expr e) {
     }
 }
 
-bool try_instance(type_context & ctx, expr const & meta, tactic_state const & s, vm_obj * out_error_obj, char const * tac_name) {
+static bool try_instance(type_context & ctx, expr const & meta, tactic_state const & s, vm_obj * out_error_obj, char const * tac_name) {
     if (ctx.is_assigned(meta))
         return true;
     expr meta_type      = ctx.instantiate_mvars(ctx.infer(meta));
@@ -77,10 +77,22 @@ bool try_instance(type_context & ctx, expr const & meta, tactic_state const & s,
     return true;
 }
 
+bool synth_instances(type_context & ctx, buffer<expr> const & metas, buffer<bool> const & is_instance,
+                     tactic_state const & s, vm_obj * out_error_obj, char const * tac_name) {
+    unsigned i = is_instance.size();
+    while (i > 0) {
+        --i;
+        if (!is_instance[i]) continue;
+        if (!try_instance(ctx, metas[i], s, out_error_obj, tac_name))
+            return false;
+    }
+    return true;
+}
+
 /** \brief Given a sequence metas/goals: <tt>(?m_1 ...) (?m_2 ... ) ... (?m_k ...)</tt>,
     we say ?m_i is "redundant" if it occurs in the type of some ?m_j.
     This procedure removes from metas any redundant element. */
-void remove_dep_goals(type_context & ctx, buffer<expr> & metas) {
+static void remove_dep_goals(type_context & ctx, buffer<expr> & metas) {
     unsigned k = 0;
     for (unsigned i = 0; i < metas.size(); i++) {
         bool found = false;
@@ -100,7 +112,7 @@ void remove_dep_goals(type_context & ctx, buffer<expr> & metas) {
     metas.shrink(k);
 }
 
-void reorder_non_dep_first(type_context & ctx, buffer<expr> & metas) {
+static void reorder_non_dep_first(type_context & ctx, buffer<expr> & metas) {
     buffer<expr> non_dep, dep;
     for (unsigned i = 0; i < metas.size(); i++) {
         bool found = false;
@@ -123,6 +135,25 @@ void reorder_non_dep_first(type_context & ctx, buffer<expr> & metas) {
     metas.append(dep);
 }
 
+void collect_new_goals(type_context & ctx, new_goals_kind k, buffer<expr> const & metas, buffer<expr> & new_goals) {
+    for (auto m : metas) {
+        if (!ctx.is_assigned(m)) {
+            ctx.instantiate_mvars_at_type_of(m);
+            new_goals.push_back(m);
+        }
+    }
+    switch (k) {
+    case new_goals_kind::NonDepFirst:
+        reorder_non_dep_first(ctx, new_goals);
+        break;
+    case new_goals_kind::NonDepOnly:
+        remove_dep_goals(ctx, new_goals);
+        break;
+    case new_goals_kind::All:
+        break; /* do nothing */
+    }
+}
+
 static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const & cfg, tactic_state const & s,
                                     vm_obj * out_error_obj, list<expr> * new_metas) {
     optional<metavar_decl> g = s.get_main_goal_decl();
@@ -163,33 +194,11 @@ static optional<tactic_state> apply(type_context & ctx, expr e, apply_cfg const
         return none_tactic_state();
     }
     /* Synthesize type class instances */
-    if (cfg.m_instances) {
-        unsigned i = is_instance.size();
-        while (i > 0) {
-            --i;
-            if (!is_instance[i]) continue;
-            if (!try_instance(ctx, metas[i], s, out_error_obj, "apply"))
-                return none_tactic_state();
-        }
-    }
+    if (cfg.m_instances && !synth_instances(ctx, metas, is_instance, s, out_error_obj, "apply"))
+        return none_tactic_state();
     /* Collect unassigned meta-variables */
     buffer<expr> new_goals;
-    for (auto m : metas) {
-        if (!ctx.is_assigned(m)) {
-            ctx.instantiate_mvars_at_type_of(m);
-            new_goals.push_back(m);
-        }
-    }
-    switch (cfg.m_new_goals) {
-    case new_goals_kind::NonDepFirst:
-        reorder_non_dep_first(ctx, new_goals);
-        break;
-    case new_goals_kind::NonDepOnly:
-        remove_dep_goals(ctx, new_goals);
-        break;
-    case new_goals_kind::All:
-        break; /* do nothing */
-    }
+    collect_new_goals(ctx, cfg.m_new_goals, metas, new_goals);
     metavar_context mctx = ctx.mctx();
     /* Assign, and create new tactic_state */
     e = mctx.instantiate_mvars(e);

src/library/tactic/apply_tactic.h

@@ -34,6 +34,12 @@ struct apply_cfg {
 optional<tactic_state> apply(type_context & ctx, expr const & e, apply_cfg const & cfg, tactic_state const & s);
 /* For backward compatibility */
 optional<tactic_state> apply(type_context & ctx, bool all, bool use_instances, expr const & e, tactic_state const & s);
+
+/* Helper functions */
+bool synth_instances(type_context & ctx, buffer<expr> const & metas, buffer<bool> const & is_instance,
+                     tactic_state const & s, vm_obj * out_error_obj, char const * tac_name);
+void collect_new_goals(type_context & ctx, new_goals_kind k, buffer<expr> const & metas, buffer<expr> & new_goals);
+
 void initialize_apply_tactic();
 void finalize_apply_tactic();
 }