fix(tactic/ring_exp): ring_exp now recognizes that `2^(n+1+1) = 2 *…

… 2^(n+1)` (#2929)

[Zulip thread with bug report](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ring_exp.20needs.20ring).

The problem was a missing lemma so that `norm_num` could fire on `x^y` if `x` and `y` are coefficients.

src/tactic/ring_exp.lean

@@ -965,6 +965,18 @@ lemma pow_e_pf_exp {pps p : α} {ps qs psqs : ℕ} :
   ... = p ^ (ps * qs) : symm (pow_mul _ _ _)
   ... = p ^ psqs : by rw [psqs_pf]
 
+/--
+Compute the exponentiation of two coefficients.
+
+The returned value is of the form `ex.coeff _ (p ^ q)`,
+with the proof of `expr.of_rat p ^ expr.of_rat q = expr.of_rat (p ^ q)`.
+-/
+meta def pow_coeff (p_p q_p : expr) (p q : coeff) : ring_exp_m (ex prod) := do
+  ctx ← get_context,
+  pq' ← mk_pow [p_p, q_p],
+  (pq_p, pq_pf) ← lift $ norm_num.derive' pq',
+  pure $ ex.coeff ⟨pq_p, pq_p, pq_pf⟩ ⟨p.1 * q.1⟩
+
 /--
 Exponentiate two expressions.
 
@@ -983,6 +995,9 @@ meta def pow_e : ex exp → ex prod → ring_exp_m (ex exp)
 lemma pow_pp_pf_one {ps : α} {qs : ℕ} : ps = 1 → ps ^ qs = 1 :=
 λ ps_pf, by rw [ps_pf, _root_.one_pow]
 
+lemma pow_pf_c_c {ps ps' pq : α} {qs qs' : ℕ} :
+  ps = ps' → qs = qs' → ps' ^ qs' = pq → ps ^ qs = pq := by cc
+
 lemma pow_pp_pf_c {ps ps' pqs : α} {qs qs' : ℕ} :
   ps = ps' → qs = qs' → ps' ^ qs' = pqs → ps ^ qs = pqs * 1 :=
 by simp; cc
@@ -1007,6 +1022,13 @@ meta def pow_pp : ex prod → ex prod → ring_exp_m (ex prod)
   o_o ← pow_orig ps qs,
   pf ← mk_proof ``pow_pp_pf_one [ps.orig, qs.orig] [ps.info],
   pure $ o.set_info o_o pf
+| ps@(ex.coeff ps_i x) qs@(ex.coeff qs_i y) := do
+  pq ← pow_coeff ps.pretty qs.pretty x y,
+  pq_o ← pow_orig ps qs,
+  pf ← mk_proof_or_refl pq.pretty ``pow_pf_c_c
+    [ps.orig, ps.pretty, pq.pretty, qs.orig, qs.pretty]
+    [ps.info, qs.info, pq.info],
+  pure $ pq.set_info pq_o pf
 | ps@(ex.coeff ps_i x) qs := do
   ps'' ← pure ps >>= prod_to_sum >>= ex_sum_b,
   pqs ← ex_exp ps'' qs,

test/ring_exp.lean

@@ -69,6 +69,10 @@ example {α} [comm_ring α] (k : ℕ) (x y z : α) :
 
 -- We can represent a large exponent `n` more efficiently than just `n` multiplications:
 example (a b : ℚ) : (a * b) ^ 1000000 = (b * a) ^ 1000000 := by ring_exp
+
+example (n : ℕ) : 2 ^ (n + 1 + 1)  = 2 * 2 ^ (n + 1) :=
+by ring_exp_eq
+
 end exponentiation
 
 section power_of_sum