fix(tactic/ring): fix loop in ring (#5711)

This occurs because when we name the atoms in `A * B = 2`, `A` is the
first and `B` is the second, and once we put it in horner form it ends up
as `B * A = 2`; but then when we go to rewrite it again `B` is named atom
number 1 and `A` is atom number 2, so we write it the other way around
and end up back at `A * B = 2`. The solution implemented here is to
retain the atom map across calls to `ring.eval` while simp is driving
it, so we end up rewriting it to `B * A = 2` in the first place but in the
second pass we still think `B` is the second atom so we stick with the
`B * A` order.

Fixes #2672

src/analysis/special_functions/trigonometric.lean

@@ -2340,17 +2340,13 @@ by rw exp_mul_I; simp
 theorem cos_eq_zero_iff {θ : ℂ} : cos θ = 0 ↔ ∃ k : ℤ, θ = (2 * k + 1) * π / 2 :=
 begin
   have h : (exp (θ * I) + exp (-θ * I)) / 2 = 0 ↔ exp (2 * θ * I) = -1,
-  { rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 (by norm_num), zero_mul, add_eq_zero_iff_eq_neg,
-        neg_eq_neg_one_mul (exp (-θ * I)), ← div_eq_iff (exp_ne_zero (-θ * I)), ← exp_sub],
-    field_simp, ring },
-  rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int],
-  split; simp; intros x h2; use x,
-  { field_simp, ring at h2,
-    rwa [mul_right_comm 2 I θ, mul_right_comm (2*(x:ℂ)+1) I (π:ℂ), mul_left_inj' I_ne_zero,
-        mul_comm 2 θ] at h2},
-  { field_simp at h2, ring,
-    rw [mul_right_comm 2 I θ, mul_right_comm (2*(x:ℂ)+1) I (π:ℂ), mul_left_inj' I_ne_zero,
-        mul_comm 2 θ, h2] },
+  { rw [@div_eq_iff _ _ (exp (θ * I) + exp (-θ * I)) 2 0 two_ne_zero', zero_mul,
+      add_eq_zero_iff_eq_neg, neg_eq_neg_one_mul, ← div_eq_iff (exp_ne_zero _), ← exp_sub],
+    field_simp only, congr' 3, ring },
+  rw [cos, h, ← exp_pi_mul_I, exp_eq_exp_iff_exists_int, mul_right_comm],
+  refine exists_congr (λ x, _),
+  refine (iff_of_eq $ congr_arg _ _).trans (mul_right_inj' $ mul_ne_zero two_ne_zero' I_ne_zero),
+  ring,
 end
 
 theorem cos_ne_zero_iff {θ : ℂ} : cos θ ≠ 0 ↔ ∀ k : ℤ, θ ≠ (2 * k + 1) * π / 2 :=

src/data/pnat/xgcd.lean

@@ -270,12 +270,12 @@ def gcd_a' : ℕ+ := succ_pnat ((xgcd a b).wp + (xgcd a b).x)
 def gcd_b' : ℕ+ := succ_pnat ((xgcd a b).y + (xgcd a b).zp)
 
 theorem gcd_a'_coe : ((gcd_a' a b) : ℕ) = (gcd_w a b) + (gcd_x a b) :=
-by { dsimp [gcd_a', gcd_w, xgcd_type.w],
-     rw [nat.succ_eq_add_one, nat.succ_eq_add_one], ring }
+by { dsimp [gcd_a', gcd_x, gcd_w, xgcd_type.w],
+     rw [nat.succ_eq_add_one, nat.succ_eq_add_one, add_right_comm] }
 
 theorem gcd_b'_coe : ((gcd_b' a b) : ℕ) = (gcd_y a b) + (gcd_z a b) :=
-by { dsimp [gcd_b', gcd_z, xgcd_type.z],
-     rw [nat.succ_eq_add_one, nat.succ_eq_add_one], ring }
+by { dsimp [gcd_b', gcd_y, gcd_z, xgcd_type.z],
+     rw [nat.succ_eq_add_one, nat.succ_eq_add_one, add_assoc] }
 
 theorem gcd_props :
  let d := gcd_d a b,

src/tactic/ring.lean

@@ -59,8 +59,10 @@ meta def add_atom (e : expr) : ring_m ℕ :=
 /-- Lift a tactic into the `ring_m` monad. -/
 @[inline] meta def lift {α} (m : tactic α) : ring_m α := reader_t.lift m
 
-/-- Run a `ring_m` tactic in the tactic monad. -/
-meta def ring_m.run (red : transparency) (e : expr) {α} (m : ring_m α) : tactic α :=
+/-- Run a `ring_m` tactic in the tactic monad. This version of `ring_m.run` uses an external
+atoms ref, so that subexpressions can be named across multiple `ring_m` calls. -/
+meta def ring_m.run' (red : transparency) (atoms : ref (buffer expr))
+  (e : expr) {α} (m : ring_m α) : tactic α :=
 do α ← infer_type e,
    u ← mk_meta_univ,
    infer_type α >>= unify (expr.sort (level.succ u)),
@@ -70,9 +72,12 @@ do α ← infer_type e,
    nc ← mk_instance_cache `(ℕ),
    using_new_ref ic $ λ r,
    using_new_ref nc $ λ nr,
-   using_new_ref mk_buffer $ λ atoms,
    reader_t.run m ⟨α, u, c, red, r, nr, atoms⟩
 
+/-- Run a `ring_m` tactic in the tactic monad. -/
+meta def ring_m.run (red : transparency) (e : expr) {α} (m : ring_m α) : tactic α :=
+using_new_ref mk_buffer $ λ atoms, ring_m.run' red atoms e m
+
 /-- Lift an instance cache tactic (probably from `norm_num`) to the `ring_m` monad. This version
 is abstract over the instance cache in question (either the ring `α`, or `ℕ` for exponents). -/
 @[inline] meta def ic_lift' (icf : cache → ref instance_cache) {α}
@@ -500,8 +505,9 @@ meta def eval : expr → ring_m (horner_expr × expr)
 
 /-- Evaluate a ring expression `e` recursively to normal form, together with a proof of
 equality. -/
-meta def eval' (red : transparency) (e : expr) : tactic (expr × expr) :=
-ring_m.run red e $ do (e', p) ← eval e, return (e', p)
+meta def eval' (red : transparency) (atoms : ref (buffer expr))
+  (e : expr) : tactic (expr × expr) :=
+ring_m.run' red atoms e $ do (e', p) ← eval e, return (e', p)
 
 theorem horner_def' {α} [comm_semiring α] (a x n b) : @horner α _ a x n b = x ^ n * a + b :=
 by simp [horner, mul_comm]
@@ -543,7 +549,9 @@ instance : inhabited normalize_mode := ⟨normalize_mode.horner⟩
     This results in terms like `(3 * x ^ 2 * y + 1) * x + y`.
   * `SOP` means sum of products form, expanding everything to monomials.
     This results in terms like `3 * x ^ 3 * y + x + y`. -/
-meta def normalize (red : transparency) (mode := normalize_mode.horner) (e : expr) : tactic (expr × expr) := do
+meta def normalize (red : transparency) (mode := normalize_mode.horner) (e : expr) :
+  tactic (expr × expr) :=
+using_new_ref mk_buffer $ λ atoms, do
 pow_lemma ← simp_lemmas.mk.add_simp ``pow_one,
 let lemmas := match mode with
 | normalize_mode.SOP :=
@@ -559,10 +567,10 @@ lemmas ← lemmas.mfoldl simp_lemmas.add_simp simp_lemmas.mk,
 (_, e', pr) ← ext_simplify_core () {}
   simp_lemmas.mk (λ _, failed) (λ _ _ _ _ e, do
     (new_e, pr) ← match mode with
-    | normalize_mode.raw := eval' red
-    | normalize_mode.horner := trans_conv (eval' red) (simplify lemmas [])
+    | normalize_mode.raw := eval' red atoms
+    | normalize_mode.horner := trans_conv (eval' red atoms) (simplify lemmas [])
     | normalize_mode.SOP :=
-      trans_conv (eval' red) $
+      trans_conv (eval' red atoms) $
       trans_conv (simplify lemmas []) $
       simp_bottom_up' (λ e, norm_num.derive e <|> pow_lemma.rewrite e)
     end e,

test/ring.lean

@@ -50,3 +50,6 @@ begin
   field_simp,
   ring
 end
+
+-- this proof style is not recommended practice
+example (A B : ℕ) (H : B * A = 2) : A * B = 2 := by {ring, exact H}