exercise of the mechanics of proof

Stream: maths

[Esteban Estupinan]

Hello everyone, I was doing the following exercise from the book the mechanics of proof. I think the start was good, and I think that to build hypothesis h2 I should use something like the distributive property. Maybe someone has already solved this exercise, can you help me please?

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

[Daniel Weber]

Are you looking for some particular proof? You can show x = 2, then substitute that at h2 and simplify:

example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 := by
  apply eq_sub_of_add_eq at h1
  norm_num at h1
  rw [h1] at h2
  apply eq_of_sub_eq_zero at h2
  simp at h2
  exact h2.symm

[Daniel Weber]

If you want to use calc you can do:

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

although it's more cryptic in my opinion. (edited it to only use rw and ring)

[Richard Copley]

(This is exercise 15 in section 1.3.11). I'm not sure what the constraints are. If each proof is still supposed to be

either ring or rw with some hypotheses

as in example 1.2.2, then this works:

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

[Jonatas Miguel]

This particular exercise took me a while to figure out. And my solution is kinda dumb and roundabout:

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

I like @Daniel Weber 's second solution, it's really straightforward in comparison to what I did. But it uses something that hadn't been presented to us through the book, so anyone getting first exposed to Lean wouldn't know about the ability to chain tactics like what's being done with by rw [h2]; ring.

I suppose the way to get rid of that bit would be to rewrite the first two lines there to read:

-- copy of @**Daniel Weber** 's solution with small tweak to express it in a way that a reader of MoP would be aware of:
example {x y : ℝ} (h1 : x + 3 = 5) (h2 : 2 * x - y * x = 0) : y = 2 :=
  calc
    y = y + (0) / 2 := by ring
    _ = y + (2 * x - y * x) / 2 := by rw [h2]
    _ = y + (x + 3 - 3)*(2 - y) / 2 := by ring
    _ = y + (5 - 3) * (2 - y) / 2 := by rw [h1]
    _ = 2 := by ring

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kim Morrison]

Or just

import Mathlib

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

[Ruben Van de Velde]

The assignment was Give proofs by calculation..., so I'm afraid neither of you gets marks :)

[Kevin Buzzard]

I'm pretty sure that linear_combination is just a calculation?

[Mario Carneiro]

I'm convinced that "calculation" is as ill defined as "canonical" when you try to pin it down precisely

[Johan Commelin]

I'll prove my next theorem with

Proof. The obvious canonical computation is left as exercise to the reader.

[Kevin Buzzard]

There's a nonzero chance that GitHub copilot could fill in the details. I was very surprised recently when I wrote a comment "galois acts on a product of linear polynomials in the obvious way" (when writing code in front of students, so I was liberally adding comments) and copilot then formalised the statement correctly.

[Jonatas Miguel]

I guess the thing to look out for when trying to respond to people working on the exercises from the Mechanics of Proof book is that there are a specific set of tools that they'd be working with in specific chapters. So, a lot of these solutions use things that someone like myself would not have seen before.

[Esteban Estupinan]

Hello everyone, please maybe you could give me some guidelines to solve and complete the following theorems?

In the first one I have the idea of ​​doing it by elimination although I think it could be done by calculation to reduce steps.

The second one, I thought I was doing well at the beginning but I notice that the resolution is getting very long and there must be a shorter path

example {x y : ℚ} (h : x + y = 5 ∧ x + 2 * y = 7) : x = 3 ∧ y = 2 := by
  obtain ⟨h1, h2⟩ := h
  constructor


example {a b : ℝ} (h1 : a * b = a) (h2 : a * b = b) :
    a = 0 ∧ b = 0 ∨ a = 1 ∧ b = 1 := by
  have h3 : a * b - a = 0 := by addarith [h1]
  have h4 :=
  calc
    a * (b - 1) = a * b - a := by ring
    _ = 0 := by rw [h3]
  have h5 := eq_zero_or_eq_zero_of_mul_eq_zero h4
  obtain h6 | h7 := h5
  left
  constructor
  apply h6

  have h8 : a * b - b = 0 := by addarith [h2]
  have h9 :=
  calc
    b * (a - 1) = a * b - b := by ring
    _ = 0 := by rw [h8]
  have h10 := eq_zero_or_eq_zero_of_mul_eq_zero h9
  obtain h11 | h12 := h10
  apply h11

[Ruben Van de Velde]

For two, I'd note that $a=b=a^2$

[Heather Macbeth]

@Esteban Estupinan Note that the pattern

  have h3 : a * b - a = 0 := by addarith [h1]
  have h4 :=
  calc
    a * (b - 1) = a * b - a := by ring
    _ = 0 := by rw [h3]

can be shortened -- you can just write

  have h4 :=
  calc
    a * (b - 1) = a * b - a := by ring
    _ = 0 := by addarith [h1]

Same later on.

[Heather Macbeth]

And in the first branch, note that once you know a = 0, you can use a calculation involving h2 to prove that b = 0.

[Esteban Estupinan]

Thank you very much Heather Macbeth. Now Im trying to solve the last 4 exercises of or section that according to the explanation in your book you have to use the lemma le_or_succ_le, I am not sure if this lemma should be used exclusively with the number 1, because I tried to solve this exercise but only half of it came out

example {n : ℕ} : n ^ 2 ≠ 7 := by
  have hn := le_or_succ_le n 1
  obtain hn | hn := hn
  apply ne_of_lt
  calc
    n ^ 2 ≤ 1 ^ 2 := by rel [hn]
    _ < 7 := by numbers
  apply ne_of_gt
  sorry
example {x : ℤ} : 2 * x ≠ 3 := by
  sorry

example {t : ℤ} : 5 * t ≠ 18 := by
  sorry

example {m : ℕ} : m ^ 2 + 4 * m ≠ 46 := by
  sorry

I would be very grateful if you could give me ideas or the beginnings to solve these exercises, especially when they have large numbers like 18 or 46 or that of the case of a squared polynomial.

[Heather Macbeth]

@Esteban Estupinan le_or_succ_le n 1 sets up a case split, dividing the natural numbers in half: $n\leq 1$ or $n\geq 2$. This is not the right splitting point to show that $n^2\ne 7$. Instead, see how much you can increase 1 while still allowing the first case to work out -- you will find that when you have increased it as much as possible, the second case also works out.

[Esteban Estupinan]

(deleted)

[Esteban Estupinan]

Hello everyone, I was trying to do this exercise. It is easy to prove when the two integers involved have the same parity, the problem arises when they have different ones. How do I restructure the demonstration or complete the parts that are with the word sorry.

example (a b c : ℤ) : Even (a - b) ∨ Even (a + c) ∨ Even (b - c) := by
  left
  obtain ha | ha := Int.even_or_odd a
  . obtain hb | hb := Int.even_or_odd b
    . obtain ⟨x, hx⟩ := ha
      obtain ⟨y, hy⟩ := hb
      use x - y
      calc
        a - b = 2 * x - 2 * y := by rw [hx, hy]
        _ = 2 * (x - y) := by ring
    . sorry
  . obtain hb | hb := Int.even_or_odd b
    . sorry
    . obtain ⟨x, hx⟩ := ha
      obtain ⟨y, hy⟩ := hb
      use x - y
      calc
        a - b = (2 * x + 1) - (2 * y + 1) := by rw [hx, hy]
        _ = 2 * (x - y) := by ring

[Ruben Van de Velde]

Lazy way:

import Mathlib
example (a b c : ℤ) : Even (a - b) ∨ Even (a + c) ∨ Even (b - c) := by
  by_cases ha : Even a <;>
  by_cases hb : Even b <;>
  by_cases hc : Even c <;>
  simp [parity_simps, *]

[Ruben Van de Velde]

You definitely don't want to use left that early, because it makes the rest of the proof impossible to finish

[Esteban Estupinan]

but according to the following solution, it explains that there is only a demonstration when the numbers have the same parity, whether they are both even or odd, which is what I managed to prove, but when they have different parities it seems that there is no way to prove.
Is there a way to separate the cases Even a Odd b and Odd a Even b using Int.even_or_odd? or a way to demonstrate only cases of same parity?
https://personal.math.ubc.ca/~jychen/2017Math220/Homework%207%20Solutions.pdf

[Ruben Van de Velde]

My proof is "We could also do a case analysis on the parities of a, b and c, which also proves the statement.", I suppose

[Ruben Van de Velde]

I don't understand your question

[Ruben Van de Velde]

Are you asking about the case where $a$ and $b$ have different parity? Then clearly $a-b$ is odd, so you'll need to prove either the second or third case.

If $c$ has the same parity as $a$, then $a+c$ is even and the second case works.

If $c$ has the opposite parity of $a$, and (as we assumed) $b$ also has the opposite parity of $a$, $b$ and $c$ must have the same parity, and we conclude that $b - c$ is even.