## Stream: Is there code for X?

### Topic: x^2+y^2>=0

#### Kevin Buzzard (May 21 2020 at 09:56):

Do we have a tactic which proves that $x^2+y^2\geq0$ if x y : real? Is this what @Heather Macbeth was asking about? I'm making the complex number game and for norm stuff you need to be able to kill these goals quickly if you want to impress mathematicians.

Can this be done with some sort of tactic combinator? I don't need anything fancy, but $3x^2\geq0$ would be another example I'd be optimistic about -- "obvious to mathematicians" is what I want to emulate.

@Mario Carneiro : the spec is that it has to solve both 3x^2+4y^2>=0, and 3x^2+4y^2=0 iff x=y=0.

#### Kenny Lau (May 21 2020 at 09:58):

so a tactic that witnesses the fact that the theory of real closed fields is complete

#### Kenny Lau (May 21 2020 at 09:59):

so basically Tarski–Seidenberg theorem

#### Kevin Buzzard (May 21 2020 at 10:00):

Given my current situation I would be just as happy with something which added hx : x^2>=0and x * x >= 0 for everything and then just tried linarith

#### Kevin Buzzard (May 21 2020 at 10:00):

coq has that with nre right?

#### Chris Hughes (May 21 2020 at 10:16):

Isn't this nlinarith. I think it's basically linarith with the assumption that squares are nonnegative

#### Kenny Lau (May 21 2020 at 10:18):

I can't find it in https://leanprover-community.github.io/mathlib_docs/tactics.html ?

#2637

great

#### Kevin Buzzard (May 21 2020 at 10:46):

I'm going live at 5pm so if you could have the tactic ready for then, that would be great :rolling_on_the_floor_laughing:

#### Kevin Buzzard (May 21 2020 at 10:47):

Fortunately, Lean's inability to close these goals is only exposed in about level 4, which is a fair way in.

#### Heather Macbeth (May 21 2020 at 16:14):

Kenny Lau said:

so a tactic that witnesses the fact that the theory of real closed fields is complete

so basically Tarski–Seidenberg theorem

@Kenny Lau Let me ask you about this here, since people mention it a lot. If I understand correctly, (an extension of) the Tarski-Seidenberg theorem is a doubly-exponential algorithm, not implemented in Lean, for determining the proof/disproof of any statement over the reals, like

example : ∀ (a b : ℝ), ∃ (c d : ℝ), ∀ (e : ℝ), ∃ (f g h : ℝ), (a + e^3 - 2 * b * c ≥ 0) →
(c - 3 * h = 0) → ((2 * b * g^2 + 3 * d < 0) ∧ (f - 7 * g + a ≤ 17))


But wouldn't the idealized form of nlinarith be something much weaker, determining only the proof/disproof of statements with a single quantifier? Like

example : ∀ (a b c d e f g h : ℝ), (a + e^3 - 2 * b * c ≥ 0) →
(c - 3 * h = 0) → ((2 * b * g^2 + 3 * d < 0) ∧ (f - 7 * g + a ≤ 17))


If I understand correctly, there is a better algorithm for such problems.

Last updated: May 17 2021 at 15:13 UTC