non-idempotence of ring (when following zify)

[robertylewis]

import tactic.ring tactic.zify

open tactic 

example (a b c : ℕ) (h : b + a < c + a) : b < c :=
begin 
  zify at h,
  rw ← sub_lt_sub_iff_right (a : ℤ) at h,
  ring at h, -- this line succeeds, but doesn't cancel the `a`s
  ring at h, -- this also succeeds and cancels the `a`s
end 

I assumed at first this was another uninstantiated mvar bug, but surprisingly, it doesn't seem to be. The first ring changes some type class instances but doesn't go any further.

I couldn't replicate it without zify and the rw. In particular, manually inserting casts at the beginning makes the problem go away.

@digama0 any instinct here? Maybe zify is bringing in some non-canonical type class instances somehow, but I'm still not sure how/where this interferes with ring.

[eric-wieser]

I wonder if this has the same cause as https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.60simp.60.20is.20not.20idempotent

[bryangingechen]

Here's another example where ring is non-idempotent:

import analysis.special_functions.pow
example : 3 * real.pi = (1 : ℤ) * (2 * real.pi) + real.pi := 
-- by norm_cast; ring
begin
  ring,
  -- ⊢ 3 * real.pi = 2 * real.pi * ↑1 + real.pi
  ring,
  -- ⊢ 3 * real.pi = (2 * ↑1 + 1) * real.pi
  ring,
  -- ⊢ 3 * real.pi = 2 * real.pi * ↑1 + real.pi
  ring,
  -- ⊢ 3 * real.pi = (2 * ↑1 + 1) * real.pi
end

Edit: This is expected since this kind of goal is out-of-scope for ring: see Zulip.

[robertylewis]

This seems to have solved itself:

import tactic.ring tactic.zify

open tactic 

example (a b c : ℕ) (h : b + a < c + a) : b < c :=
begin 
  zify at h,
  rw ← sub_lt_sub_iff_right (a : ℤ) at h,
  ring_nf at h,
end