Merge pull request #51 from ForeverHaibara/setup

Setup

Author: ForeverHaibara

.gitignore

@@ -7,4 +7,8 @@ __pycache__/
 .trae/
 .benchmarks/
 *.log
-.coverage
+.coverage
+
+build/
+dist/
+*.egg-info/

LICENSE

@@ -1,5 +1,7 @@
 # Triples
 
+[![PyPI version](https://img.shields.io/pypi/v/triples.svg)](https://pypi.org/project/triples/)
+
 Triples 是由 forever豪3 开发的基于 Python 的 SymPy 库的多项式不等式自动证明程序。其专注于通过配方法生成不等式的可读证明。它同时提供直观的图形界面与代码接口，助力代数不等式的探索。
 
 Triples is an automatic inequality proving software developed by ForeverHaibara, based on the Python SymPy library. It focuses on generating readable proofs of inequalities through sum of squares (SOS). The program offers both a graphical user interface and a code interface to facilitate the exploration of Olympiad-level algebraic inequalities.
@@ -43,13 +45,10 @@ Triples is an automatic inequality proving software developed by ForeverHaibara,
 
 See more in the Jupyter notebook:    [notebooks/examples.ipynb](notebooks/examples.ipynb)
 
-Ensure "triples" is in the directory or the system path.
+Triples has hard dependencies on Python>=3.6, SymPy>=1.9, NumPy, SciPy, and an SDP solver, e.g., Clarabel. It can now be installed via pip:
 
 ```
-pip install sympy
-pip install numpy
-pip install scipy
-pip install clarabel
+pip install triples
 ```
 
 ```py
@@ -60,7 +59,7 @@ a, b, c, x, y, z = sp.symbols("a b c x y z")
 
 ### Sum of Squares
 
-Given a sympy polynomial, the `sum_of_squares` solver  will return a Solution-class object if it succeeds. It returns None if it fails (but it does not mean the polynomial is not a sum of squares or positive semidefinite).
+Given a sympy expression, the `sum_of_squares` solver  will return a Solution-class object if it succeeds. It returns None if it fails (but it does not mean the expression is not a sum of squares or positive semidefinite).
 
 **Example 1** $a,b,c\in\mathbb{R}$, prove:  $\left(a^2+b^2+c^2\right)^2\geq 3\left(a^3b+b^3c+c^3a\right)$.
 
@@ -74,7 +73,7 @@ Given a sympy polynomial, the `sum_of_squares` solver  will return a Solution-cl
 
 <br>
 
-If there are inequality or equality constraints, send them as a list of sympy expressions to `ineq_constraints` and `eq_constraints`.
+If there are inequality or equality constraints, send them as a list of sympy expressions to `ineq_constraints` and `eq_constraints`. (These are the second and third arguments of the `sum_of_squares` function.)
 
 **Example 2** $a,b,c\in\mathbb{R}_+$, prove:  $a(a-b)(a-c)+b(b-c)(b-a)+c(c-a)(c-b)\geq 0$.
 
@@ -105,19 +104,15 @@ x*(Σ(2*F(a) + 13))/6 + Σ(a - b)**2*F(c) + (Σ(a - 1)**2*F(b)*F(c))/6 + 5*(Σ(a
 
 ## 图形化界面 Graphic User Interface
 
-本程序图形化界面有两种启动方式: Flask 与 Gradio.
+本程序图形化界面有两种启动方式: Flask 与 Gradio. 使用图形化界面必须下载完整的仓库, 而非使用 pip 安装.
 
-Two graphical backends are supported: Flask and Gradio.
+Two graphical backends are supported: Flask and Gradio. To use the graphical interface, you need to download the full repository instead of installing via pip.
 
 ### Flask 启动
 
 1. 安装依赖: Install Dependencies
 
 ```
-pip install sympy
-pip install numpy
-pip install scipy
-pip install clarabel
 pip install flask
 pip install flask_cors
 pip install flask_socketio
@@ -131,12 +126,7 @@ pip install flask_socketio
 1. 安装依赖: Install Dependencies
 
 ```
-pip install sympy
-pip install numpy
-pip install scipy
-pip install clarabel
 pip install gradio>=5.0
-pip install pillow
 ```
 
 1. 控制台中运行 `python gradio.app.py` 启动后端. Run `python gradio.app.py` to launch the backend.

README.md

@@ -0,0 +1,67 @@
+# Triples
+
+Triples is an automatic inequality proving software developed by ForeverHaibara, based on the Python SymPy library. It focuses on generating readable proofs of inequalities through sum of squares (SOS). The program offers both a graphical user interface and a code interface to facilitate the exploration of Olympiad-level algebraic inequalities.
+
+Homepage: [https://github.com/ForeverHaibara/Triple-SOS](https://github.com/ForeverHaibara/Triple-SOS)
+
+To install, use:
+```
+pip install triples
+```
+
+## Code Usage
+
+```py
+from triples import sum_of_squares
+import sympy as sp
+a, b, c, x, y, z = sp.symbols("a b c x y z")
+```
+
+### Sum of Squares
+
+Given a sympy polynomial, the `sum_of_squares` solver  will return a Solution-class object if it succeeds. It returns None if it fails (but it does not mean the polynomial is not a sum of squares or positive semidefinite).
+
+**Example 1** $a,b,c\in\mathbb{R}$, prove:  $\left(a^2+b^2+c^2\right)^2\geq 3\left(a^3b+b^3c+c^3a\right)$.
+
+```py
+>>> sol = sum_of_squares((a**2 + b**2 + c**2)**2 - 3*(a**3*b + b**3*c + c**3*a))
+>>> sol.solution # this should be a sympy expression
+(Σ(a**2 - a*b - a*c - b**2 + 2*b*c)**2)/2
+>>> sol.solution.doit() # this expands the cyclic sums
+(-a**2 + 2*a*b - a*c - b*c + c**2)**2/2 + (a**2 - a*b - a*c - b**2 + 2*b*c)**2/2 + (-a*b + 2*a*c + b**2 - b*c - c**2)**2/2
+```
+
+<br>
+
+If there are inequality or equality constraints, send them as a list of sympy expressions to `ineq_constraints` and `eq_constraints`.
+
+**Example 2** $a,b,c\in\mathbb{R}_+$, prove:  $a(a-b)(a-c)+b(b-c)(b-a)+c(c-a)(c-b)\geq 0$.
+
+```py
+>>> sol = sum_of_squares(a*(a-b)*(a-c) + b*(b-c)*(b-a) + c*(c-a)*(c-b), ineq_constraints = [a,b,c])
+>>> sol.solution
+((Σ(a - b)**2*(a + b - c)**2)/2 + Σa*b*(a - b)**2)/(Σa)
+```
+
+<br>
+
+If you want to track the inequality and equality constraints, you can send in a dict containing the alias of the constraints.
+
+**Example 3** $a,b,c\in\mathbb{R}_+$ and $abc=1$, prove: $\sum \frac{a^2}{2+a}\geq 1$.
+
+```py
+>>> sol = sum_of_squares(((a+2)*(b+2)*(c+2)*(a**2/(2+a)+b**2/(2+b)+c**2/(2+c)-1)).cancel(), ineq_constraints=[a,b,c], eq_constraints={a*b*c-1:x})
+>>> sol.solution
+x*(Σ(2*a + 13))/6 + Σa*(b - c)**2 + (Σa*b*(c - 1)**2)/6 + 5*(Σ(a - 1)**2)/6 + 7*(Σ(a - b)**2)/12
+>>> sol.solution.doit()
+a*b*(c - 1)**2/3 + a*c*(b - 1)**2/3 + a*(-b + c)**2 + a*(b - c)**2 + b*c*(a - 1)**2/3 + b*(-a + c)**2 + b*(a - c)**2 + c*(-a + b)**2 + c*(a - b)**2 + x*(4*a + 4*b + 4*c + 78)/6 + 7*(-a + b)**2/12 + 7*(-a + c)**2/12 + 5*(a - 1)**2/3 + 7*(a - b)**2/12 + 7*(a - c)**2/12 + 7*(-b + c)**2/12 + 5*(b - 1)**2/3 + 7*(b - c)**2/12 + 5*(c - 1)**2/3
+>>> F = sp.Function("F")
+>>> sol = sum_of_squares(((a+2)*(b+2)*(c+2)*(a**2/(2+a)+b**2/(2+b)+c**2/(2+c)-1)).cancel(), {a: F(a), b: F(b), c: F(c)}, {a*b*c-1:x})
+>>> sol.solution
+x*(Σ(2*F(a) + 13))/6 + Σ(a - b)**2*F(c) + (Σ(a - 1)**2*F(b)*F(c))/6 + 5*(Σ(a - 1)**2)/6 + 7*(Σ(a - b)**2)/12
+```
+
+
+## Warnings
+
+* The `triples` package uses dynamic patches to fix some known bugs in the SymPy library for older versions of SymPy, and may slightly affect the behaviour of SymPy. This includes a fix for `radsimp` at [https://github.com/sympy/sympy/pull/26720](https://github.com/sympy/sympy/pull/26720) and setting `CRootOf.is_algebraic = True` at [https://github.com/sympy/sympy/pull/26806](https://github.com/sympy/sympy/pull/26806).

notebooks/README_pypi.md

@@ -0,0 +1,47 @@
+[build-system]
+requires = ["setuptools>=61.0", "wheel"]
+build-backend = "setuptools.build_meta"
+
+[project]
+name = "triples"
+version = "0.1.0"
+description = "Automatic sum-of-squares proofs for algebraic inequalities"
+readme = "notebooks/README_pypi.md"
+license = {file = "LICENSE"}
+authors = [
+    {name = "ForeverHaibara", email = "1378855363@qq.com" },
+]
+requires-python = ">=3.6"
+dependencies = [
+    "numpy",
+    "scipy",
+    "sympy>=1.9",
+    "clarabel; python_version >= '3.7'",
+    "cvxopt; python_version < '3.7'",
+]
+keywords = ["sum-of-squares", "SOS", "inequality", "solver", "optimization"]
+classifiers = [
+    "Development Status :: 4 - Beta",
+    "Intended Audience :: Science/Research",
+    "License :: OSI Approved :: GNU General Public License v3 (GPLv3)",
+    "Programming Language :: Python :: 3",
+    "Programming Language :: Python :: 3.6",
+    "Programming Language :: Python :: 3.7",
+    "Programming Language :: Python :: 3.8",
+    "Programming Language :: Python :: 3.9",
+    "Programming Language :: Python :: 3.10",
+    "Programming Language :: Python :: 3.11",
+    "Programming Language :: Python :: 3.12",
+    "Programming Language :: Python :: 3.13",
+    "Topic :: Scientific/Engineering :: Mathematics",
+]
+
+[project.urls]
+"Homepage" = "https://github.com/ForeverHaibara/Triple-SOS"
+
+[tool.setuptools.packages.find]
+where = ["."]
+include = ["triples*"]
+
+[tool.setuptools.package-data]
+triples = ["**/*.npz"]

pyproject.toml

@@ -1,7 +1,15 @@
-from .utils import pl, CyclicSum, CyclicProduct
-from .core import sum_of_squares
+from .utils import pl, CyclicSum, CyclicProduct, generate_monoms
+
+from .core import sum_of_squares, StructuralSOS, LinearSOS, SDPSOS, SOSPoly
+
+from .sdp import SDPProblem, congruence
+
+__version__ = "0.1.0"
 
 __all__ = [
-    'pl', 'CyclicSum', 'CyclicProduct',
-    'sum_of_squares'
+    '__version__',
+
+    'pl', 'CyclicSum', 'CyclicProduct', 'generate_monoms',
+    'sum_of_squares', 'StructuralSOS', 'LinearSOS', 'SDPSOS', 'SOSPoly',
+    'SDPProblem', 'congruence'
 ]

triples/__init__.py

@@ -6,34 +6,40 @@
     sum_of_squares, sum_of_squares_multiple
 )
 
+from .preprocess import (
+    ReformulateAlgebraic, CancelDenominator, SolveMul, SolvePolynomial
+)
+
 from .linsos import (
-    LinearSOS,
+    LinearSOS, LinearSOSSolver
 )
 
 from .structsos import (
-    StructuralSOS, prove_univariate
+    StructuralSOS, StructuralSOSSolver, prove_univariate
 )
 
 from ..utils import pqr_sym, pqr_cyc, pqr_ker
 
 from .symsos import (
-    SymmetricSOS, sym_representation, sym_representation_inv,
+    SymmetricSOS, SymmetricSubstitution, sym_representation, sym_representation_inv,
+
 )
 
 from .sdpsos import (
-    SDPSOS, SDPProblem, JointSOSElement, SOSPoly, SOHSPoly
+    SDPSOS, SDPSOSSolver, SDPProblem,
+    JointSOSElement, SOSPoly, SOHSPoly, SOSMomentPoly,
 )
 
 __all__ = [
     'ProofNode', 'ProofTree',
     'InequalityProblem',
     'Solution',
     'sum_of_squares', 'sum_of_squares_multiple',
-    'LinearSOS',
-    'StructuralSOS',
-    'prove_univariate',
+    'ReformulateAlgebraic', 'CancelDenominator', 'SolveMul', 'SolvePolynomial',
+    'LinearSOS', 'LinearSOSSolver',
+    'StructuralSOS', 'StructuralSOSSolver', 'prove_univariate',
     'pqr_sym', 'pqr_cyc', 'pqr_ker',
-    'SymmetricSOS', 'sym_representation', 'sym_representation_inv',
-    'SDPSOS', 'SDPProblem', 'JointSOSElement', 'SOSPoly', 'SOHSPoly'
-
+    'SymmetricSOS', 'SymmetricSubstitution', 'sym_representation', 'sym_representation_inv',
+    'SDPSOS', 'SDPSOSSolver', 'SDPProblem',
+    'JointSOSElement', 'SOSPoly', 'SOHSPoly', 'SOSMomentPoly',
 ]

triples/core/__init__.py

@@ -5,12 +5,18 @@
 
 from ..node import ProofNode, ProofTree
 from .features import get_features
+from .modeling import ReformulateAlgebraic
+from .algebraic import CancelDenominator, SolveMul
 from .polynomial import SolvePolynomial
 from .reparam import Reparametrization
 from .signs import sign_sos, get_symbol_signs
 
 __all__ = [
     'ProofNode', 'ProofTree',
-    'get_features', 'SolvePolynomial', 'Reparametrization',
+    'get_features',
+    'ReformulateAlgebraic',
+    'CancelDenominator', 'SolveMul',
+    'SolvePolynomial',
+    'Reparametrization',
     'sign_sos', 'get_symbol_signs',
 ]

triples/core/preprocess/__init__.py

@@ -43,7 +43,7 @@ def get_polynomial_solvers(self, configs):
             ]
         return solvers
 
-    def explore(self, configs):        
+    def explore(self, configs):
         if self.state != 0 and len(self.children) == 0:
             # all children failed
             self.finished = True

triples/core/preprocess/polynomial.py

@@ -1,3 +1,6 @@
+"""
+To be deprecated. Do not use this file.
+"""
 from typing import Tuple, Dict, List, Union, Optional
 
 import sympy as sp