Decision procedure for `(ℝ,+,*,≤)`

Stream: Is there code for X?

[Geoffrey Irving]

Do we have the decision procedure for real semialgebraic geometry?

(Asking for one of these worked last time, figured I should try again.)

[Yaël Dillies]

tactic#nlinarith is not complete, but works in practice

[Eric Rodriguez]

(it certainly works more often than I have seen from omega haha, I do think I'm using it wrong though)

[David Loeffler]

Yaël Dillies said:

tactic#nlinarith is not complete, but works in practice

What exactly do you mean by "works in practice" ? It seems to be very, very weak; it does succeed in showing that ∀ (x y : ℝ), 0 ≤ x ^ 2 + y ^ 2, but it gets stuck if you ask for 0 ≤ x ^ 4 + y ^ 2, or 2 * x * y ≤ x ^ 2 + y ^ 2.

[Kevin Buzzard]

I remember that it solves some really complex-looking problem which comes up when defining the basic API for the integers defined as a quotient of Nat^2 and I've always loved it for that

[Junyan Xu]

A decision procedure would solve this right away I guess.
image.png

[Geoffrey Irving]

Here's example where nlinarith needs significant help. Is there a way to avoid the sign splits?

import Mathlib

set_option maxHeartbeats 10000000 in
lemma nlinarith_wish {a b c d x u v : ℝ} (ab : a ≤ b) (cd : c ≤ d)
    (xac : x ≤ a * c) (xad : x ≤ a * d) (xbc : x ≤ b * c) (xbd : x ≤ b * d)
    (au : a ≤ u) (ub : u ≤ b) (cv : c ≤ v) (vd : v ≤ d) : x ≤ u * v := by
  --nlinarith  -- I wish this one worked, but it does not
  all_goals cases nonpos_or_nonneg c
  all_goals cases nonpos_or_nonneg d
  all_goals cases nonpos_or_nonneg u
  all_goals cases nonpos_or_nonneg v
  repeat nlinarith

[Eric Wieser]

Possibly worth remembering that linarith is currently buggy (#2717, #8875), which almost certainly impacts nlinarith too. Of course, it's possible that your example is not in scope of what it's supposed to do either.

[Kevin Buzzard]

I thought that nlinarith was little more than linarith + positivity + "squares are nonnegative"

[Eric Rodriguez]

I think it also does "Nat is nonnegative"

[Kevin Buzzard]

My point is that it really might not be in scope, my memory was that it was a quick hack to get some basic extension of linarith that knew some basic nonlinear stuff. The known decision procedures for the whole thing have really crappy runtime, right?

[Alex J. Best]

linarith itself should handle nats are nonnegative if I understand correctly #7439

[Geoffrey Irving]

Is there any other machinery that would solve my example in one go?

[Geoffrey Irving]

@Kevin Buzzard They have bad worst-case runtime, but I don’t know if that means they aren’t practical.

[Heather Macbeth]

@Geoffrey Irving John Harrison has an implementation of a "semidecision procedure" (if that's the word) for linearly ordered rings/fields in HOL Light. I've thought for a while that it would be nice to port it to Lean.

[Heather Macbeth]

It looks to be quite a bit easier to implement than the full cylindrical algebraic decomposition algorithm.

[Heather Macbeth]

Here's the article: https://www.cl.cam.ac.uk/~jrh13/papers/sos.html

[Eric Rodriguez]

Oh, would this be polyrith vibes, i.e. cert can be generated by fast external program?

[Heather Macbeth]

Also see page 6 and 7 of this article by Parrilo (to whom Harrison attributes the main idea):
https://www.mit.edu/~6.454/www_fall_2001/cmcaram/parrilo.pdf

[Heather Macbeth]

The basic idea: given a problem like

a b c : R
h : a * x ^ 2 + b * x + c = 0
⊢ b ^ 2 - 4 * a * c ≥ 0

come up with a proof by magic identity + Grobner basis verification:

calc
  b ^ 2 - 4 * a * c = (2 * a * x + b) ^ 2 := by linear_combination -4 * a * h
  _ ≥ 0 := by positivity

[Heather Macbeth]

The process could still be slow, though. Let $E$ be the polynomial expression you want to prove to be nonnegative (subject to certain polynomial constraints in the same variables). If I understand correctly, in general there will be no magic identity to turn $E$ into a sum of squares. But there will be a magic identity to turn $A^nE$ into a sum of squares, for large enough $n$, where $A=x^2+y^2+\ldots$ is the sum of the squares of all the variables occuring in the problem. So you iterate, $n=0,1,2,3\ldots$

[Geoffrey Irving]

Fortunately that process would generate a certificate that could then be baked into the saved proof.

[Geoffrey Irving]

To clarify, why is this only a semidecision procedure? If I'm reading Theorem 4 and the implementation right, if you run the SDP in high enough precision and iterate through enough powers, you'll eventually find the certificate. Is that right?

[Heather Macbeth]

I guess because if you present it with something false, it will never terminate.

[Geoffrey Irving]

Ah, sorry, of course. :)

[Geoffrey Irving]

Is it possible to map a certificate of SDP failure to an attempted counterexample, with some loss? I'm curious if some of the proving work could be reused as counterexample work.

[Heather Macbeth]

I don't know of any way of doing that. On the other hand, you can probably hook up (different) external software to find and check counterexamples directly.

[Heather Macbeth]

That is, the numbers themselves form the certificate for an existentially-quantified problem, whereas you need some cleverness (such as Harrison's idea with the magic identity producing a sum-of-squares expression) to produce a certificate for a universally-quantified problem.

[Heather Macbeth]

For example, Li-Passmore-Paulson (section 7 here) use Mathematica for numerical witnesses.