Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip Kevin Buzzard (May 21 2020 at 09:56):

Do we have a tactic which proves that x2+y20x^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 3x203x^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.

view this post on Zulip Kenny Lau (May 21 2020 at 09:58):

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

view this post on Zulip Kenny Lau (May 21 2020 at 09:59):

so basically Tarski–Seidenberg theorem

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 21 2020 at 10:00):

coq has that with nre right?

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 21 2020 at 10:18):

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

view this post on Zulip Kenny Lau (May 21 2020 at 10:18):

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

view this post on Zulip Gabriel Ebner (May 21 2020 at 10:19):

#2637

view this post on Zulip Kenny Lau (May 21 2020 at 10:20):

great

view this post on Zulip Kevin Buzzard (May 21 2020 at 10:46):

I added some tests

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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