How "normal" is `ring_nf` normal form?

Stream: maths

[Kevin Buzzard]

import tactic
import data.real.basic

example (a b : ℕ → ℝ) (n : ℕ) (t u : ℝ) (h : 0 < a n - t + (b n - u)) :
  0 < a n + (b n + (-t - u)) :=
begin
  -- convert h using 1, ring, -- I know I can do this
  -- but I want to do the below instead:
  ring_nf, -- succeeds but doesn't seem to do anything
  ring_nf at h, -- randomly moves some brackets around
  /-
  h : 0 < a n + (-t + (b n - u))
  ⊢ 0 < a n + (b n + (-t - u))
  -/
  exact h, -- fails
end

I had thought that the idea of ring_nf was that if it couldn't solve the goal, it would put things into some sort of unique canonical form, making exact h work. Clearly I'm wrong. @Mario Carneiro is this not what ring_nf does?

[Heather Macbeth]

  ring_nf at ⊢ h,
  exact h,

[Heather Macbeth]

As Mario explained to me at some point, it's only canonical within its own tactic-call, so to speak. So you get it to do both at once.

[Kevin Buzzard]

Oh this is great! Thanks! I was worried that it might be one of those "fixed in this PR which is unfortunately too late for your class because you promised them you would never bump mathlib" things :D