fix(tactic/ring): fix loop in ring

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/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,9 @@ begin
   field_simp,
   ring
 end
+
+example (A B : ℕ) : true :=
+begin
+  suffices : A * B = 2, trivial,
+  ring, guard_target B * A = 2, sorry
+end