proving a goal already instantiated by `use` variables?

Stream: new members

[rzeta0]

I've hit an unusual challenge - the goal I'm proving is already instantiated by the choices made by use.

Note: I'm new to constructor and use.

Context

I'm doing ex 2.5.9-9 from The Mechanics of Proof:

Let $a, b, c$ be real numbers, and suppose that $a \le b+c$,  $b \le a+c$ and $c \le a+b$. Show that there exist nonnegative real numbers $x, y, z$  such that  $a=y+z$, $b=x+z$  and $c=x+y$.

"Show there exist" means I simply have to find an example that works. Here $x=y=z=0$ satisfies the constraints.

To be explicit, $x=y=z=0$ means $a=b=c=0$, and the requirements are met: $0 \le 0 + 0$ three times.

Lean Code

The exercise gives us a head start:

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
  sorry

I started developing the proof as follows:

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
    use 0, 0, 0
    constructor -- 0 ≥ 0
    · norm_num
    constructor -- 0 ≥ 0
    · norm_num
    constructor -- 0 ≥ 0
    · norm_num

The satisfies the first three goals of the conjunction x ≥ 0 then y ≥ 0 and then z ≥ 0.

I continued...

    constructor -- a = 0+0
    · -- TODO

The info view confirms what the current dot-focussed goal is

a b c : ℝ
ha : a ≤ b + c
hb : b ≤ a + c
hc : c ≤ a + b
⊢ a = 0 + 0

Question: How do I show a = 0 + 0 ? Why is it even asking me to? I find this confusing.

My Attempt at Thinking

My beginner brain is telling me I need to show that the chosen example confirms to both the hypotheses and the "such that" conjunction.

A simpler example is "show there exists a natural number $n$ such that $n>10$. I can chose $n=11$ and then show $n=11>10$. If there was an additional hypothesis "$n$ is even". Then I could choose $n=12$ and show both "12 is even" and $12>10$.

Following this simpler example, I can't see why Lean is asking me to use the chosen $x=y=z=0$ to prove $a=0+0$.

Yes, I am confused, sorry.

[Edward van de Meent]

rzeta0 said:

"Show there exist" means I simply have to find an example that works. Here x=y=z=0 satisfies the constraints.

this doesn't satisfy the constraints, and this is exactly what lean is trying to tell you!
you get to say what $a,b$ and $c$ are; you need to prove that these $x,y$ and $z$ exist for all possible combinations of $a,b$ and $c$. in particular, $x=y=z=0$ (obviously) doesn't work for $a=b=c=1$.

[Edward van de Meent]

a rephrasing of the question might be: "Prove that for all real $a,b,c$, if $a≤b+c$,  $b≤a+c$ and $c≤a+b$, there exist nonnegative $x,y,z$ such that ..."

[Edward van de Meent]

it seems your idea of the question was "Prove that there exist $a,b,c,x,y,z$ such that ...", but that is a distinctly different question.

[rzeta0]

@Edward van de Meent

Do you mean "you get to say what x, yand z are" .. not "you get to say what a,b and c are" ?

I need to read your reply a few times to get my brain to understand. I will reply later this afternoon.

[Edward van de Meent]

indeed: you get to say what x,y and z are, but not what a,b and c are.

[Ruben Van de Velde]

use is a "dangerous" tactic, in the sense that you go from proving "there is some value I haven't found yet that satisfies some constraints" to "this value, this is the one that satisfies the constraints, which I'll prove now". In your case, you asserted that zero was this value, but you're now noticing that it isn't

[Ruben Van de Velde]

So you need to go back to before the point where you wrote use, and think what better values would be

[Edward van de Meent]

there are quite some more tactics which can be dangerous in this way; apply, left and right can give similar issues.

[rzeta0]

After a couple of hours trying to understand this I'm afraid I can't.

Here is my thinking in detail so we can spot the error:

1. The purpose of the proof is to choose $x, y, z$ which satisfy the constraints.

2. We can try $x=y=z=0$.

3. The exercise defines a=y+z, b=x+z, c=x+y. This gives us $a=b=c=0$.

4. The hypotheses are satisfied. ha: a ≤ b + c becomes 0 ≤ 0 + 0, which is true. Similar for hb and hc.

Where in these 4 steps is my error?

I appreciate your patience with my mathematical immaturity.

[Yakov Pechersky]

On the contrary, you are not free to assign a = b = c = 0. You need to find, for any assignment of a, b, c such that a ≤ b + c etc, the x, y, z. For example, a = b = c = 1 satisfies the inequalities. In that instance, what could x, y, z be?

[Yakov Pechersky]

Said differently, you proved something of assigned x y z => assigned a b c but you are asked to prove (handwavily) assigned a b c => assigned x y z.

[rzeta0]

Yakov - thanks for trying to help.

When I inevitably use use in the code, it will be for x, y and z.

That is correct?

[Dan Velleman]

rzeta0 said:

Here is my thinking in detail so we can spot the error:
...

3. The exercise defines a=y+z, b=x+z, c=x+y. This gives us $a=b=c=0$.
   

This is your mistake. The exercise does not define a, b, and c by these equations. Rather, these equations are part of what you have to prove. You have to prove that there are numbers x, y, and z that satisfy six conditions, and these three equations are the last three of those six conditions.

It might be helpful to think of a, b, and c as being chosen by someone else before the proof starts. Someone has chosen three numbers a, b, and c, written them down on a piece of paper, and sealed that piece of paper in an envelope. Those are the values of a, b, and c in this proof. You don't get to change them. You know that they satisfy the hypotheses ha, hb, and hc, but you don't know anything else about them. The values of x, y, and z are going to depend on a, b, and c. In other words, in your use steps, you won't be choosing particular numbers for x, y, and z, you'll be choosing formulas involving a, b, and c.

[rzeta0]

Thanks everyone for the replies.

Together with this thread, and the other one, I think I understand the root cause now.

I should be thinking of this as a "for any a,b,c, show there exist x, y,z such that ..."