Is this exercise in the book "The Mechanics of Proof" feasib

Stream: maths

[David Leroie]

In part "1.3.11. Exercises" in exercise 15 we have : https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#tips-and-tricks

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=

In this part of the book we have only learned how to use ring and rw in lean

But this exercise seems impossible

You need to add h1 and h2 to the right side of y = ??? so that it remains equal to y, then justify with := by ring

I can't do it, I'll share what I tried :

y = 2 - ((2 * x - y * x) / ((x + 3) - 3))

This solution does not work on lean because the divisor is equal to x and for lean x can be equal to 0

y = ((2 * x - y * x) - 2 * (x + 3) + 6) / (3 - (x + 3))

This solution also doesn't work because the divisor can be 0 according to lean

I know that x is not equal to 0 thanks to h1, but Lean doesn't know that. There is no assumption given in the statement of this exercise to tell us that x is
different from 0, and at this point in the book, we have only learned to use ring and rw; we are not allowed to use anything else.

So, is there a way to successfully complete this exercise using only the assumptions in the statement, or is it impossible with our current knowledge, and do
we need to use other lean tools we haven't yet learned ?

[David Leroie]

In part "1.3.11. Exercises" in exercise 15 we have : https://hrmacbeth.github.io/math2001/01_Proofs_by_Calculation.html#tips-and-tricks

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=

In this part of the book we have only learned how to use ring and rw in lean

But this exercise seems impossible

You need to add h1 and h2 to the right side of y = ??? so that it remains equal to y, then justify with := by ring

I can't do it, I'll share what I tried :

y = 2 - ((2 * x - y * x) / ((x + 3) - 3))

This solution does not work on lean because the divisor is equal to x and for lean x can be equal to 0

y = ((2 * x - y * x) - 2 * (x + 3) + 6) / (3 - (x + 3))

This solution also doesn't work because the divisor can be 0 according to lean

I know that x is not equal to 0 thanks to h1, but Lean doesn't know that. There is no assumption given in the statement of this exercise to tell us that x is
different from 0, and at this point in the book, we have only learned to use ring and rw; we are not allowed to use anything else.

So, is there a way to successfully complete this exercise using only the assumptions in the statement, or is it impossible with our current knowledge, and do
we need to use other lean tools we haven't yet learned ?

[Riccardo Brasca]

The difficulty here is purely mathematical (my students also struggled a lot with that one). Here is a possible solution

Solution

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 := by
calc
y = (-1/2y+1)(x+3)-1/2(2x-yx)-(-5/2y+3) := by ring
_ = (-1/2y+1)5-1/20-(-5/2y+3) := by rw [h1, h2]
_ = 2 := by ring
done

[Kevin Buzzard]

How about $y=y * 2 / 2 = y * (5 - 3) / 2 = y * ((x + 3) - 3) / 2 = y * x / 2 = (2 * x - (2 * x - y * x)) / 2 = (2 * x - 0) / 2 = 2 * x / 2 = x = (x + 3) - 3 = 5 - 5 = 2$?

[Riccardo Brasca]

Please don't double post

[Riccardo Brasca]

I am talking to @David Leroie

[Notification Bot]

4 messages were moved here from #lean4 > Is this exercise in the book "The Mechanics of Proof" feasib by Kevin Buzzard.