feat(tactic/ring_exp): handle nat.succ p as p + 1 (#5166)

Fixes: #5157 

This PR adds a `rewrite` operation to `ring_exp`, which takes a normalized `p' : ex sum` and a proof that `p = p'.orig`, and shows `p` also normalizes to `p'.pretty`. The only use currently is `nat.succ`. If we still had `nat.has_pow`, the same function could have handled rewriting from `nat.has_pow` to `monoid.has_pow`.

src/tactic/ring_exp.lean

@@ -658,6 +658,34 @@ match p.1, q.1 with -- Special case to speed up multiplication with 1.
   pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩
 end
 
+section rewrite
+
+/-! ### `rewrite` section
+
+In this section we deal with rewriting terms to fit in the basic grammar of `eval`.
+For example, `nat.succ n` is rewritten to `n + 1` before it is evaluated further.
+-/
+
+/-- Given a proof that the expressions `ps_o` and `ps'.orig` are equal,
+show that `ps_o` and `ps'.pretty` are equal.
+
+Useful to deal with aliases in `eval`. For instance, `nat.succ p` can be handled
+as an alias of `p + 1` as follows:
+```
+| ps_o@`(nat.succ %%p_o) := do
+  ps' ← eval `(%%p_o + 1),
+  pf ← lift $ mk_app ``nat.succ_eq_add_one [p_o],
+  rewrite ps_o ps' pf
+```
+-/
+meta def rewrite (ps_o : expr) (ps' : ex sum) (pf : expr) : ring_exp_m (ex sum) :=
+do
+  ps'_pf ← ps'.info.proof_term,
+  pf ← lift $ mk_eq_trans pf ps'_pf,
+  pure $ ps'.set_info ps_o pf
+
+end rewrite
+
 /--
 Represents the way in which two products are equal except coefficient.
 
@@ -807,6 +835,7 @@ meta def add : ex sum → ex sum → ring_exp_m (ex sum)
       [qqs.info, pqs.info],
     pure $ pqqs.set_info ppqqs_o pf
   end
+
 end addition
 
 section multiplication
@@ -1336,6 +1365,10 @@ meta def eval : expr → ring_exp_m (ex sum)
   ps' ← eval ps,
   qs' ← eval qs,
   add ps' qs'
+| ps_o@`(nat.succ %%p_o) := do
+  ps' ← eval `(%%p_o + 1),
+  pf ← lift $ mk_app ``nat.succ_eq_add_one [p_o],
+  rewrite ps_o ps' pf
 | e@`(%%ps - %%qs) := (do
   ctx ← get_context,
   ri ← match ctx.info_b.ring_instance with

test/ring_exp.lean

@@ -1,4 +1,5 @@
 import tactic.ring_exp
+import tactic.zify
 import algebra.group_with_zero.power
 
 universes u
@@ -139,6 +140,13 @@ begin
 end
 end complicated
 
+-- Test that `nat.succ d` gets handled as `d + 1`.
+example (d : ℕ) : 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 :=
+begin
+  zify [nat.one_le_pow'],
+  ring_exp,
+end
+
 section conv
 /-!
   ### `conv` section