|
| 1 | +/- |
| 2 | +Copyright (c) 2026 Kim Morrison. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +
|
| 5 | +Test cases for the ℕ/ℤ DIV/MOD enrichment of the integer frontend |
| 6 | +(issues #24 and #45). Each goal contains `a / b` or `a % b` over ℕ |
| 7 | +or ℤ; the lift pre-pass introduces witness equalities and bounds |
| 8 | +before the SOS reifier runs. The leading block covers positive |
| 9 | +literal divisors (issue #24); the trailing block (after the |
| 10 | +non-literal-divisor section header) covers divisors whose positivity |
| 11 | +is derived from in-scope hypotheses via `omega` (issue #45). |
| 12 | +-/ |
| 13 | +import Mathlib.Tactic.SOS |
| 14 | + |
| 15 | +-- Trivial ℕ div lower bound: `n / 2 + n / 2 ≤ n` follows from |
| 16 | +-- `n = 2 * (n / 2) + n % 2` and `0 ≤ n % 2`. |
| 17 | +example : ∀ n : ℕ, n / 2 + n / 2 ≤ n := by sos |
| 18 | + |
| 19 | +-- Trivial ℕ mod upper bound: `n % 3 ≤ 2` follows from `n % 3 + 1 ≤ 3`. |
| 20 | +example : ∀ n : ℕ, n % 3 ≤ 2 := by sos |
| 21 | + |
| 22 | +-- ℕ div+mod identity: `2 * (n / 2) + n % 2 = n` is the witness itself. |
| 23 | +example : ∀ n : ℕ, 2 * (n / 2) + n % 2 = n := by sos |
| 24 | + |
| 25 | +-- ℤ remainder nonneg under ediv (the default `/` on ℤ). |
| 26 | +example : ∀ n : ℤ, 0 ≤ n % 3 := by sos |
| 27 | + |
| 28 | +-- ℤ remainder bound: `n % 5 ≤ 4`. |
| 29 | +example : ∀ n : ℤ, n % 5 ≤ 4 := by sos |
| 30 | + |
| 31 | +-- ℤ div+mod identity with sign-invariant statement. |
| 32 | +example : ∀ n : ℤ, 2 * (n / 2) + n % 2 = n := by sos |
| 33 | + |
| 34 | +-- `n / 2 ≤ n` over ℕ (the witness `n = 2*(n/2) + n%2` and `0 ≤ n%2` |
| 35 | +-- give `n/2 ≤ n/2 + (n/2 + n%2) = n`). |
| 36 | +example : ∀ n : ℕ, n / 2 ≤ n := by sos |
| 37 | + |
| 38 | +-- Tight: `3 * (n / 3) ≤ n`. |
| 39 | +example : ∀ n : ℕ, 3 * (n / 3) ≤ n := by sos |
| 40 | + |
| 41 | +-- ℤ goal with a non-negativity precondition. |
| 42 | +example : ∀ n : ℤ, 0 ≤ n → 2 * (n / 2) ≤ n := by sos |
| 43 | + |
| 44 | +-- Larger divisor literal: `n / 7 + n / 7 ≤ n` (the search treats |
| 45 | +-- `n/7` as an atom `q`; from `n = 7q + r` and `0 ≤ r` it gets |
| 46 | +-- `2q ≤ 2q + 5q + r = n` requiring `5q ≥ 0`, which follows from |
| 47 | +-- `0 ≤ q` introduced by `assertNatCastNonneg`). |
| 48 | +example : ∀ n : ℕ, n / 7 + n / 7 ≤ n := by sos |
| 49 | + |
| 50 | +-- Two distinct sites (different divisor literals) on the same `n`: |
| 51 | +-- both `n / 2` and `n / 3` need witnesses, with non-shadowing names. |
| 52 | +example : ∀ n : ℕ, 2 * (n / 2) ≤ n ∧ 3 * (n / 3) ≤ n → True := by |
| 53 | + intro _ _; trivial |
| 54 | + |
| 55 | +-- Both divisor literals as distinct atoms in the conclusion. |
| 56 | +example : ∀ n : ℕ, n / 2 + n / 3 ≤ n + n := by sos |
| 57 | + |
| 58 | +-- DIV/MOD in a `0 ≤ …`-shape hypothesis is enriched too (the lift |
| 59 | +-- scans hypothesis types in addition to the conclusion). Trivial |
| 60 | +-- consequence of `0 ≤ n / 2` plus the witness `n = 2 * (n/2) + n%2`. |
| 61 | +example : ∀ n : ℕ, 0 ≤ n / 2 → 0 ≤ n / 2 + n / 2 + n / 2 := by sos |
| 62 | + |
| 63 | +-- Equality conclusion `liftToReal` splits via `le_antisymm` and |
| 64 | +-- recurses on each ≤-subgoal; the second entry into `enrichDivMod` |
| 65 | +-- must NOT re-enrich the same site by rediscovering its own |
| 66 | +-- previously-introduced witness hypotheses. |
| 67 | +example : ∀ n : ℕ, n % 2 + 2 * (n / 2) = n := by sos |
| 68 | + |
| 69 | +-- Non-literal divisor with no positivity hypothesis in scope: the |
| 70 | +-- unconditional witnesses (`n · (m/n) + m%n = m` and `m%n ≥ 0`) are |
| 71 | +-- still introduced, but the strict bound `m%n < n` is skipped because |
| 72 | +-- `omega` can't prove `0 < n`. The goal `m / n ≤ m` is false at the |
| 73 | +-- real point `n := 0, m := 0, m/n := 1, m%n := 0` (consistent with |
| 74 | +-- the unconditional witnesses), so the search correctly fails. |
| 75 | +example : True := by |
| 76 | + fail_if_success |
| 77 | + (have : ∀ m n : ℕ, m / n ≤ m := by sos) |
| 78 | + trivial |
| 79 | + |
| 80 | +/-! ### Non-literal divisor enrichment (issue #45) |
| 81 | +
|
| 82 | +When the divisor is not a positive literal, `enrichDivMod` introduces |
| 83 | +the unconditional div/mod identity and remainder ≥ 0 witnesses, and |
| 84 | +routes the strict bound `r < n` through `omega` on the divisor |
| 85 | +positivity (over the source domain). Sites whose positivity is |
| 86 | +derivable from the local context — a `n ≠ 0` / `0 < n` / `m < n` |
| 87 | +hypothesis — get the full witness suite; sites whose positivity isn't |
| 88 | +provable get only the unconditional facts. The omega-derived `0 < n` |
| 89 | +is local to the `by` block: it's used to discharge `Nat.mod_lt` / |
| 90 | +`Int.emod_lt_of_pos`, not added as a separate ℝ-cast hypothesis. |
| 91 | +
|
| 92 | +Harrison's `sos.ml:1729` lands directly on the unconditional ℕ path |
| 93 | +(no positivity hypothesis needed). The remaining `:1726`, `:1727`, |
| 94 | +`:1730`, `:1731` examples enrich correctly but their natural |
| 95 | +certificates require products of inequality constraints (e.g. |
| 96 | +`n · (m/n) ≥ 0` derived from `n ≥ 0 ∧ m/n ≥ 0`), which is a |
| 97 | +Schmüdgen-preordering certificate rather than a Putinar one — out of |
| 98 | +scope until #38 lands. See the FIXME blocks below for the per-case |
| 99 | +diagnoses. -/ |
| 100 | + |
| 101 | +-- sos.ml:1729 — `n · (m / n) ≤ m`. Holds unconditionally over ℕ: |
| 102 | +-- `n · (m/n) = m - m%n ≤ m`. The unconditional witnesses (div/mod |
| 103 | +-- identity and `0 ≤ m%n`) give a direct Putinar cert. |
| 104 | +example : ∀ m n : ℕ, n * (m / n) ≤ m := by sos |
| 105 | + |
| 106 | +-- ℤ companion: with `0 < n` in scope, `omega` discharges the |
| 107 | +-- divisor-positivity sides of `Int.emod_nonneg` / `Int.emod_lt_of_pos` |
| 108 | +-- and the same cert closes the goal. |
| 109 | +example : ∀ m n : ℤ, 0 < n → n * (m / n) ≤ m := by sos |
| 110 | + |
| 111 | +-- Focused tests for the optional positivity-guarded witnesses. |
| 112 | +-- Each one directly exercises the `omega`-derived bound that |
| 113 | +-- `enrichSite` adds for non-literal divisors and would silently |
| 114 | +-- regress if the soft-failed witness intros stopped firing. |
| 115 | + |
| 116 | +-- ℕ strict bound from `n ≠ 0`: the witness `0 ≤ n - (m%n) - 1` is |
| 117 | +-- precisely what's needed (the rest is `Nat.cast_lt` on the |
| 118 | +-- conclusion). |
| 119 | +example : ∀ m n : ℕ, n ≠ 0 → m % n < n := by sos |
| 120 | + |
| 121 | +-- ℤ remainder ≥ 0 from `n ≠ 0`: directly the `hnn` witness. |
| 122 | +example : ∀ m n : ℤ, n ≠ 0 → 0 ≤ m % n := by sos |
| 123 | + |
| 124 | +-- ℤ strict bound from `0 < n`: directly the `hgap` witness. |
| 125 | +example : ∀ m n : ℤ, 0 < n → m % n < n := by sos |
| 126 | + |
| 127 | +-- FIXME sos.ml:1726 — `n ≠ 0 ⇒ 0 % n = 0`. With the strict bound |
| 128 | +-- `n - (0%n) - 1 ≥ 0` in scope the cert needs `n · (0/n) ≥ 0`, a |
| 129 | +-- product of two non-negative atoms, which Putinar can't form |
| 130 | +-- without Schmüdgen preordering (#38). |
| 131 | +-- example : ∀ n : ℕ, n ≠ 0 → 0 % n = 0 := by sos |
| 132 | + |
| 133 | +-- FIXME sos.ml:1730 — `n ≠ 0 ⇒ 0 / n = 0`. Same preordering |
| 134 | +-- obstruction as 1726. |
| 135 | +-- example : ∀ n : ℕ, n ≠ 0 → 0 / n = 0 := by sos |
| 136 | + |
| 137 | +-- FIXME sos.ml:1727 — `m < n ⇒ m / n = 0`. Refute path turns it |
| 138 | +-- into `m/n ≥ 1 ∧ m + 1 ≤ n ⇒ False`, which needs the multiplicative |
| 139 | +-- step `n · (m/n) ≥ n` (i.e. constraint product `n · (m/n - 1) ≥ 0`). |
| 140 | +-- example : ∀ m n : ℕ, m < n → m / n = 0 := by sos |
| 141 | + |
| 142 | +-- FIXME sos.ml:1731 — `p ≠ 0 ∧ m ≤ n ⇒ m / p ≤ n / p`. Two DIV |
| 143 | +-- sites with the same non-literal divisor `p`; both get the full |
| 144 | +-- witness suite from `omega`. The natural refutation chains |
| 145 | +-- `p · (m/p - n/p - 1) ≥ p` against `m - n ≤ 0`, again a Schmüdgen |
| 146 | +-- product. |
| 147 | +-- example : ∀ m n p : ℕ, p ≠ 0 → m ≤ n → m / p ≤ n / p := by sos |
| 148 | + |
| 149 | +/-! ### Refute + equality cofactor — CSDP numerical degeneracy (issue #54) |
| 150 | +
|
| 151 | +The three goals below all admit short Schmüdgen-style refutation |
| 152 | +certificates with constant cofactors (computed by hand for each): |
| 153 | +
|
| 154 | + * `(a*b)/b = a` (`b ≠ 0`): split by `le_antisymm` into two ≤-goals, |
| 155 | + each closes by refute against the witness `a·b = b·q + r` plus a |
| 156 | + single Schmüdgen product `b·(q − a − 1) ≥ 0` (one direction) or |
| 157 | + `b·(a − q − 1) ≥ 0` (the other). Cardinality 2. |
| 158 | + * `n/2 + (n+1)/2 = n`: pure Putinar from `2·(q₁+q₂ - n - 1) + r₁ |
| 159 | + + r₂ - p_1 - p_2 = -1`. |
| 160 | + * `a/c + b/c ≤ (a+b)/c` (`c ≠ 0`): refute closes via Schmüdgen |
| 161 | + `c·(q_a + q_b - q_{ab} - 1) ≥ 0` against `a + b = c·q_{ab} + |
| 162 | + r_{ab}`, sum of the per-summand equalities. |
| 163 | +
|
| 164 | +All three certificates verify exactly under `Certificate.checks` |
| 165 | +(`decide +kernel` on the polynomial identity). The blocker is at the |
| 166 | +CSDP solve step, not at the certificate verifier or the cert search |
| 167 | +space: when the goal goes through the refute / infeasibility arm |
| 168 | +(target = −1, useTraceCost = false), the LP-encoded equality cofactor |
| 169 | +block (`λ = x⁺ − x⁻` with `x⁺, x⁻ ≥ 0` and zero cost) leaves CSDP's |
| 170 | +central path on the boundary of primal feasibility. CSDP returns |
| 171 | +non-success codes (1/5/7) at the natural relaxation depth and only |
| 172 | +much later — at extraDeg ≥ 1, cardinality ≥ 6 — produces a |
| 173 | +numerically feasible solution, by which point the SDP has dozens of |
| 174 | +extra σ blocks whose Gram matrices don't round to the natural cert. |
| 175 | +
|
| 176 | +The closed-positivity path uses `useTraceCost = true`, which gives |
| 177 | +CSDP a well-defined central path; the LP cofactor block then behaves |
| 178 | +fine. So the existing `n = 2·(n/2) + n%2` showcase test (which is |
| 179 | +also an equality goal but doesn't need refute on either ≤-half) |
| 180 | +closes cleanly, and the obstruction is specific to refute-arm goals |
| 181 | +whose certificate genuinely needs the integer-discreteness step. |
| 182 | +
|
| 183 | +Harrison's HOL Light `sos.ml` avoids this problem by eliminating |
| 184 | +ideal cofactor variables before the SDP solve: |
| 185 | +
|
| 186 | + * `SOS_RULE` rewrites `NUM` goals to `INT` (`NUM_TO_INT_CONV`), then |
| 187 | + `INT_SOS` refutes the negation and calls `REAL_SOS`. |
| 188 | + * `REAL_SOS` runs `GEN_REAL_ARITH REAL_NONLINEAR_SUBST_PROVER`, |
| 189 | + which repeatedly substitutes any equation with a substitutable |
| 190 | + real variable into the rest of the system before the SDP solve |
| 191 | + (`Examples/sos.ml:1229-1252`). |
| 192 | + * The underlying Positivstellensatz at `Examples/sos.ml:1054` also |
| 193 | + runs `eliminate_all_equations` on the coefficient equations |
| 194 | + *symbolically* before building the CSDP problem; `mk_matrix` |
| 195 | + skips negative-tag blocks (the ideal cofactors) at |
| 196 | + `Examples/sos.ml:1058-1062`, and the CSDP objective is only ever |
| 197 | + populated on the surviving positive SDP block diagonals |
| 198 | + (`Examples/sos.ml:1063-1069`). |
| 199 | +
|
| 200 | +So Harrison's effective encoding is `a = b·q + r, 0 ≤ r, r ≤ b − 1`, |
| 201 | +but the equality is used to substitute one variable away (typically |
| 202 | +`r := a − b·q` for div/mod sites), leaving a pure quadratic-module |
| 203 | +problem with no LP cofactor null direction. For our case B, after the |
| 204 | +substitution `r := a·b − b·q`, the Schmüdgen-2 cert |
| 205 | +`-1 = 2·(a·b − b·q) + (b − (a·b − b·q) − 1) + b·(q − a − 1)` lands |
| 206 | +directly without ever instantiating an LP block. |
| 207 | +
|
| 208 | +The fix is to add an equality-elimination pre-pass to the search: |
| 209 | +identify equalities of the form `var = poly_without_var` in `ps`, |
| 210 | +substitute `var` out of every other constraint and the target, drop |
| 211 | +the equality from `ps`. This mirrors `REAL_NONLINEAR_SUBST_PROVER`. |
| 212 | +Surgical at the search level: drops `ps`-driven LP blocks, leaves the |
| 213 | +certificate-verifier API unchanged because the eliminated variable |
| 214 | +becomes part of the polynomial expression in the cert. A smaller |
| 215 | +short-term mitigation (`-ε` cost on the LP split block) bounds the |
| 216 | +null direction numerically; testing showed CSDP still returns return |
| 217 | +codes 1/5 on these specific problems, so a numerical regulariser is |
| 218 | +not by itself sufficient — the symbolic elimination is the right |
| 219 | +solution. |
| 220 | +
|
| 221 | +-/ |
| 222 | + |
| 223 | +/-! ### Shared DIV/MOD quotient and remainder atoms (issue #67) -/ |
| 224 | + |
| 225 | +open Lean Meta Elab Tactic in |
| 226 | +private partial def containsRawNatDivMod (e : Expr) : MetaM Bool := do |
| 227 | + match_expr e with |
| 228 | + | Nat.div _ _ => return true |
| 229 | + | Nat.mod _ _ => return true |
| 230 | + | _ => |
| 231 | + match e with |
| 232 | + | .app f a => return (← containsRawNatDivMod f) || (← containsRawNatDivMod a) |
| 233 | + | .lam _ t b _ | .forallE _ t b _ => |
| 234 | + return (← containsRawNatDivMod t) || (← containsRawNatDivMod b) |
| 235 | + | .mdata _ b => containsRawNatDivMod b |
| 236 | + | _ => return false |
| 237 | + |
| 238 | +set_option linter.unusedTactic false in |
| 239 | +example : ∀ a b : ℕ, b ≠ 0 → (a * b) / b ≤ a := by |
| 240 | + intro a b hb |
| 241 | + run_tac do |
| 242 | + let st ← Lean.Elab.Tactic.saveState |
| 243 | + SOS.Lift.refuteToReal |
| 244 | + let some parsed ← SOS.Reify.parseGoalAtomic | |
| 245 | + throwError "issue #67 regression: refuted DIV/MOD goal did not reify" |
| 246 | + unless parsed.atoms.size == 4 do |
| 247 | + throwError "issue #67 regression: expected atoms a/b/q/r, got {parsed.atoms.size}" |
| 248 | + for atom in parsed.atoms do |
| 249 | + if ← containsRawNatDivMod atom then |
| 250 | + throwError "issue #67 regression: raw Nat.div/Nat.mod leaked into atom {atom}" |
| 251 | + st.restore |
| 252 | + have hpos : 0 < b := Nat.pos_of_ne_zero hb |
| 253 | + rw [Nat.mul_div_left _ hpos] |
| 254 | + |
| 255 | +example : ∀ a b : ℕ, b ≠ 0 → (a * b) / b = a := by |
| 256 | + sos (config := { maxDepth := 0, maxSubsetCardinality := 2 }) |
| 257 | + |
| 258 | +example : ∀ n : ℕ, n / 2 + (n + 1) / 2 = n := by |
| 259 | + sos (config := { maxDepth := 0, maxSubsetCardinality := 2 }) |
| 260 | + |
| 261 | +example : ∀ a b c : ℕ, c ≠ 0 → a / c + b / c ≤ (a + b) / c := by |
| 262 | + sos (config := { maxDepth := 0, maxSubsetCardinality := 2 }) |
0 commit comments