From 62089341344d9ecff27de17968cbc56035c30105 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 30 Jun 2017 12:41:35 -0700
Subject: [PATCH] feat(library/init/meta/converter/interactive): add support
 for `rw` at `conv` tactical

---
 doc/changes.md                               |  1 +
 library/init/meta/converter/interactive.lean | 25 ++++++++++++++++++++
 library/init/meta/interactive.lean           |  4 ++--
 tests/lean/run/conv_tac1.lean                | 13 ++++++++++
 4 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/doc/changes.md b/doc/changes.md
index f5c2f319a3..d1b2487105 100644
--- a/doc/changes.md
+++ b/doc/changes.md
@@ -25,6 +25,7 @@ master branch (aka work in progress branch)
   Examples:
   - `conv at h in (f _ _) { simp }` applies `simp` to first subterm matching `f _ _` at hypothesis `h`.
   - `conv in (_ = _) { to_lhs, whnf }` replace the left-hand-side of the equality in target with its weak-head-normal-form.
+  - `conv at h in (0 + _) { rw [zero_add] }`
 
 *Changes*
 
diff --git a/library/init/meta/converter/interactive.lean b/library/init/meta/converter/interactive.lean
index 338b0dd845..1ec816db64 100644
--- a/library/init/meta/converter/interactive.lean
+++ b/library/init/meta/converter/interactive.lean
@@ -98,6 +98,31 @@ do s ← tactic.mk_simp_set no_dflt attr_names hs ids,
 meta def guard_lhs (p : parse texpr) : tactic unit :=
 do t ← lhs, tactic.interactive.guard_expr_eq t p
 
+section rw
+open tactic.interactive (rw_rules rw_rule get_rule_eqn_lemmas to_expr')
+open tactic (rewrite_cfg)
+
+private meta def rw_lhs (h : expr) (cfg : rewrite_cfg) : conv unit :=
+do l ← conv.lhs,
+   (new_lhs, prf, _) ← tactic.rewrite h l cfg,
+   update_lhs new_lhs prf
+
+private meta def rw_core (rs : list rw_rule) (cfg : rewrite_cfg) : conv unit :=
+rs.mfor' $ λ r, do
+ save_info r.pos,
+ eq_lemmas ← get_rule_eqn_lemmas r,
+ orelse'
+   (do h ← to_expr' r.rule, rw_lhs h {cfg with symm := r.symm})
+   (eq_lemmas.mfirst $ λ n, do e ← tactic.mk_const n, rw_lhs e {cfg with symm := r.symm})
+   (eq_lemmas.empty)
+
+meta def rewrite (q : parse rw_rules) (cfg : rewrite_cfg := {}) : conv unit :=
+rw_core q.rules cfg
+
+meta def rw (q : parse rw_rules) (cfg : rewrite_cfg := {}) : conv unit :=
+rw_core q.rules cfg
+end rw
+
 end interactive
 end conv
 
diff --git a/library/init/meta/interactive.lean b/library/init/meta/interactive.lean
index b7e994da0c..94a26bce24 100644
--- a/library/init/meta/interactive.lean
+++ b/library/init/meta/interactive.lean
@@ -279,7 +279,7 @@ do {
    This is not an optimization, by skipping the elaborator we make sure that no unwanted resolution is used.
    Example: the elaborator will force any unassigned ?A that must have be an instance of (has_one ?A) to nat.
    Remark: another benefit is that auxiliary temporary metavariables do not appear in error messages. -/
-private meta def to_expr' (p : pexpr) : tactic expr :=
+meta def to_expr' (p : pexpr) : tactic expr :=
 match p with
 | (const c [])          := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
 | (local_const c _ _ _) := do new_e ← resolve_name' c, save_type_info new_e p, return new_e
@@ -294,7 +294,7 @@ meta structure rw_rule :=
 meta instance rw_rule.reflect : has_reflect rw_rule :=
 λ ⟨p, s, r⟩, `(_)
 
-private meta def get_rule_eqn_lemmas (r : rw_rule) : tactic (list name) :=
+meta def get_rule_eqn_lemmas (r : rw_rule) : tactic (list name) :=
 let aux (n : name) : tactic (list name) := do {
   p ← resolve_name n,
   -- unpack local refs
diff --git a/tests/lean/run/conv_tac1.lean b/tests/lean/run/conv_tac1.lean
index f1110458c9..68cf79c812 100644
--- a/tests/lean/run/conv_tac1.lean
+++ b/tests/lean/run/conv_tac1.lean
@@ -62,3 +62,16 @@ begin
   },
   assumption
 end
+
+example (x y : nat) (f : nat → nat) (h : f (0 + x + y) = 0 + y) : f (x + y) = 0 + y :=
+begin
+  -- use conv to rewrite subterm of a hypothesis
+  conv at h in (0 + _) { rw [zero_add] },
+  assumption
+end
+
+example (x : nat) (f : nat → nat) (h₁ : x = 0) (h₂ : ∀ x, f x = x + x) : f x = x :=
+begin
+  conv { to_rhs, rw [h₁, -add_zero 0, -h₁], },
+  exact h₂ x
+end