Example 1.4.3 from MoP

Stream: Lean for Scientists and Engineers 2024

[Gerard Finol]

The solution seen in yesterday's lecture of the Example 1.4.3 from MoP looked like:

import Mathlib

example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 :=
  calc
    x + y = x + y := by ring
    _ ≤ (x) + (x + 5) := by rel [h1]
    _ ≤ -2 + (-2 + 5) := by rel [h2]
    _ < 2 := by norm_num

As we are doing one rel [h1] followed by rel [h2], I thought that we could change that by rel [h1, h2] and do everything in just one step. But it looks like lean does not like that...

import Mathlib

example {x y : ℝ} (h1 : y ≤ x + 5) (h2 : x ≤ -2) : x + y < 2 :=
  calc
    x + y = x + y := by ring
    _ ≤ (-2) + (-2 + 5) := by rel [h1, h2] --  Does not work
    _ < 2 := by norm_num

I get the following error message: "rel failed, cannot prove goal by 'substituting' the listed relationships. The steps which could not be automatically justified were: y ≤ -2 + 5 ". Does anybody know why?

[Gerard Finol]

In the previous example (1.4.2 from MoP), rel [h1, h2] works just fine :sweat_smile: :

import Mathlib
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 :=
  calc
    r = (s + r + r - s) / 2 := by ring
    _ ≤ (3 + (s + 3) - s) / 2 := by rel [h1, h2]
    _ = 3 := by ring

[Kevin Buzzard]

These tactics do not do magic. They are algorithms written by humans to precise specifications. Looking at 1.4.2 and the inequality you want to prove, it's of the form $(X-s)/2 \leq (Y-s)/2$ and part of rel's specification is that it realises that it can strip off the $/2$ and the $-s$ and it suffices to prove $X\leq Y$. Now (adding in the brackets, which are invisible to you but very important to Lean) we have to prove $(s+r)+r\leq 3+(s+3)$. Again, part of rel's specification is that it knows things like "if $a\leq b$ and $c\leq d$ then $a+c\leq b+d$", so it realises that i suffices to prove $s+r\leq 3$ and $r\leq (s+3)$, but these are precisely the hypotheses which you gave it.

In your situation, let's apply the same algorithm. We want to prove $x+y\leq (-2)+(-2+5)$, and the way the rel algorithm works, it's going to try and deduce this from $x\leq-2$ and $y\leq(-2+5)$. This algorithm is not magic, it's not thinking, it's applying a mechanical rule. And here you can see that you did not give it exactly these proofs, so the algorithm fails. This doesn't mean the result is false, but it does explain the phenomenon you're seeing.

Similarly, you would easily be able to break the first proof by moving brackets around to make equations which are mathematically "obviously the same" but which Lean would regard as different, because $(x+y)+z$ and $x+(y+z)$ are equal, but they're not equal by definition, they're equal because of the axiom of associativity, an axiom which the rel tactic doesn't know. Here is 1.4.2 revisited:

import Mathlib
example {r s : ℚ} (h1 : s + 3 ≥ r) (h2 : s + r ≤ 3) : r ≤ 3 :=
  calc
    r = (s + (r + r) - s) / 2 := by ring -- move the brackets a bit, mathematically no difference at all
    _ ≤ (3 + (s + 3) - s) / 2 := by rel [h1, h2] -- proof now breaks
    _ = 3 := by ring

When I was learning Lean, my first reaction to things like this was "well this is just stupid, why doesn't the algorithm do something more clever? Obviously the hypotheses imply the conclusion". And the answer is that this is called "scope creep". The point of the rel tactic is to be quick and efficient and only try the "naive" things which I've explained above. If you are looking for a tactic which starts rearranging terms and spotting patterns which humans take for granted, then at the end of the day you are asking for a far far more complex algorithm. This is called the Fourier-Motzkin algorithm, it's much more complex than rel and it's far harder to implement in Lean, but it has been done, and it's in the linarith tactic. So you can solve your problem with one tactic, but that tactic is linarith, not rel [h1, h2].

The disadvantage of more high-powered tactics is that they take longer to run. This is why it's useful to have both quick and dirty tactics and more complex ones. The art is learning when to use what.

[Gerard Finol]

Oh, now I understand it. Thank you very much for your detailed answer @Kevin Buzzard !