Mechanics of Proof 4.1.1

Stream: new members

[Tyler Josephson ⚛️]

The first example in Mechanics of Proof 4.1.1 has been puzzling me:

The original example states

example {a : ℝ} (h : ∀ x, a ≤ x ^ 2 - 2 * x) : a ≤ -1 :=
  calc
    a ≤ 1 ^ 2 - 2 * 1 := by apply h
    _ = -1 := by numbers

But I can make a small change to the proof (shift to a different value along the parabola), and all goals still close:

example {a : ℝ} (h : ∀ x, a ≤ x ^ 2 - 2 * x) : a ≤ 0 :=
  calc
    a ≤ 0 ^ 2 - 2 * 0 := by apply h
    _ = 0 := by numbers

From my understanding of the context, a ≤ -1 was supposed to hold "for all real numbers x" and it makes sense that (1, -1) is a special point, being the minimum of the curve. But then why can I close the goals by shifting to another point on the parabola?

[Mauricio Collares]

Looking purely at the statement, you didn't change the hypothesis but you weakened the conclusion of the theorem. You wouldn't be able to prove the original conclusion by choosing x = 0.

[Yury G. Kudryashov]

a ≤ -1 implies a ≤ 0, so there is nothing surprising in the fact that you can prove a weaker inequality starting with the same assumptions.

[Tyler Josephson ⚛️]

It's clicking a bit better for me now. I guess I have a mental picture of a ≤ 0 corresponding to this sort of picture. But a ≤ 0 need not imply that a > -1.
04_logic_01_parabola-copy.png

[Eric Wieser]

Note that if you wanted to express that the mimum of the parabola is exactly -1, you could use

example : IsGreatest {a | ∀ x, a ≤ x ^ 2 - 2 * x} (-1) := sorry

as your statement

[Tyler Josephson ⚛️]

Would this be a reasonable explanation:
a ≤ x ^ 2 - 2 * x implies that there exists some a > -1 (for example, when x = 0)
But
∀ x, a ≤ x ^ 2 - 2 * x does not imply that there exists some a > -1, because the ∀ x part of the statement prevents that

[Eric Wieser]

In lean it doesn't make sense to say "P a implies there exists some a", because you've already picked a specific a

[Eric Wieser]

That is, these two statements are trivially identical, and the second is obviously not what you meant

example {P : ℝ → Prop} (a : ℝ) (h : P a) : ∃ a, a > -1 := sorry
example {P : ℝ → Prop} (a : ℝ) (h : P a) : ∃ b, b > -1 := sorry