struggling with non-linear (squared) inequality

Stream: new members

[rzeta0]

I'm struggling to complete this exercise (see code below).

The problem I'm having is highlighted with a -- <--. I c

Essentially, I can't get from a goal state:

x : ℝ
hx : x ^ 2 < 9
ha : x ≤ -3

to show that ¬ x^2 <9.

In the second case x ≥ 3 I can easily show ¬ x^2 <9.

So I assume the challenge with the first case is that x ≤ 3 can include negative values. In fact the warning message from rel says it can't prove 0 ≤ x.

I have tried splitting x into x<0 and x≥0 but didn't seem helpful.

With paper-and-pen I'd say "pick x=-5, which conforms to x≤-3, which gives us x^2>9, a counter-example" but Ive not learned such a pattern in Lean yet.

Any suggestions?

---

import Mathlib.Tactic

example {x : ℝ} (hx : x ^ 2 < 9) : ¬ (x ≤ -3 ∨ x ≥ 3) := by
  intro h
  obtain ha | hb := h
  · -- x ≤ -3
    have g1:=
      calc
        x ^ 2 = x * x := by ring
        _ ≥ (-3) * (-3) := by rel [ha] -- < -- problem
        _ = 9 := by norm_num
  · -- x ≥ 3
    have g2:=
      calc
        x ^ 2 = x * x := by ring
        _ ≥ 3 * 3 := by rel [hb]
        _ = 9 := by norm_num
    apply not_lt_of_ge at g2
    contradiction

[rzeta0]

ps - linarith is disabled in MoP.

[Daniel Weber]

The problem here is that multiplication isn't monotone for negative values, e.g. a ≤ b -> -3 * a ≤ -3 * b is false, so rel can't do the substitution (it can't tell that you're doing it twice so it cancels out). Try this:

import Mathlib.Tactic

example {x : ℝ} (hx : x ^ 2 < 9) : ¬ (x ≤ -3 ∨ x ≥ 3) := by
  intro h
  obtain ha | hb := h
  · -- x ≤ -3
    have ha' : -x ≥ 3 := by sorry
    have g1:=
      calc
        x ^ 2 = (-x) * (-x) := by ring
        _ ≥ 3 * 3 := by rel [ha']
        _ = 9 := by norm_num
    sorry
  · -- x ≥ 3
    have g2:=
      calc
        x ^ 2 = x * x := by ring
        _ ≥ 3 * 3 := by rel [hb]
        _ = 9 := by norm_num
    apply not_lt_of_ge at g2
    contradiction

[Daniel Weber]

By the way, you can write

intro h
obtain ha | hb := h

as rintro (ha | hb)

[Eric Wieser]

rzeta0 said:

With paper-and-pen I'd say "pick x=-5, which conforms to x≤-3, which gives us x^2>9, a counter-example" but Ive not learned such a pattern in Lean yet.

This is a proof of ∃ {x : ℝ} (hx : x ≤ -3 ∨ x ≥ 3), ¬(x ^ 2 < 9), (or equivalently, ¬∀ {x : ℝ} (hx : x ≤ -3 ∨ x ≥ 3), x ^ 2 < 9) which just requires you to pick one x. The statement you are trying to prove requires you to show that the property holds for any such x

[rzeta0]

Hi Eric

So let me check my understanding:

• If the proof objective was "for all x where x ≤ -3 ∨ x ≥ 3, it is the case that ¬(x ^ 2 < 9)" then I can just pick one counterexample against (x^2 < 9) where x complies with x ≤ -3 ∨ x ≥ 3.

• However for a proof objective "for all x where (x ^ 2 < 9) , it is the case that ¬ (x ≤ -3 ∨ x ≥ 3)" then one counter-example against (x ≤ -3 ∨ x ≥ 3) is not possible (because there isn't one).

(sorry for being slow, I'm new to quantifiers)

[Eric Wieser]

I think thinking in terms of "counterexamples" isn't helpful here; a counterexamples is something you use to demonstrate that you stated the wrong theorem or made a wrong turn in your proof. If you actually are needing to come up with a particular x mid proof, then at the point you're looking for an example, not a counterexample!

[Eric Wieser]

(I say this because the trouble seems to be around how negations act with quantifiers, and being clear on where exactly the negation is an important part of resolving that)