failed vs valid proof - beginner lesson to be learned?

Stream: new members

[rzeta0]

Previously I posted a lean proof attempting to implement the following:

$$y=(x-2)(x+2) \land (x \geq 2) \implies y \geq 4$$

Version 1 of a lean proof is as follows:

example {x y : ℤ} (h1 : y = (x-2)*(x+2)) (h2: x ≥ 0) : y ≥ -4 :=
  calc
    y = (x-2)*(x+2) := by rw [h1]
    _ ≥ (0-2)*(x+2) := by rel [h2]
    _ ≥ (0-2)*(0+2) := by rel [h2] -- error here
    _ = -4 := by norm_num

It turns out the rel tactic fails if any multiplicative factors can't be shown to be positive.

Version 2 of the a lean proof works but I feel is less aesthetically pleasing:

example {x y : ℤ} (h1 : y = (x-2)*(x+2)) (h2: x ≥ 0) : y ≥ -4 :=
  calc
    y = (x-2)*(x+2) := by rw [h1]
    _ = x^2 - 4 := by ring
    _ ≥ (0)^2 - 4 := by rel [h2]
    _ = -4 := by norm_num

So my question is, given the theorem is valid, what can we learn about trying to prove it in Lean.

Is the lesson any of the following?

• some tactics, such as rel are limited in their ability to reason - that's life
• with Lean, always be prepared to find a different way, even less aesthetically-pleasing way, because tactics are imperfect
• discuss here so the developers can guide their improvement of tactics
• ... something else?

[Michal Wallace (tangentstorm)]

So... The rel docs claim that it's looking through the database for theorems marked @[gcongr] and applying those, so on the one hand you could try to make a gcongr rule and teach rel new tricks.

But on the other hand... What rule are you trying to apply here? Suppose x=5:

y ≥  (0-2)*(5+2)    -- -14
_ ≥  (0-2)*(0+2)    --  -4

I'm not terribly convinced you should be able to prove that...