beginner error with ring tactic

Stream: new members

[rzeta0]

I'm beginning to learn Lean 4 using the Mechanics of Proof tutorial.

The following gives an error and I can't see why:

x ^ 3 - 8 * x ^ 2 + 2 * x = x * (x^2 - 8*x + 2) := by ring

I'd welcome explanations - I suspect it is syntax rather than maths which looks correct:

$$x^3 - 8x^2 +2x = x(x^2-8x+2)$$

[Andrew Yang]

Can you provide an #mwe? The following works for me.

import Mathlib

example (x : ℤ) : x ^ 3 - 8 * x ^ 2 + 2 * x = x * (x^2 - 8*x + 2) := by ring

[Andrew Yang]

(also can someone move this to #new members?)

[rzeta0]

here's an mwe

example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 :=
  calc
    x ^ 3 - 8 * x ^ 2 + 2 * x = x * (x^2 - 8*x + 2) := by ring

gives

04_Proving_Inequalities.lean:137:58

ring failed: not an equality

[Andrew Yang]

Hmm my error message was different though. Anyway you might need to provide the next line or else calc might get confused

example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 :=
  calc
    x ^ 3 - 8 * x ^ 2 + 2 * x = x * (x^2 - 8*x + 2) := by ring
          x * (x^2 - 8*x + 2) ≥ 3 := by sorry

[Yakov Pechersky]

Basically, you can't use a naked calc like that to construct an intermediate hypothesis. You are using calc in term mode, which expects the LHS are the first LHS, and the RHS as the last RHS

[Yaël Dillies]

Would be great if the error said that though...

[rzeta0]

I have fixed it by trial and error - as Yael suggests, the errors aren't ideal.

example {x : ℤ} (hx : x ≥ 9) : x ^ 3 - 8 * x ^ 2 + 2 * x ≥ 3 :=
  calc
    x ^ 3 - 8 * x ^ 2 + 2 * x = x * (x^2 - 8*x + 2) := by ring
    _ = x * (x*(x - 8) + 2) := by ring
    _ ≥ (9) * (9*(9-8) + 2) := by rel [hx]
    _ ≥ 3 := by numbers

Another example - having (9*(1)+2) instead of (9*(9-8)+2) gives an error which doesn't explain what the actual problem is...

rel failed, cannot prove goal by 'substituting' the listed relationships. The steps which could not be automatically justified were:
1 ≤ x - 8

[Notification Bot]

This topic was moved here from #maths > beginner error with ring tactic by Mario Carneiro.

[Yaël Dillies]

Yaël Dillies said:

Would be great if the error said that though...

I've opened lean#4318. Feel free to :+1: it

[Heather Macbeth]

rzeta0 said:

Another example - having (9*(1)+2) instead of (9*(9-8)+2) gives an error which doesn't explain what the actual problem is...

rel failed, cannot prove goal by 'substituting' the listed relationships.
The steps which could not be automatically justified were:
1 ≤ x - 8

Hmm, this looks like a pretty reasonable error message to me, I don't really see how it could be improved.
Self-contained example:

import Mathlib

example {x : ℚ} (hx : x ≥ 9) : x * ( x * (x - 8) + 2) ≥ 9 * (9 * 1 + 2) := by rel [hx]
/-
rel failed, cannot prove goal by 'substituting' the listed relationships.
The steps which could not be automatically justified were:
1 ≤ x - 8
-/

The error is saying that one of the substitutions occurring in

x * ( x * (x - 8) + 2) ≥ 9 * (9 * 1 + 2)

is that an (x - 8) is being replaced by a 1, and you have not provided a hypothesis which states the inequality x - 8 ≥ 1.