Google Git Google Git
Sign in
fuchsia/third_party/github.com/leanprover/lean4/refs/heads/upstream/comm_solver_kernel^!/.
commit
1fc654b3d710fa8426e29dbbba80708020eee701
[log]
author
Leonardo de Moura <leomoura@amazon.com>
Mon Oct 26 02:24:09 2026 +0000
committer
Leonardo de Moura <leomoura@amazon.com>
Mon Oct 26 02:24:09 2026 +0000
tree
1d7ee1590bac8651efb3f31ff22821daad1e115f
parent
e05cacba3c67fc9a5daba88c6ede4d6a3c619192 [diff] 
perf: encode `grind` ring certificate numerals as constructor applications

This PR makes the `ToExpr` instances for the polynomials, monomials, and expressions of `Lean.Grind.CommRing` encode numerals as `Int.ofNat n`, `Int.negSucc n`, and raw `Nat` literals, so that the kernel no longer unfolds `OfNat.ofNat` and `Neg.neg` when it evaluates the certificates of the `grind` ring solver and of the `Sym.simp` arithmetic normalizer. Proof terms printed by `grind.debug.proof` now show these constructor applications.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

diff --git a/src/Lean/Meta/Sym/Arith/ToExpr.lean b/src/Lean/Meta/Sym/Arith/ToExpr.lean
index 2467634..1b58e6a 100644
--- a/src/Lean/Meta/Sym/Arith/ToExpr.lean
+++ b/src/Lean/Meta/Sym/Arith/ToExpr.lean

@@ -11,11 +11,19 @@
 namespace Lean.Meta.Sym.Arith
 open Grind.CommRing
 /-!
-`ToExpr` instances for `CommRing.Poly` types.
+`ToExpr` instances for `CommRing.Poly` types. Numerals are constructor applications on raw
+literals (`Int.ofNat n`, `Int.negSucc n`, and raw `Nat` literals), which the kernel evaluates
+without unfolding `OfNat.ofNat` and `Neg.neg` when it checks certificates.
 -/
 
+/-- `k` as `Int.ofNat n` or `Int.negSucc n` on a raw literal. -/
+def mkIntLitK (k : Int) : Expr :=
+  match k with
+  | .ofNat n => mkApp (mkConst ``Int.ofNat) (mkRawNatLit n)
+  | .negSucc n => mkApp (mkConst ``Int.negSucc) (mkRawNatLit n)
+
 def ofPower (p : Power) : Expr :=
-  mkApp2 (mkConst ``Power.mk) (toExpr p.x) (toExpr p.k)
+  mkApp2 (mkConst ``Power.mk) (mkRawNatLit p.x) (mkRawNatLit p.k)
 
 instance : ToExpr Power where
   toExpr := ofPower
@@ -32,8 +40,8 @@
 
 def ofPoly (p : Poly) : Expr :=
   match p with
-  | .num k => mkApp (mkConst ``Poly.num) (toExpr k)
-  | .add k m p => mkApp3 (mkConst ``Poly.add) (toExpr k) (toExpr m) (ofPoly p)
+  | .num k => mkApp (mkConst ``Poly.num) (mkIntLitK k)
+  | .add k m p => mkApp3 (mkConst ``Poly.add) (mkIntLitK k) (toExpr m) (ofPoly p)
 
 instance : ToExpr Poly where
   toExpr := ofPoly
@@ -43,15 +51,15 @@
 
 def ofRingExpr (e : CommRing.Expr) : Expr :=
   match e with
-  | .num k => mkApp (mkConst ``CommRing.Expr.num) (toExpr k)
-  | .intCast k => mkApp (mkConst ``CommRing.Expr.intCast) (toExpr k)
-  | .natCast k => mkApp (mkConst ``CommRing.Expr.natCast) (toExpr k)
-  | .var x => mkApp (mkConst ``CommRing.Expr.var) (toExpr x)
+  | .num k => mkApp (mkConst ``CommRing.Expr.num) (mkIntLitK k)
+  | .intCast k => mkApp (mkConst ``CommRing.Expr.intCast) (mkIntLitK k)
+  | .natCast k => mkApp (mkConst ``CommRing.Expr.natCast) (mkRawNatLit k)
+  | .var x => mkApp (mkConst ``CommRing.Expr.var) (mkRawNatLit x)
   | .add a b => mkApp2 (mkConst ``CommRing.Expr.add) (ofRingExpr a) (ofRingExpr b)
   | .mul a b => mkApp2 (mkConst ``CommRing.Expr.mul) (ofRingExpr a) (ofRingExpr b)
   | .sub a b => mkApp2 (mkConst ``CommRing.Expr.sub) (ofRingExpr a) (ofRingExpr b)
   | .neg a => mkApp (mkConst ``CommRing.Expr.neg) (ofRingExpr a)
-  | .pow a k => mkApp2 (mkConst ``CommRing.Expr.pow) (ofRingExpr a) (toExpr k)
+  | .pow a k => mkApp2 (mkConst ``CommRing.Expr.pow) (ofRingExpr a) (mkRawNatLit k)
 
 instance : ToExpr CommRing.Expr where
   toExpr := ofRingExpr

diff --git a/tests/elab/grind_guide_2.lean.out.expected b/tests/elab/grind_guide_2.lean.out.expected
index 9fbefca..f4cee41 100644
--- a/tests/elab/grind_guide_2.lean.out.expected
+++ b/tests/elab/grind_guide_2.lean.out.expected

@@ -10,12 +10,16 @@
         let e_2 := Expr.zero;
         let e_3 := (Expr.intMul (-1) (Expr.var 1)).add (Expr.intMul 1 (Expr.var 0));
         let rctx := RArray.leaf (f 2);
-        let rp_1 := CommRing.Poly.add 1 (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 0);
+        let rp_1 :=
+          CommRing.Poly.add (Int.ofNat 1) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit)
+            (CommRing.Poly.num (Int.ofNat 0));
         let rp_2 :=
-          CommRing.Poly.add (-1) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 1);
+          CommRing.Poly.add (Int.negSucc 0) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit)
+            (CommRing.Poly.num (Int.ofNat 1));
         let re_1 := CommRing.Expr.var 0;
-        let re_2 := CommRing.Expr.num 0;
-        let re_3 := ((CommRing.Expr.num 1).neg.mul (CommRing.Expr.var 0)).add (CommRing.Expr.num 1);
+        let re_2 := CommRing.Expr.num (Int.ofNat 0);
+        let re_3 :=
+          ((CommRing.Expr.num (Int.ofNat 1)).neg.mul (CommRing.Expr.var 0)).add (CommRing.Expr.num (Int.ofNat 1));
         lt_unsat ctx
           (le_lt_combine ctx p_3 p_5 p_1 (eagerReduce (Eq.refl true))
             (le_le_combine ctx p_4 p_2 p_3 (eagerReduce (Eq.refl true))

diff --git a/tests/elab/grind_linarith_2.lean b/tests/elab/grind_linarith_2.lean
index c48799b..e2dc134 100644
--- a/tests/elab/grind_linarith_2.lean
+++ b/tests/elab/grind_linarith_2.lean

@@ -14,7 +14,7 @@
         let e_1 := Expr.zero;
         let e_2 := Expr.intMul 0 (Expr.var 0);
         let rctx := RArray.branch 1 (RArray.leaf a) (RArray.leaf b);
-        let rp_1 := CommRing.Poly.num 0;
+        let rp_1 := CommRing.Poly.num (Int.ofNat 0);
         let re_1 := (CommRing.Expr.var 0).add (CommRing.Expr.var 1);
         let re_2 := (CommRing.Expr.var 1).add (CommRing.Expr.var 0);
         diseq_unsat ctx

diff --git a/tests/elab/grind_linarith_trim_context.lean b/tests/elab/grind_linarith_trim_context.lean
index fdbeaf0..c969a0f 100644
--- a/tests/elab/grind_linarith_trim_context.lean
+++ b/tests/elab/grind_linarith_trim_context.lean

@@ -12,12 +12,16 @@
         let e_2 := Expr.zero;
         let e_3 := (Expr.intMul (-1) (Expr.var 1)).add (Expr.intMul 1 (Expr.var 0));
         let rctx := RArray.leaf (f 2);
-        let rp_1 := CommRing.Poly.add 1 (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 0);
+        let rp_1 :=
+          CommRing.Poly.add (Int.ofNat 1) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit)
+            (CommRing.Poly.num (Int.ofNat 0));
         let rp_2 :=
-          CommRing.Poly.add (-1) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit) (CommRing.Poly.num 1);
+          CommRing.Poly.add (Int.negSucc 0) (CommRing.Mon.mult { x := 0, k := 1 } CommRing.Mon.unit)
+            (CommRing.Poly.num (Int.ofNat 1));
         let re_1 := CommRing.Expr.var 0;
-        let re_2 := CommRing.Expr.num 0;
-        let re_3 := ((CommRing.Expr.num 1).neg.mul (CommRing.Expr.var 0)).add (CommRing.Expr.num 1);
+        let re_2 := CommRing.Expr.num (Int.ofNat 0);
+        let re_3 :=
+          ((CommRing.Expr.num (Int.ofNat 1)).neg.mul (CommRing.Expr.var 0)).add (CommRing.Expr.num (Int.ofNat 1));
         lt_unsat ctx
           (le_lt_combine ctx p_3 p_5 p_1 (eagerReduce (Eq.refl true))
             (le_le_combine ctx p_4 p_2 p_3 (eagerReduce (Eq.refl true))

diff --git a/tests/elab/grind_ring_trim_context.lean b/tests/elab/grind_ring_trim_context.lean
index 7316771..48cccb5 100644
--- a/tests/elab/grind_ring_trim_context.lean
+++ b/tests/elab/grind_ring_trim_context.lean

@@ -5,16 +5,18 @@
         id
           (let ctx := RArray.branch 1 (RArray.leaf x) (RArray.leaf x⁻¹);
           let e_1 := (Expr.var 0).mul (Expr.var 1);
-          let e_2 := Expr.num 0;
-          let e_3 := Expr.num 1;
+          let e_2 := Expr.num (Int.ofNat 0);
+          let e_3 := Expr.num (Int.ofNat 1);
           let e_4 := (Expr.var 0).pow 2;
           let m_1 := Mon.mult (Power.mk 1 1) Mon.unit;
           let m_2 := Mon.mult (Power.mk 0 1) Mon.unit;
-          let p_1 := Poly.num (-1);
-          let p_2 := Poly.add (-1) (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num 0);
-          let p_3 := Poly.add 1 (Mon.mult (Power.mk 0 2) Mon.unit) (Poly.num 0);
-          let p_4 := Poly.add 1 (Mon.mult (Power.mk 0 1) (Mon.mult (Power.mk 1 1) Mon.unit)) (Poly.num (-1));
-          let p_5 := Poly.add 1 (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num 0);
+          let p_1 := Poly.num (Int.negSucc 0);
+          let p_2 := Poly.add (Int.negSucc 0) (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num (Int.ofNat 0));
+          let p_3 := Poly.add (Int.ofNat 1) (Mon.mult (Power.mk 0 2) Mon.unit) (Poly.num (Int.ofNat 0));
+          let p_4 :=
+            Poly.add (Int.ofNat 1) (Mon.mult (Power.mk 0 1) (Mon.mult (Power.mk 1 1) Mon.unit))
+              (Poly.num (Int.negSucc 0));
+          let p_5 := Poly.add (Int.ofNat 1) (Mon.mult (Power.mk 0 1) Mon.unit) (Poly.num (Int.ofNat 0));
           one_eq_zero_unsat ctx p_1 (eagerReduce (Eq.refl true))
             (Stepwise.simp ctx 1 p_4 (-1) m_1 p_5 p_1 (eagerReduce (Eq.refl true))
               (Stepwise.core ctx e_1 e_3 p_4 (eagerReduce (Eq.refl true)) (diseq0_to_eq x h_4))

diff --git a/tests/elab/grind_semiring_norm.lean b/tests/elab/grind_semiring_norm.lean
index ee475a2..026345d 100644
--- a/tests/elab/grind_semiring_norm.lean
+++ b/tests/elab/grind_semiring_norm.lean

@@ -19,7 +19,7 @@
           (CommRing.eq_normS (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
             (((CommRing.Expr.var 0).add (CommRing.Expr.var 1)).pow 2)
             ((((CommRing.Expr.var 0).pow 2).add
-                  (((CommRing.Expr.num 2).mul (CommRing.Expr.var 0)).mul (CommRing.Expr.var 1))).add
+                  (((CommRing.Expr.num (Int.ofNat 2)).mul (CommRing.Expr.var 0)).mul (CommRing.Expr.var 1))).add
               ((CommRing.Expr.var 1).pow 2))
             (eagerReduce (Eq.refl true))))
 -/