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

Stream: new members

[David Leroie]

In part "2.5.9. Exercises" in exercise 6 we have :
https://hrmacbeth.github.io/math2001/02_Proofs_with_Structure.html#id38

example {t : ℝ} (h : ∃ a : ℝ, a * t + 1 < a + t) : t ≠ 1 := by
  obtain ⟨s, hxt⟩ := h
  have H := le_or_gt s t
  obtain hx | hx := H
  . have h1 :=
      calc
        (s - 1) * (t - 1)
          = s * (t - 1) - 1 * (t - 1) := by ring
        _ = s * (t - 1) - (t - 1) := by ring
        _ = s * t - s - t + 1 := by ring
        _ = s * t + 1 - (s + t) := by ring
        _ < s + t - (s + t) := by rel [hxt]
        _ = 0 := by ring

The tutorial requires us to use have H := le_or_gt s t

So we first have the hypothesis hx : s ≤ t et h1 : (s - 1) * (t - 1) < 0, we must demonstrate that t ≠ 1

According to hypothesis hx : s ≤ t we can deduce that (s - 1) ≤ (t - 1) since adding -1 to both sides of an inequality does not change it

The mathematical logic is that if we have (s - 1) * (t - 1) < 0 then we have a positive factor and a negative factor.

So we know that in (s - 1) * (t - 1) < 0 the factor that is positive is (t - 1) because it is greater than (s - 1) :
(t - 1) > 0

Except that it is impossible to tell lean with the knowledge we have at this point in the lean tutorial, addarith cannot deduce this fact from the hypotheses

We learned to use : ring, rw, rel, numbers, extra, addarith, cancel

Then we learned to use several lemmas :

ne_of_lt
ne_of_gt
le_antisymm
le_or_succ_le
eq_zero_or_eq_zero_of_mul_eq_zero
abs_le_of_sq_le_sq'
le_or_gt

We can also use and (∧) and or (∨), the existence quantifier, creating hypotheses with have

We are only allowed to use what we have learned at this point in the tutorial.

The AI ​​gives me a solution with cases by contradiction, but we haven't learned proof by contradiction yet so we're not allowed to use it.

[Aaron Liu]

Please edit your post to use #backticks

[Notification Bot]

This topic was moved here from #lean4 > Is this exercise in the book "The Mechanics of Proof" feasib by Patrick Massot.

[Aaron Liu]

I think casing on le_or_gt s 1 will be more useful

[David Leroie]

Aaron Liu said:

I think casing on le_or_gt s 1 will be more useful

We don't have the right, we have to use have H := le_or_gt s t

Otherwise I managed to solve that with have H := le_or_gt (s - 1) 0 but you have to do as he said

[Aaron Liu]

you don't have to do what the author did

[David Leroie]

Aaron Liu said:

you don't have to do what the author did

It's not what the author did, but what the author told us to do.

[Aaron Liu]

As in Example 2.5.2, I used the lemma le_or_gt, which says that if $s$ and $t$ are real numbers then either $s \le t$ or $t < s$; it can be a useful case division.

I don't see where you are being told to do anything

[Aaron Liu]

also s and t are free in this quote, they don't correspond to the s and t that you bound them to

[David Leroie]

Aaron Liu said:

As in Example 2.5.2, I used the lemma le_or_gt, which says that if $s$ and $t$ are real numbers then either $s \le t$ or $t < s$; it can be a useful case division.

I don't see where you are being told to do anything

Okay, you're right, it doesn't explicitly say to use these parameters, but why is it there if we shouldn't use them?

Is it possible to complete the exercise with these specific parameters? If it's impossible, then I'll use other parameters.

[Aaron Liu]

You should use it with (s := s) and (t := 1)

[David Leroie]

Aaron Liu said:

You should use it with (s := s) and (t := 1)

Could I have confirmation that it's impossible to do this with le_or_gt s t?

Because even if it doesn't explicitly say to use that, I want to use it.

[Aaron Liu]

It's never impossible, since obtain preserves provability

[Aaron Liu]

but I don't think it's useful at all

[David Leroie]

Aaron Liu said:

It's never impossible, since obtain preserves provability

So how do we do it?

[Aaron Liu]

you do the cases, and then copy-paste the proof that uses le_or_gt s 1 onto both of the cases, ignoring the new hypotheses that you get in each case

[David Leroie]

Aaron Liu said:

you do the cases, and then copy-paste the proof that uses le_or_gt s 1 onto both of the cases, ignoring the new hypotheses that you get in each case

Yes, I thought about doing that, but can we do it with the hypotheses
(s - 1) * (t - 1) < 0
s ≤ t
s > t

without creating a new hypothesis?

[Aaron Liu]

probably not (I haven't tried but it doesn't seem possible)