trying to understand what needs to be existence proved

Stream: new members

[rzeta0]

I asked about this exercise in a different question, but this question is specifically to check I understand what needs to be proved. (The other question asks about an unusual focussed goal).

Here is the Lean proof header.

example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) :
    ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by

Here is my interpretation:

• a, b, c are real values
• we have three hypotheses, which we can think of as constraints ha : a ≤ b + c, hb : b ≤ a + c, hc : c ≤ a + b
• the proposal we need to prove is that there exist x, y, z which conform to the following constraint: x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y

So I need to find a suitable x, y and z (not a, b, c`). The other thread confused me about this.

And I need to show that my choice of x, y and z meet both the constraint x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y and all the hypotheses ha, hb and hc.

Is there an error in my thinking above?

I believe x=y=z=0 satisfies all the constraint, but the other thread suggests this is wrong. I genuinely can't see why.

[rzeta0]

---

In my mind it would be easier if the ha, hb, hc were in the proof objective and the a = y + z ∧ b = x + z ∧ c = x + y was a hypothesis.

This way I can use the hypothesis to construct a, b, c and show that a ≤ b + c, b ≤ a + c, c ≤ a + b were met.

[Eric Paul]

Here's one way to think about it:

I am going to choose three real numbers and I'm not going to tell what they are.
Let's say that I choose a = 1, b = 1, and c = 1. I have made this choice but have not told you.

However, I do give you a little bit of information about the choice I made.
I tell that my secret choices satisfy the following:
a ≤ b + c, b ≤ a + c, and c ≤ a + b.

Now, I ask you to find three real numbers x, y, and z such that
x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y.

You are saying that x = 0, y = 0, and z = 0 is a valid choice.
But we see that we are meant to have that a = y + z and this is not correct under this choice
(because we have 1 = 0 + 0).

So whatever values you choose for x, y, and z, it must satisfy certain relationships with the a, b, and c I've already chosen.

[Eric Paul]

Here's a simpler example that may help:

import Mathlib

example (a : ℝ) : ∃x : ℝ, a ≤ x := by sorry

In this piece of code we are given a real number a and our goal is to show that there exists a real number x such that a ≤ x. (Notice how this is similar to your situation just with fewer given real numbers and fewer constraints to satisfy.)

We could take the same approach and try saying that x = 0:

import Mathlib

example (a : ℝ) : ∃x : ℝ, a ≤ x := by
  use 0
  sorry

Now our goal is to show that a ≤ 0. And this is not possible because we don't know what a is! The only piece of information we have is that a is real number.

What you need to do to solve this goal is similar in spirit, although simpler, to what you need to do in your situation.

[MohanadAhmed]

rzeta0 said:

Is there an error in my thinking above?

I believe x=y=z=0 satisfies all the constraint, but the other thread suggests this is wrong. I genuinely can't see why.

One way to see why your choice of x y z does not satisfy the problem is to the following: since you chose $x = y = z = 0$, then you are forcing $a = 0 + 0 = 0, b = 0, c = 0$. But this was not given! You can see Eric Paul's example above of $a=b=c=1$ of one such case that satisfies the conditions ha, hb, hc but would not work with your choice of all zeros.

In general you would need your choice of x, y, z to depend on a, b, c.

Take again Eric Pauls example:

import Mathlib
example (a : ℝ) : ∃x : ℝ, a ≤ x := by sorry

You can read this as Can you find a number x such that x > a? And the answer is obviously yes. Take the number x = a + 1. Whatever the value of a, (x = a + 1) is always going to be higher than a! We could also have taken the number x = a + 2 or any number x = a + z where z is some positive constant. Notice in this case the number of choices that you can use is infinite, any of them would work.

Sometimes however the problem is constrained such that only one solution exists. Consider:

example (a : ℝ): ∃x : ℝ, 2*x = a := by
  use a / 2
  linarith

Nothing other than $a/2$ would work!

In your original problem your choice for x, y and z will probably depend on a, b and c, i.e. x will be a function of a, b, c and similarly for y and z.

Solution of Original Problem 2.5.9

import Mathlib.Tactic

example {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) :
    ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by
  simp_rw [ge_iff_le]
  use (b + c - a)/2
  use (c + a - b)/2
  use (a + b - c)/2
  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
  all_goals linarith

[Dan Velleman]

rzeta0 said:

So I need to find a suitable x, y and z (not a, b, c`). The other thread confused me about this.

And I need to show that my choice of x, y and z meet both the constraint x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y and all the hypotheses ha, hb and hc.

Is there an error in my thinking above?

You have to prove x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y, but you don't have to prove ha, hb, and hc. They are given in the problem.

In my mind it would be easier if the ha, hb, hc were in the proof objective and the a = y + z ∧ b = x + z ∧ c = x + y was a hypothesis.

This way I can use the hypothesis to construct a, b, c and show that  a ≤ b + c, b ≤ a + c, c ≤ a + b were met.

Yes, that would be easier. But that's not what the problem says. And as you correctly observed in the first quote above, you are finding x, y, and z, but not a, b, and c. This is the fundamental point on which you seem to be hung up. You should think of a, b, and c as fixed in this proof (although you haven't been told what their values are). You don't get to change them. So you can't make the equations a = y + z, b = x + z, and c = x + y true by changing the values of a, b, and c. Rather, you have to make them true by a very careful choice of x, y, and z.

[rzeta0]

Thanks everyone for the replies. @Eric Paul your reply in particular I think helped.

I did do a previous exercise successfully where the solution depended on a variable, so I think the wording of this exercise really didn't work for me.

Would I be right in saying that exercise is an example of the following the logical phrase

"for any a, b, c, subject to constraints on a,b,c, ... show there exists an x, y, x, such that"

The "for any" helps me have the correct interpretation, if it is truly applicable here.

[Eric Paul]

Yes, what you said is the correct way to think of what is happening.

In fact, you can rewrite what you are trying to show using "for all" and it is the same:

import Mathlib

theorem version1 {a b c : ℝ} (ha : a ≤ b + c) (hb : b ≤ a + c) (hc : c ≤ a + b) :
    ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by sorry

theorem version2 : ∀{a b c : ℝ}, a ≤ b + c → b ≤ a + c → c ≤ a + b →
    ∃ x y z, x ≥ 0 ∧ y ≥ 0 ∧ z ≥ 0 ∧ a = y + z ∧ b = x + z ∧ c = x + y := by sorry

theorem same : @version1 = @version2 := rfl

Here version1 is what you have, version2 writes it using the "for all a, b, c such that" notation, and same proves that the two theorems are equal (in fact there is no proving to be done really, Lean can't tell them apart)