ring tactic in the field of rationals

Stream: new members

[JK]

I'm a bit confused by the following simple example that works in Lean:

example (w : ℚ) (h : 3*w + 1 = 4) :
    w = 1 :=
  calc
    w = (3 * w + 1) / 3 - 1/3 := by ring
    _ = 4/3 - 1/3 := by rw [h]
    _ = 1 := by ring

How does the ring tactic "know" about division? (I understand that the rationals are a field ... but I would expect to have to use a "field tactic" to take advantage of that fact.)

[Eric Wieser]

ring is using norm_num

[Eric Wieser]

It doesn't know about division by variables, only by numeric constants

[Eric Wieser]

For a similar reason, ring knows about Nat.factorial!

import Mathlib

example {R} [CommRing R] {a : R} : Nat.factorial 3 * a = a + a + a + a + a + a := by
  ring

[JK]

That's still odd to me, since (3 * w + 1) / 3 is not defined in an arbitrary ring, nor is 1/3 for that matter.

[Eric Wieser]

I guess it's probably more accurate to say that ring knows about $\mathbb{Q}$-algebras

[Aaron Liu]

commutative ones