A ring_exp tactic for dealing with exponents in rings (#1715)

* Test for ring_exp

* Implement -a/b * -a/b = a/b * a/b

* Hide extra information in the `ex` type in `ex_info`

* Some attempts to make the proof returned by ring_exp shorter

* Fix that ring_exp wouldn't handle pow that isn't monomial.has_pow

* Some optimizations in ring_exp

* Make all proofs explicit, halving execution time more or less

* Cache `has_add` and `has_mul` instances for another 2x speedup

* ring_exp can replace ring to compile mathlib

* Revert `ring` to non-test version

* Code cleanup and documentation

* Revert the test changes to `linarith`

* Undo the test changes to `ring2`

* Whitespace cleanup

* Fix overzealous error handling

Instead of catching any `fail` in eval, we just catch the operations that can
safely `fail` (i.e. `invert` and `negate`). This should make internal errors
visible again.

* Fix the TODO's

* Example use of ring_exp in data.polynomial

* Check that `ring_exp` deals well with natural number subtraction

* Fix incorrect docstring

* Improve documentation

* Small stylistic fixes

* Fix slow behaviour on large exponents

* Add `ring_exp` to the default tactics

* Use applicative notation where appropriate

* The `ring_exp` tactic also does normalization

Co-Authored-By: Rob Lewis <Rob.y.lewis@gmail.com>

* Move `normalize` from `tactic.interactive` to `ring_exp` namespace

* Fix name collision between `equiv` in data.equiv.basic and `equiv` in `test/tactics.lean`

I just renamed the definition in `test/tactics.lean` to `my_equiv`
and the operator to `my≅`.

* Fixes for the linter

* Fix the usage of type classes for `sub_pf` and `div_pf`

* Fix an additional linting error

* Optimization: we don't need norm_num to determine `x * 1 = x`

* Improve documentation of `test/ring_exp.lean`

* Rename `resolve_atoms` to `resolve_atom_aux` for clarity

* Small stylistic fixes

* Remove unneccessary hidden fields to `ex`

* Control how much unfolding `ring_exp` does by putting a `!` after it

* Reword comment for `ex_type`

* Use `ring_exp!` to deal with `(n : ℕ) + 1 - 1 = n`

* Document the `!` flag for `ring`, `ring_exp` and `ring_exp_eq`

* Get rid of searching for another cached instance

* Fix `ring_exp` failing on terms on the form `0^succ (succ ...)`

docs/tactics.md

@@ -191,6 +191,24 @@ by { abel at hyp, exact hyp }
 Evaluate expressions in the language of *commutative* (semi)rings.
 Based on [Proving Equalities in a Commutative Ring Done Right in Coq](http://www.cs.ru.nl/~freek/courses/tt-2014/read/10.1.1.61.3041.pdf) by Benjamin Grégoire and Assia Mahboubi.
 
+The variant `ring!` uses a more aggessive reducibility setting to determine equality of atoms.
+
+### ring_exp
+
+Evaluate expressions in *commutative* (semi)rings, allowing for variables in the exponent.
+
+This tactic extends `ring`: it should solve every goal that `ring` can solve.
+Additionally, it knows how to evaluate expressions with complicated exponents
+(where `ring` only understands constant exponents).
+The variants `ring_exp!` and `ring_exp_eq!` use a more aggessive reducibility setting to determine equality of atoms.
+
+For example:
+```lean
+example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring_exp
+example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring_exp
+example (x y : ℕ) : x + id y = y + id x := by ring_exp!
+```
+
 ### congr'
 
 Same as the `congr` tactic, but takes an optional argument which gives

src/data/polynomial.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes, Johannes Hölzl, Jens Wagemaker
 
 Theory of univariate polynomials, represented as `ℕ →₀ α`, where α is a commutative semiring.
 -/
-import data.finsupp algebra.gcd_domain ring_theory.euclidean_domain tactic.ring ring_theory.multiplicity
+import data.finsupp algebra.gcd_domain ring_theory.euclidean_domain tactic.ring_exp ring_theory.multiplicity
 
 noncomputable theory
 local attribute [instance, priority 100] classical.prop_decidable
@@ -2387,10 +2387,11 @@ def pow_add_expansion {α : Type*} [comm_semiring α] (x y : α) : ∀ (n : ℕ)
 | (n+2) :=
   begin
     cases pow_add_expansion (n+1) with z hz,
-    rw [_root_.pow_succ, hz],
-    existsi (x*z + (n+1)*x^n+z*y),
-    simp [_root_.pow_succ],
-    ring
+    existsi x*z + (n+1)*x^n+z*y,
+    calc (x + y) ^ (n + 2) = (x + y) * (x + y) ^ (n + 1) : by ring_exp
+    ... = (x + y) * (x ^ (n + 1) + ↑(n + 1) * x ^ (n + 1 - 1) * y + z * y ^ 2) : by rw hz
+    ... = x ^ (n + 2) + ↑(n + 2) * x ^ (n + 1) * y + (x*z + (n+1)*x^n+z*y) * y ^ 2 :
+      by { push_cast, ring_exp! }
   end
 
 variables [comm_ring α]
@@ -2432,12 +2433,12 @@ def pow_sub_pow_factor (x y : α) : Π {i : ℕ},{z : α // x^i - y^i = z*(x - y
 | 1 := ⟨1, by simp⟩
 | (k+2) :=
   begin
-    cases pow_sub_pow_factor with z hz,
+    cases @pow_sub_pow_factor (k+1) with z hz,
     existsi z*x + y^(k+1),
-    rw [_root_.pow_succ x, _root_.pow_succ y, ←sub_add_sub_cancel (x*x^(k+1)) (x*y^(k+1)),
-        ←mul_sub x, hz],
-    simp only [_root_.pow_succ],
-    ring
+    calc x ^ (k + 2) - y ^ (k + 2)
+        = x * (x ^ (k + 1) - y ^ (k + 1)) + (x * y ^ (k + 1) - y ^ (k + 2)) : by ring_exp
+    ... = x * (z * (x - y)) + (x * y ^ (k + 1) - y ^ (k + 2)) : by rw hz
+    ... = (z * x + y ^ (k + 1)) * (x - y) : by ring_exp
   end
 
 def eval_sub_factor (f : polynomial α) (x y : α) :

src/tactic/default.lean

@@ -25,6 +25,7 @@ import
   tactic.tidy
   tactic.abel
   tactic.ring
+  tactic.ring_exp
   tactic.linarith
   tactic.omega
   tactic.wlog