Zulip Chat Archive

Stream: new members

Topic: struggling with non-linear (squared) inequality


rzeta0 (Dec 07 2024 at 15:39):

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 (Dec 07 2024 at 15:39):

ps - linarith is disabled in MoP.

Daniel Weber (Dec 07 2024 at 15:52):

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 (Dec 07 2024 at 15:55):

By the way, you can write

intro h
obtain ha | hb := h

as rintro (ha | hb)

Eric Wieser (Dec 07 2024 at 16:26):

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 (Dec 07 2024 at 17:16):

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 (Dec 07 2024 at 17:44):

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 (Dec 07 2024 at 17:45):

(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)


Last updated: May 02 2025 at 03:31 UTC