From 389537cf0e8bfa37b0123a2d9ff00a88391eb98b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 18 Mar 2025 16:04:06 -0700
Subject: [PATCH] fix: consistent term order in linear integer normalization
 (#7560)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR ensures that we use the same ordering to normalize linear `Int`
terms and relations. This change affects `simp +arith` and `grind`
normalizer.

This consistency is important in the cutsat procedure. We want to avoid
a situation where the cutsat state contains both "atoms":
- `「(NatCast.natCast x + NatCast.natCast y) % 8」`
- `「(NatCast.natCast y + NatCast.natCast x) % 8」`

This was happening because we were using different orderings for
(nested) terms and relations (`=`, `<=`).
---
 src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean |  2 +-
 tests/lean/run/grind_cutsat_nat_dvd.lean       | 12 ++++++++++++
 2 files changed, 13 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
index fbedf9f46a..fa30307cec 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
@@ -211,7 +211,7 @@ def toLinearExpr (e : Expr) : MetaM (Int.Linear.Expr × Array Expr) := do
   if atoms.size == 1 then
     return (e, atoms)
   else
-    let (atoms, perm) := sortExprs atoms
+    let (atoms, perm) := sortExprs atoms (lt := false)
     let e := e.applyPerm perm
     return (e, atoms)
 
diff --git a/tests/lean/run/grind_cutsat_nat_dvd.lean b/tests/lean/run/grind_cutsat_nat_dvd.lean
index 2d85e95f4b..f9741ed9ea 100644
--- a/tests/lean/run/grind_cutsat_nat_dvd.lean
+++ b/tests/lean/run/grind_cutsat_nat_dvd.lean
@@ -30,3 +30,15 @@ example (x y : Nat) :
 
 example (i : Nat) : i < 330 → 7 ∣ (660 + i) * (1319 - i) → 1319 - i < 1979 := by
   grind
+
+example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
+    4 ≤ (x + y) % 8 ∧ (x + y) % 8 ≤ 6 := by
+  grind
+
+example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
+    4 ≤ (y + x) % 8 ∧ (x + y) % 8 ≤ 6 := by
+  grind
+
+example (x y : Nat) (_ : 2 ≤ x) (_ : x ≤ 3) (_ : 2 ≤ y) (_ : y ≤ 3) :
+    4 ≤ (y + x) % 8 ∧ (y + x) % 8 ≤ 6 := by
+  grind