An inequality prover from maple ported to sympy

[William Zhang (mintIceCream_)]

Hello, undergrad here, i found an old chinese paper/maple script which seemed kind of interesting so i decided to port it to sympy
Heres the code and everything https://github.com/iceCreamMint/inqeuality-prover/tree/main
Its an prover for non-strict multivariable polynomial inequalities with rational coefficents and positive real variables
Theres also one for geometric inequalities involving one triangle but that part seems really complicated so i havent done anything with it yet
In my opinion the way it works is rather interesting, it does cad but ignores lower dimensional cells to avoid having to solve for roots(i think this is why it can only deal with unstrict inequalities?)
Other than that, it does some preprocessing to radicals and rationals to make them valid for cad

Currently the main bottleneck seems to be that resultants are painfully slow
For example, take
p = 6561*x**8*y**4*z**4 - 26244*x**8*y**3*z**3 + 39366*x**8*y**2*z**2 - 26244*x**8*y*z + 6561*x**8 - 26244*x**7*y**5*z**4 - 26244*x**7*y**4*z**5 + 78732*x**7*y**4*z**3 + 78732*x**7*y**3*z**4 - 78732*x**7*y**3*z**2 - 78732*x**7*y**2*z**3 + 26244*x**7*y**2*z + 26244*x**7*y*z**2 + 39366*x**6*y**6*z**4 + 26244*x**6*y**5*z**5 - 52488*x**6*y**5*z**3 + 39366*x**6*y**4*z**6 - 52488*x**6*y**4*z**4 - 39366*x**6*y**4*z**2 - 52488*x**6*y**3*z**5 + 49572*x**6*y**3*z**3 + 78732*x**6*y**3*z - 39366*x**6*y**2*z**4 - 69984*x**6*y**2*z**2 - 26244*x**6*y**2 + 78732*x**6*y*z**3 + 69984*x**6*y*z - 26244*x**6*z**2 - 23328*x**6 - 26244*x**5*y**7*z**4 + 26244*x**5*y**6*z**5 - 52488*x**5*y**6*z**3 + 26244*x**5*y**5*z**6 - 52488*x**5*y**5*z**4 + 157464*x**5*y**5*z**2 - 26244*x**5*y**4*z**7 - 52488*x**5*y**4*z**5 + 29160*x**5*y**4*z**3 - 78732*x**5*y**4*z - 52488*x**5*y**3*z**6 + 29160*x**5*y**3*z**4 + 20412*x**5*y**3*z**2 + 157464*x**5*y**2*z**5 + 20412*x**5*y**2*z**3 - 23328*x**5*y**2*z - 78732*x**5*y*z**4 - 23328*x**5*y*z**2 + 6561*x**4*y**8*z**4 - 26244*x**4*y**7*z**5 + 78732*x**4*y**7*z**3 + 39366*x**4*y**6*z**6 - 52488*x**4*y**6*z**4 - 39366*x**4*y**6*z**2 - 26244*x**4*y**5*z**7 - 52488*x**4*y**5*z**5 + 29160*x**4*y**5*z**3 - 78732*x**4*y**5*z + 6561*x**4*y**4*z**8 - 52488*x**4*y**4*z**6 + 312012*x**4*y**4*z**4 + 46656*x**4*y**4*z**2 + 39366*x**4*y**4 + 78732*x**4*y**3*z**7 + 29160*x**4*y**3*z**5 - 285768*x**4*y**3*z**3 - 46656*x**4*y**3*z - 39366*x**4*y**2*z**6 + 46656*x**4*y**2*z**4 + 57348*x**4*y**2*z**2 + 23328*x**4*y**2 - 78732*x**4*y*z**5 - 46656*x**4*y*z**3 - 62208*x**4*y*z + 39366*x**4*z**4 + 23328*x**4*z**2 + 31104*x**4 - 26244*x**3*y**8*z**3 + 78732*x**3*y**7*z**4 - 78732*x**3*y**7*z**2 - 52488*x**3*y**6*z**5 + 49572*x**3*y**6*z**3 + 78732*x**3*y**6*z - 52488*x**3*y**5*z**6 + 29160*x**3*y**5*z**4 + 20412*x**3*y**5*z**2 + 78732*x**3*y**4*z**7 + 29160*x**3*y**4*z**5 - 285768*x**3*y**4*z**3 - 46656*x**3*y**4*z - 26244*x**3*y**3*z**8 + 49572*x**3*y**3*z**6 - 285768*x**3*y**3*z**4 + 254016*x**3*y**3*z**2 - 78732*x**3*y**2*z**7 + 20412*x**3*y**2*z**5 + 254016*x**3*y**2*z**3 - 20736*x**3*y**2*z + 78732*x**3*y*z**6 - 46656*x**3*y*z**4 - 20736*x**3*y*z**2 + 39366*x**2*y**8*z**2 - 78732*x**2*y**7*z**3 + 26244*x**2*y**7*z - 39366*x**2*y**6*z**4 - 69984*x**2*y**6*z**2 - 26244*x**2*y**6 + 157464*x**2*y**5*z**5 + 20412*x**2*y**5*z**3 - 23328*x**2*y**5*z - 39366*x**2*y**4*z**6 + 46656*x**2*y**4*z**4 + 57348*x**2*y**4*z**2 + 23328*x**2*y**4 - 78732*x**2*y**3*z**7 + 20412*x**2*y**3*z**5 + 254016*x**2*y**3*z**3 - 20736*x**2*y**3*z + 39366*x**2*y**2*z**8 - 69984*x**2*y**2*z**6 + 57348*x**2*y**2*z**4 - 233280*x**2*y**2*z**2 + 20736*x**2*y**2 + 26244*x**2*y*z**7 - 23328*x**2*y*z**5 - 20736*x**2*y*z**3 + 18432*x**2*y*z - 26244*x**2*z**6 + 23328*x**2*z**4 + 20736*x**2*z**2 - 18432*x**2 - 26244*x*y**8*z + 26244*x*y**7*z**2 + 78732*x*y**6*z**3 + 69984*x*y**6*z - 78732*x*y**5*z**4 - 23328*x*y**5*z**2 - 78732*x*y**4*z**5 - 46656*x*y**4*z**3 - 62208*x*y**4*z + 78732*x*y**3*z**6 - 46656*x*y**3*z**4 - 20736*x*y**3*z**2 + 26244*x*y**2*z**7 - 23328*x*y**2*z**5 - 20736*x*y**2*z**3 + 18432*x*y**2*z - 26244*x*y*z**8 + 69984*x*y*z**6 - 62208*x*y*z**4 + 18432*x*y*z**2 + 6561*y**8 - 26244*y**6*z**2 - 23328*y**6 + 39366*y**4*z**4 + 23328*y**4*z**2 + 31104*y**4 - 26244*y**2*z**6 + 23328*y**2*z**4 + 20736*y**2*z**2 - 18432*y**2 + 6561*z**8 - 23328*z**6 + 31104*z**4 - 18432*z**2 + 4096

and compute sp.resultant(p, sp.diff(p,x), x)

computing this takes around the ballpark of 50 seconds, maple takes 4
In some cases factoring the polynomial and computing resultant between all pairs of factors is significantly faster than calling sp.resultant, but im not sure if its still the resultant at that point, program still seems to work and be correct though
So currently im trying to implement the modular resultant algorithm as described by Collins(1971) to see if it gets any faster
Other than that im trying to look for ways to allow equalities in conditions and figure out a way to deal with strict inequalites, reading about grobner bases right now and hoping that might help

In the program there are two inequality solvers, first one is xprove(statement, condition) which tries to prove condition -> statement for positive real variables, there are a bunch of tests for this
yprove just calls xprove a bunch of times to try and prove inequalities in real non-zero variables, there are no tests for this

The script/paper also seems to be related to the maple RegularChains package, i dont know if the sympy agca library does anything similar(i have a lot of reading to do)

Its my first time doing anything like this, any feedback is appreciated, thank you

[Oscar Benjamin]

There is an issue discussing adding something like this to SymPy:
https://github.com/sympy/sympy/issues/26177

> and compute sp.resultant(p, sp.diff(p,x), x)
> computing this takes around the ballpark of 50 seconds, maple takes 4

Are you saying that Maple takes 4 seconds for this and with SymPy it
takes 50 seconds?

If so then I think that is to be expected because Maple will do this
operation in its kernel which means it is basically using a C
implementation whereas SymPy hee uses a Python implementation. The
algorithms might also be different but I would expect that the SymPy
implementation would be at least 10x faster if it were in C. For some
polynomial operations SymPy can now make use of python-flint meaning
that the FLINT library which is written in C for operations like this.
Using python-flint for multivariate polynomials is not implemented in
SymPy yet but when it is it will be possible to use FLINT's resultant
routines for this.

In the meantime it might make sense to implement the solver using
python-flint directly since it only requires multivariate polynomials
with rational coefficients and python-flint provides a faster
implementation of those already for direct use.

Oscar

> --
> You received this message because you are subscribed to the Google Groups "sympy" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to sympy+un...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/sympy/04911951-4b31-4208-a083-f950e8524f11n%40googlegroups.com.

[William Zhang (mintIceCream_)]

>  There is an issue discussing adding something like this to SymPy:
> https://github.com/sympy/sympy/issues/26177

Yes, this seems to be exactly what i was trying to do

> In the meantime it might make sense to implement the solver using
> python-flint directly since it only requires multivariate polynomials
> with rational coefficients and python-flint provides a faster
> implementation of those already for direct use.

I will look into this, thank you for the suggestion