Feature: Nonlinear Arithmetic (Sum-of-Squares)

[charles-cooper]

primarily authored by Claude Opus 4.6, updated with review feedback

Feature: Nonlinear Arithmetic for HOL4

Problem

HOL4 handles polynomial equalities via Gröbner bases (REAL_RING, NUM_RING, INT_RING) and linear inequality reasoning via REAL_ARITH / ARITH_TAC / COOPER_TAC. But there is no automated support for nonlinear inequalities:

(* These all fail with "linear_ineqs: no contradiction" *)
REAL_ARITH ``x pow 2 >= &0``
REAL_ARITH ``x >= &5 /\ y >= &5 ==> x * y >= &25``
REAL_ARITH ``&2 * x * y <= x pow 2 + y pow 2``  (* AM-GM *)

Users must currently manually decompose these into sum-of-squares form by hand.

Proposed Solution: Layered Approach

A three-phase approach, where each phase is independently useful and builds on the last:

• Phase 0: Heuristic nonlinear prover — no external dependencies (~500 LOC)
• Phase 1: SOS via CSDP with certificate caching (~1100 LOC)
• Phase 2: Univariate Sturm sequences — complete for 1 variable (~2000 LOC)

Phase 0: Heuristic Nonlinear Prover (no external dependencies)

The key insight is that HOL4 already has the positivstellensatz certificate verifier (hol_of_positivstellensatz in RealArith0.sml) and the GEN_REAL_ARITH framework. What's missing is a certificate finder for nonlinear goals. Phase 0 adds simple heuristic strategies that find certificates for common patterns without any external solver:

Strategy 1 — Linearization (adapted from Coq micromega's nra): Abstract nonlinear monomials as fresh variables, derive bounds from hypotheses, then call the existing REAL_LINEAR_PROVER. For example, given x ≥ 5 ∧ y ≥ 5 ⊢ x*y ≥ 25: introduce z = x*y, derive z ≥ 5*5 = 25 from the hypothesis bounds, then the goal is linear in z.

Strategy 2 — Simple certificate patterns: Try basic positivstellensatz certificate shapes:

• Square(t) for goals like t² ≥ 0
• Sum(Square(t₁), Square(t₂)) for t₁² + t₂² ≥ 0
• Product(Axiom_le i, Axiom_le j) for product-of-nonneg goals

Strategy 3 — Multiplication of hypotheses: Given hypotheses h₁ ≥ 0, ..., hₙ ≥ 0, try multiplying pairs/triples and adding to see if the goal follows by linear reasoning. This is what enumerate_products does in HOL-Light's SOS but with a bounded search.

Strategy 4 — Exact rational Cholesky for quadratic forms: For a goal p(x₁,...,xₙ) ≥ 0 where p has degree 2, write p = vᵀMv where v = [1, x₁, ..., xₙ]. Compute M by coefficient matching (exact rationals). Attempt exact rational Cholesky decomposition of M. If M = LLᵀ succeeds, read off the SOS decomposition directly — no SDP, no numerics, no rounding. This handles all nonneg quadratic forms: e.g. x² - xy + y² ≥ 0 → Cholesky → (x - y/2)² + 3y²/4 ≥ 0.

Strategy 5 — Verify-then-search with Z3/cvc5: If HolSmt is available, send the goal to Z3/cvc5 in oracle mode first. If it returns SAT (goal is invalid), fail immediately — don't waste time searching for a certificate that doesn't exist. If it returns UNSAT (goal is valid), run the heuristic search with higher degree bounds since we know a certificate exists. If heuristics find a certificate, produce a kernel-verified theorem (no oracle tag). If heuristics fail despite knowing the goal is valid, fall back to oracle-tagged theorem. This turns HolSmt from "alternative" into "complement."

This phase handles goals like x² ≥ 0, x ≥ 0 ∧ y ≥ 0 ⟹ x*y ≥ 0, x ≥ 5 ∧ y ≥ 5 ⟹ x*y ≥ 25, 2*x*y ≤ x² + y², and all nonneg quadratic forms — with no external dependencies.

Phase 1: SOS via SDP (CSDP)

For goals that heuristics can't handle, use the full Positivstellensatz approach from HOL-Light's sos.ml:

1. Normalize all terms to canonical polynomial form (via existing REAL_POLY_CONV)
2. Compute the Newton polytope to minimize the monomial basis
3. Formulate "this polynomial is non-negative" as a semidefinite program (SDP)
4. Call CSDP (external, untrusted SDP solver) to find a numerical solution
5. Round the floating-point result to exact rational coefficients
6. Build a positivstellensatz certificate (Square, Sum, Product, ...)
7. Verify the certificate in HOL4's kernel via hol_of_positivstellensatz

Key property: CSDP is untrusted. It only finds certificates. Verification is purely algebraic, inside the HOL4 kernel. A buggy solver can cause the tactic to fail, never to produce an unsound theorem.

Certificate caching (following Isabelle's pattern): When CSDP finds a certificate, print it in a serialized form. Users can then embed the certificate string in their proof script (e.g., REAL_SOS_CERT "...") so the proof replays without CSDP. This means:

• Development time: need CSDP installed to discover proofs
• CI / distribution: certificates are self-contained, no CSDP needed
• Proofs are reproducible and deterministic

Phase 2: Univariate Sturm Sequences

For completeness on univariate goals, formalize Sturm's theorem in HOL4. This gives a complete decision procedure for sentences of univariate real arithmetic.

HOL4 already has: polynomial evaluation, IVT (POLY_IVT_POS), root finiteness (POLY_ROOTS_FINITE), squarefree decomposition (POLY_SQUAREFREE_DECOMP_ORDER). What's needed:

• Sturm sequence (pseudo-remainder sequence) computation
• Sign variation counting
• The Sturm-Tarski theorem connecting sign variations to root counts
• Root isolation

Architecture follows Li/Paulson (Isabelle): the actual root isolation can be done by an untrusted oracle (even a small SML implementation of ~300 LOC), with the kernel verifying that the sample points cover all sign-invariant regions via Sturm evaluation.

Existing Infrastructure

Most of the infrastructure has already been ported from HOL-Light:

Component	Source	HOL4 Status
Gröbner bases	grobner.ml	✅ Grobner.sml
Polynomial normalization	normalizer.ml	✅ Normalizer.sml
positivstellensatz type	realarith.ml	✅ RealArith0.sml
Certificate verifier (hol_of_positivstellensatz)	realarith.ml	✅ RealArith0.sml (handles Square, Sum, Product, Eqmul, Axiom_le, etc.)
GEN_REAL_ARITH framework	realarith.ml	✅ RealArith.sml (takes a prover function as parameter)
Polynomial theory (IVT, roots, order, squarefree)	—	✅ polyScript.sml
Heuristic nonlinear prover	—	❌ Phase 0
SOS core (SDP formulation + CSDP)	sos.ml	❌ Phase 1
Sturm sequences / root isolation	—	❌ Phase 2

Architecture

All phases plug into the existing GEN_REAL_ARITH framework, cascading from fast/simple to slow/powerful:

GEN_REAL_ARITH (existing framework)
    │
    ├── REAL_LINEAR_PROVER (existing, handles linear goals)
    │
    └── REAL_NONLINEAR_PROVER (new, cascading):
            │
            ├── 1. Linearization (abstract monomials → linear)  [Phase 0]
            ├── 2. Simple certificate search (squares, products) [Phase 0]
            ├── 3. SOS via CSDP (full Positivstellensatz)        [Phase 1]
            └── 4. Univariate Sturm (if single variable)         [Phase 2]
                    │
                    └── hol_of_positivstellensatz (existing, trusted verifier)

Proposed API

(* Phase 0: no external dependencies *)
val NLA_TAC       : tactic          (* heuristic nonlinear arithmetic *)
val NLA_PROVE     : term -> thm

(* Phase 1: requires CSDP for certificate discovery *)
val REAL_SOS      : term -> thm     (* nonlinear real arithmetic via SOS *)
val REAL_SOS_TAC  : tactic
val REAL_SOS_CERT : string -> term -> thm  (* replay cached certificate, no CSDP needed *)
val INT_SOS       : term -> thm     (* integer via embedding into reals *)
val SOS_RULE      : term -> thm     (* natural numbers via NUM_TO_INT_CONV *)
val SOS_CONV      : conv            (* prove p >= 0 by SOS decomposition *)
val PURE_SOS      : term -> thm     (* pure SOS, no hypothesis handling *)

(* Phase 2 *)
val STURM_TAC     : tactic          (* univariate decision procedure *)

External Dependencies

• Phase 0: None
• Phase 1: CSDP — coinor-csdp on Debian/Ubuntu. Communication via temp files in SDPA format. Configurable via HOL4_CSDP_EXECUTABLE env var. With certificate caching (REAL_SOS_CERT), CSDP is only needed at proof development time, not for replay.
• Phase 2: None (or optionally Z3/cvc5 as untrusted oracle for faster root isolation)

Example Goals

(* Basic positivity *)
REAL_SOS ``x pow 2 >= &0``
REAL_SOS ``x pow 2 + y pow 2 >= &0``
REAL_SOS ``x pow 4 + y pow 4 + z pow 4 >= &0``

(* With hypotheses *)
REAL_SOS ``x >= &5 /\ y >= &5 ==> x * y >= &25``
REAL_SOS ``x >= &0 /\ y >= &0 ==> x * y >= &0``

(* Classic inequalities *)
REAL_SOS ``&2 * x * y <= x pow 2 + y pow 2``           (* AM-GM *)
REAL_SOS ``x pow 6 + y pow 6 + z pow 6
           >= &3 * x pow 2 * y pow 2 * z pow 2``        (* Schur-like *)
PURE_SOS ``x pow 4 + y pow 4 + z pow 4
           - &4 * x * y * z + x + y + z + &3 >= &1 / &7``

(* Integer / Natural number *)
INT_SOS ``(x:int) * x >= 0``
SOS_RULE ``x >= 5 /\ y >= 5 ==> x * y >= 25``
SOS_RULE ``n * n + n >= n``

(* From HOL-Light's test suite *)
REAL_SOS ``&2 * x pow 4 + &2 * x pow 3 * y
           - x pow 2 * y pow 2 + &5 * y pow 4 >= &0``

Completeness Properties

Phase	Domain	Completeness	Notes
0	ℝ (heuristic)	Incomplete	Handles common patterns: squares, products of nonneg, linearizable goals
1	ℝ (REAL_SOS)	Theoretically complete	By Stengle's Positivstellensatz. Practically limited by SDP precision and degree bound.
1	ℤ (INT_SOS)	Incomplete	Sound: embeds into reals. Fails when integrality matters.
1	ℕ (SOS_RULE)	Incomplete	Via NUM_TO_INT_CONV → INT_SOS. ℕ subtraction/DIV/MOD handled by NUM_SIMPLIFY_CONV preprocessing.
2	ℝ univariate	Complete	Sturm-Tarski theorem gives a decision procedure for univariate real arithmetic.

Connection to HolSmt / cvc5 Alethe Replay

The cvc5 Alethe proof replay work (#1829) falls back to oracle for nonlinear theory lemmas (la_generic only handles linear arithmetic). Even Phase 0 heuristics would allow kernel-verified replay of many nonlinear theory lemma steps that currently require oracle tags.

Alternatives Considered

Approach	Pros	Cons	Verdict
SMT oracle (Z3 nlsat / cvc5 CAD)	Complete for QF_NRA, no new code	Oracle-tagged theorems, no kernel verification	Complementary — useful for finding goals are valid, but SOS/heuristics verify in kernel
Implementing Z3's nlsat in HOL4 tactics	Complete, no external deps	nlsat is a search procedure, not certificate-based; doesn't fit the trusted-kernel architecture well. Would need ~5000+ LOC of verified search.	Not practical as first step
Full multivariate CAD (Collins-style)	Complete decision procedure	Nobody has formalized this in any prover. BKR hybrid (Isabelle) took ~11K LOC of Isabelle theory.	Future work; univariate CAD (Phase 2) is achievable
Interval arithmetic	Simple, no dependencies	Very incomplete, ground terms only	Useful complement but not a substitute
Manual decomposition	Works today	Requires user expertise, tedious	What users do now; we're automating this

Why this layered approach: Phase 0 (heuristics) gives immediate value with zero dependencies. Phase 1 (SOS) handles harder goals with an optional external solver. Phase 2 (Sturm) gives completeness for univariate problems. Each phase is independently useful.

Why not Z3's nlsat directly? @someplaceguy suggested implementing Z3's nonlinear algorithm in HOL4 tactics. Z3's nlsat uses MCSAT + CAD projections — a search procedure that incrementally builds models and generates conflict clauses. This doesn't naturally produce compact checkable certificates the way SOS does. The Positivstellensatz certificate architecture (untrusted finder → trusted kernel checker) is a better fit for theorem provers, and is what HOL-Light, Isabelle, and Coq all use.

Implementation Details

positivstellensatz Constructor Access

The SOS and heuristic code must construct certificates using Square, Sum, Product, Axiom_le, etc. Currently these constructors are abstract (not exported from RealArith0.sig). Options:

• (a) Export the datatype constructors from RealArith0.sig
• (b) Add smart constructor functions (e.g., mk_Square : term -> positivstellensatz)
• (c) Place the nonlinear prover code inside a structure that has access (same compilation unit)

Natural Number Ergonomics

Most HOL4 users write over ℕ. The ℕ → ℤ → ℝ → SOS → back chain involves NUM_TO_INT_CONV and NUM_SIMPLIFY_CONV (already in Grobner.sml) to handle truncating subtraction, DIV, MOD, PRE, EVEN/ODD before converting to real arithmetic.

Benchmarks

Test cases should come from:

• HOL-Light's sos.ml test suite (~50 examples)
• SMT-LIB QF_NRA benchmarks (adapted)
• Real HOL4 proofs that currently use oracle-mode SMT for nonlinear goals
• Coq micromega test suite

Questions

1. File placement: src/real/sosLib.{sig,sml} alongside RealField? Or a new src/real/sos/ directory?

2. positivstellensatz constructors: Which approach for accessing the abstract type? (see above)

3. Integration with REAL_ARITH: Should REAL_ARITH automatically try nonlinear heuristics as a fallback when linear arithmetic fails? Or keep them strictly separate? (HOL-Light keeps them separate; Coq's auto doesn't call nra)

4. CI: Phase 0 tests need no special setup. Phase 1 (CSDP) tests should gate on availability like HolSmt gates on Z3/cvc5. Phase 2 tests need no special setup.

5. Naming: sosLib (algorithm name) vs nlrealLib (domain name) vs nonlinearLib? The Phase 0 heuristics aren't really "SOS" so a broader name might be better.

[charles-cooper]

paging @someplaceguy @mn200 @xrchz for feedback

[charles-cooper]

CAD (Cylindrical Algebraic Decomposition) Complete decision procedure ~5000+ LOC, much harder to implement

this sounds pretty good actually, thoughts?

[charles-cooper]

primarily authored by Claude Opus 4.6

Follow-up: CAD and Completeness

After more investigation, I want to revisit the "CAD is too hard" claim in the original proposal. The situation is more nuanced.

What Exists in Other Provers

Approach	System	LOC (implementation)	External deps	Complete?
SOS via SDP	HOL-Light, Isabelle, Coq	~1900 (OCaml)	CSDP	Theoretically yes, practically limited
Univariate CAD (certificate-based)	Isabelle (Li/Paulson)	~1600 ML + ~8400 Isabelle	Mathematica	Yes (univariate)
Multivariate QE (BKR hybrid)	Isabelle (Kosaian/Tan/Platzer)	~10900 Isabelle	None (fully verified)	Yes (all of QF_NRA)
Collins-style CAD	Nobody has formalized this	—	—	—

The Key Insight: Certificate-Based Approach

Both SOS and CAD can use the same architecture: an untrusted oracle finds the proof certificate, and a trusted kernel verifier checks it. The question is what oracle and what certificates.

For SOS:

• Oracle: CSDP (SDP solver)
• Certificate: Positivstellensatz witness (sums of squares + products of hypotheses)
• Verifier: hol_of_positivstellensatz (algebraic identity checking)

For univariate CAD:

• Oracle: could be Mathematica, Z3, cvc5, or even a small SML implementation
• Certificate: list of sample points where the formula has been verified, plus proof that these sample points cover all sign-invariant regions
• Verifier: Sturm sequence evaluation + polynomial sign checking at rational points

What Would a Univariate CAD for HOL4 Look Like?

Li's approach in Isabelle uses Mathematica as the oracle, but the oracle just needs to:

1. Isolate real roots of a set of polynomials
2. Return rational sample points between consecutive roots

Z3/cvc5 could serve as this oracle. When we run Z3_TAC or CVC_TAC on a nonlinear goal and it returns UNSAT, the solver has essentially performed CAD internally. The missing piece is extracting a checkable certificate from the solver output.

Alternatively, a small SML implementation of root isolation (~300-500 LOC using Sturm sequences or Descartes' rule) could serve as the oracle with no external dependencies at all. The oracle doesn't need to be verified — it just needs to produce candidate sample points that the kernel then checks.

Practical Assessment

Approach	New HOL4 code needed	External deps	Completeness
SOS (proposed)	~1100 LOC	CSDP	Practically limited
SOS + univariate CAD	~2500 LOC	CSDP + (Mathematica OR none)	Complete for univariate, SOS for multivariate
SOS + full multivariate	~8000+ LOC	CSDP	Complete for all QF_NRA

Recommendation: Layered Approach

1. Phase 1 (this proposal): SOS via CSDP. Handles most practical goals. ~1100 LOC.
2. Phase 2: Univariate Sturm sequences in HOL4. Formalizing Sturm's theorem gives us both a complete univariate decision procedure AND better root isolation for SOS. Adds ~1500 LOC of HOL4 theory + ~500 LOC of ML.
3. Phase 3 (stretch): If demand exists, use Z3/cvc5 as an oracle for multivariate problems, with kernel verification of the witness.

The honest answer is: CAD isn't "too hard" in an absolute sense, but it's harder than SOS for the first iteration. SOS gets us 80% of the practical value at 20% of the implementation cost. A univariate CAD as Phase 2 is quite achievable and would close the completeness gap for single-variable problems.

What HOL4 Already Has (relevant to CAD)

• polyTheory: polynomial evaluation, roots, IVT (POLY_IVT_POS), orders, squarefree decomposition (POLY_SQUAREFREE_DECOMP_ORDER), finite roots (POLY_ROOTS_FINITE)
• realTheory: real arithmetic, completeness (sup/inf)
• Grobner.sml: polynomial ideal operations

What's missing for univariate CAD:

• Sturm sequence computation (pseudo-remainder sequences)
• Sign variation counting
• Root isolation (follows from Sturm sequences)
• Formal connection between sample point evaluation and universal validity

[charles-cooper]

primarily authored by Claude Opus 4.6

Issue body has been updated with a revised design:

• Layered approach (Phase 0/1/2) instead of SOS-only
• Phase 0: Heuristic nonlinear prover with no external dependencies (~500 LOC) — linearization (à la Coq micromega), simple certificate pattern search, hypothesis multiplication
• Phase 1: SOS via CSDP with certificate caching (Isabelle-style REAL_SOS_CERT "..." so proofs replay without CSDP)
• Phase 2: Univariate Sturm sequences for completeness on single-variable problems
• Added connection to cvc5 Alethe replay (HolSmt: add cvc5 Alethe proof replay #1829) — even Phase 0 heuristics help replay nonlinear theory lemmas
• Addressed why not Z3's nlsat directly — search procedures don't produce compact certificates; Positivstellensatz architecture fits theorem provers better
• Added notes on positivstellensatz constructor access, natural number ergonomics, benchmarking sources

The earlier CAD follow-up comment is now incorporated into the main body.

[xrchz]

No major concerns from me after a skim (I'm not super familiar with these theories/tactics in any case) -- I would say go for it!

[mn200]

Agreed; it's very appealing!

[tanyongkiam]

I recommend focusing or starting only on Phase 1 (which essentially is to port HOL light's SOS_TAC). This is also available in Isabelle (under "sos"). I believe (but cannot confirm) that the Phase 0 plans are already subsumed inside sos preprocessing.

I wouldn't recommend going for Phase 2 (or trying for full NRA via CAD / other means, which do exist).

[charles-cooper]

I recommend focusing or starting only on Phase 1 (which essentially is to port HOL light's SOS_TAC). This is also available in Isabelle (under "sos"). I believe (but cannot confirm) that the Phase 0 plans are already subsumed inside sos preprocessing.

I wouldn't recommend going for Phase 2 (or trying for full NRA via CAD / other means, which do exist).

claude reports:

Phase 0 vs SOS preprocessing: I looked at HOL-Light's sos.ml carefully. The SOS preprocessing (enumerate_products) builds a monoid for the Positivstellensatz cone and feeds it into the SDP. Phase 0 does something different — it generates product-of-hypothesis theorems and feeds them to the linear prover. For goals like x ≥ 5 ∧ y ≥ 5 ⟹ x*y ≥ 25, Phase 0 generates ⊢ (x-5)*(y-5) ≥ 0 and the linear prover closes it immediately, with no external tool. SOS would set up a full SDP for this. So they're complementary rather than one subsuming the other — Phase 0 handles "product-of-bounds + linear reasoning" cheaply, SOS handles intrinsically nonlinear goals (sum-of-squares decompositions) that Phase 0 can't touch.

Phase 1 plan: Agree SOS is the high-value target. HOL-Light's sos.ml is BSD-2-Clause so we can port it freely. I'm planning to split it:

• Phase 1a (pure SOS, no external deps): Newton polytope → Gram matrix → exact rational Cholesky. This handles goals that are literally sums of squares (e.g. x² + y² ≥ 2xy) without needing CSDP. ~500 LOC.
• Phase 1b (full SOS via CSDP): SDPA-format interface, floating-point SDP → rational rounding → certificate verification. Handles the general Positivstellensatz. ~1000 LOC additional.

Phase 1a combined with Phase 0 should cover most practical NLA goals without any external dependency. Phase 1b adds the heavy machinery for harder cases.