why doesn't ring tactic take [] arguments?

Stream: new members

[Rado Kirov]

On chapter 3.6 of MIL, looks like ring tactic is weaker than linarith (not quite sure what is linear in this as it seems to work with polynomials).

With linarith this is a one liner

example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  have h' : (x + 1) * (x - 1) = 0 := by linarith [h]
  sorry -- rest of proof

while with ring I have do a much bigger dance:

example {x : ℝ} (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by

  have h' : x ^ 2 - 1 = 0 := by rw [h, sub_self]
  have h'' : (x + 1) * (x - 1) = 0 := by
    rw [← h']
    ring
  sorry -- rest of proof

why can't ring take [h] and figure out the basic algebraic transformation like linarith? Generally, which tactics take [] arguments and which don't?

[Sabbir Rahman]

ring only proves algebraic identities using semiring properties. So if you want to prove x^2 - 1 = (x-1) * (x+1) then ring will do that easily, as this requires no other information except for the ring properties. In your case, (x-1) * (x+1) = 0 is not an algebraic identity as it requires the hypothesis x^2 = 1. On the other hand, linarith does use hypothesis to prove stuff. so it is using the fact x^2 = 1 along with algebraic manipulation to get the goal

[Kyle Miller]

You might like linear_combination, which is one way to imagine how ring would take arguments.

[Rado Kirov]

neat, that worked

variable {R : Type*} [CommRing R] [IsDomain R]
variable (x y : R)

example (h : x ^ 2 = 1) : x = 1 ∨ x = -1 := by
  have h'' : (x + 1) * (x - 1) = 0 := by linear_combination h

no idea why it doesn't have [], but will take it for now (it will all become clear at some point).

[Kyle Miller]

The way that syntax works is you can write for example linear_combination 2 * h1 + 3 * h2 to say exactly how the goal is a linear combination of the given hypotheses.