x^2+y^2>=0

Stream: Is there code for X?

[Kevin Buzzard]

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]

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

[Kenny Lau]

so basically Tarski–Seidenberg theorem

[Kevin Buzzard]

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]

coq has that with nre right?

[Chris Hughes]

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

[Kenny Lau]

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

[Kenny Lau]

or https://github.com/leanprover-community/mathlib/search?q=nlinarith&unscoped_q=nlinarith

[Gabriel Ebner]

#2637

[Kenny Lau]

great

[Kevin Buzzard]

I added some tests

[Kevin Buzzard]

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]

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

[Heather Macbeth]

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.