From 16a3d2477d4a84e2e3a1ff3f7c9229e20dc9600f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 18:55:35 -0800
Subject: [PATCH 01/10] fix: typo

---
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
index d0c91ed8186f..cce8defcb099 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
@@ -125,7 +125,7 @@ def EqCnstr.pp (c : EqCnstr) : GoalM MessageData := do
 def EqCnstr.denoteExpr (c : EqCnstr) : GoalM Expr := do
   return mkIntEq (← c.p.denoteExpr') (mkIntLit 0)
 
-def EqCnstr.throwUnexpected (c : LeCnstr) : GoalM α := do
+def EqCnstr.throwUnexpected (c : EqCnstr) : GoalM α := do
   throwError "`grind` internal error, unexpected{indentD (← c.pp)}"
 
 /-- Returns occurrences of `x`. -/

From f9621c5b207cc98c615382fcd7ed6f7f72f5ef0c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 18:55:54 -0800
Subject: [PATCH 02/10] feat: pick variable to eliminate

---
 .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean    | 35 ++++++++++++++++---
 1 file changed, 31 insertions(+), 4 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index f5e7f892d07c..755358a9dc85 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -10,6 +10,29 @@ namespace Lean.Meta.Grind.Arith.Cutsat
 def mkEqCnstr (p : Poly) (h : EqCnstrProof) : GoalM EqCnstr := do
   return { p, h, id := (← mkCnstrId) }
 
+def _root_.Int.Linear.Poly.pickVarToElim? (p : Poly) : Option (Int × Var) :=
+  match p with
+  | .num _ => none
+  | .add k x p => go k x p
+where
+  go (k : Int) (x : Var) (p : Poly) : Int × Var :=
+    if k == 1 || k == -1 then
+      (k, x)
+    else match p with
+      | .num _ => (k, x)
+      | .add k' x' p =>
+        if k'.natAbs < k.natAbs then
+          go k' x' p
+        else
+          go k x p
+
+def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
+  if (← isInconsistent) then return ()
+  trace[grind.cutsat.eq] "{← c.pp}"
+  let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
+  if k.natAbs != 1 then
+
+
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
   trace[grind.cutsat.eq] "{mkIntEq a b}"
@@ -17,10 +40,14 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
   return ()
 
 @[export lean_process_new_cutsat_lit]
-def processNewEqLitImpl (a k : Expr) : GoalM Unit := do
-  trace[grind.cutsat.eq] "{mkIntEq a k}"
-  -- TODO
-  return ()
+def processNewEqLitImpl (a ke : Expr) : GoalM Unit := do
+  let some k ← getIntValue? ke | return ()
+  let some p := (← get').terms.find? { expr := a } | return ()
+  if k == 0 then
+    (← mkEqCnstr p (.expr (← mkEqProof a ke))).assert
+  else
+    -- TODO
+    return ()
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where

From ddb02b811400eb40ce24fbd16ea898960dd85f98 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 18:56:29 -0800
Subject: [PATCH 03/10] feat: use absolute value

---
 src/Init/Data/Int/Linear.lean | 22 +++++++++++++++++-----
 1 file changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 9ffec932bac7..ab9ad55a6b64 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -864,17 +864,28 @@ private theorem dvd_of_eq' {a x p : Int} : a*x + p = 0 → a ∣ p := by
   rw [Int.mul_comm, ← Int.neg_mul, Eq.comm, Int.mul_comm] at h
   exact ⟨-x, h⟩
 
+private def abs (x : Int) : Int :=
+  Int.ofNat x.natAbs
+
+private theorem abs_dvd {a p : Int} (h : a ∣ p) : abs a ∣ p := by
+  cases a <;> simp [abs]
+  · simp at h; assumption
+  · simp [Int.negSucc_eq] at h; assumption
+
 def dvd_of_eq_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) : Bool :=
-  d₂ == p₁.coeff x && p₂ == p₁.insert (-d₂) x
+  let a := p₁.coeff x
+  d₂ == abs a && p₂ == p₁.insert (-a) x
 
 theorem dvd_of_eq (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly)
     : dvd_of_eq_cert x p₁ d₂ p₂ → p₁.denote' ctx = 0 → d₂ ∣ p₂.denote' ctx := by
   simp [dvd_of_eq_cert]
   intro h₁ h₂
   have h := eq_add_coeff_insert ctx p₁ x
-  rw [← h₁, ← h₂] at h
-  rw [h]
-  apply dvd_of_eq'
+  rw [← h₂] at h
+  rw [h, h₁]
+  intro h₃
+  apply abs_dvd
+  apply dvd_of_eq' h₃
 
 private theorem eq_dvd_subst' {a x p d b q : Int} : a*x + p = 0 → d ∣ b*x + q → a*d ∣ a*q - b*p := by
   intro h₁ ⟨z, h₂⟩
@@ -892,7 +903,7 @@ def eq_dvd_subst_cert (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ :
   let b := p₂.coeff x
   let p := p₁.insert (-a) x
   let q := p₂.insert (-b) x
-  d₃ == a * d₂ &&
+  d₃ == abs (a * d₂) &&
   p₃ == (q.mul a |>.combine (p.mul (-b)))
 
 theorem eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂ : Poly) (d₃ : Int) (p₃ : Poly)
@@ -913,6 +924,7 @@ theorem eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂
   rw [Int.add_comm] at h₁ h₂
   have := eq_dvd_subst' h₁ h₂
   rw [Int.sub_eq_add_neg, Int.add_comm] at this
+  apply abs_dvd
   simp [this]
 
 private theorem eq_eq_subst' {a x p b q : Int} : a*x + p = 0 → b*x + q = 0 → b*p - a*q = 0 := by

From 20141644b4a8dca748221f91f3e2eac589284389 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 19:22:52 -0800
Subject: [PATCH 04/10] feat: add divisibility constraint for equality

---
 .../Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean  | 14 +++++++++++++-
 .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean    | 16 +++++++++++++---
 .../Meta/Tactic/Grind/Arith/Cutsat/Types.lean    |  8 ++++----
 .../Meta/Tactic/Grind/Arith/Cutsat/Util.lean     |  8 +++-----
 4 files changed, 33 insertions(+), 13 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 755358a9dc85..011328ee32f8 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 def mkEqCnstr (p : Poly) (h : EqCnstrProof) : GoalM EqCnstr := do
@@ -28,10 +29,21 @@ where
 
 def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
   if (← isInconsistent) then return ()
+  -- TODO: apply substitutions
   trace[grind.cutsat.eq] "{← c.pp}"
   let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
+  -- TODO: eliminate `x` from lowers, uppers, and dvdCnstrs
+  -- TODO: reset `x`s occurrences
+  -- assert a divisibility constraint IF `|k| != 1`
   if k.natAbs != 1 then
-
+    let p := c.p.insert (-k) x
+    let d := Int.ofNat k.natAbs
+    let c ← mkDvdCnstr d p (.ofEq x c)
+    c.assert
+  modify' fun s => { s with
+    elimEqs := s.elimEqs.set x (some c)
+    elimStack := x :: s.elimStack
+  }
 
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index 3ba60152dec7..d4bce2b55fde 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -37,8 +37,11 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do
     return mkApp10 (mkConst ``Int.Linear.dvd_solve_elim)
       (← getContext) (toExpr c₁.d) (toExpr c₁.p) (toExpr c₂.d) (toExpr c₂.p) (toExpr c'.d) (toExpr c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
-  | .subst _c₁ _c₂ => throwError "NIY"
-  | .ofEq _c => throwError "NIY"
+  | .subst _x _c₁ _c₂ => throwError "NIY"
+  | .ofEq x c =>
+    return mkApp7 (mkConst ``Int.Linear.dvd_of_eq)
+      (← getContext) (toExpr x) (toExpr c.p) (toExpr c'.d) (toExpr c'.p)
+      reflBoolTrue (← c.toExprProof)
 
 partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
   match c'.h with
@@ -56,7 +59,14 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
       (← getContext) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p)
       reflBoolTrue
       (← c₁.toExprProof) (← c₂.toExprProof)
-  | .subst _c₁ _c₂ => throwError "NIY"
+  | .subst _x _c₁ _c₂ => throwError "NIY"
+
+partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
+  match c'.h with
+  | .expr h =>
+    return h
+  | .norm _c => throwError "NIY"
+  | .subst _x _c₁ _c₂  => throwError "NIY"
 
 end
 end Lean.Meta.Grind.Arith.Cutsat
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
index c743d8159836..e6fe0cd71d72 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
@@ -34,8 +34,8 @@ inductive DvdCnstrProof where
   | solveCombine (c₁ c₂ : DvdCnstr)
   | solveElim (c₁ c₂ : DvdCnstr)
   | elim (c : DvdCnstr)
-  | ofEq (c : EqCnstr)
-  | subst (c₁ : EqCnstr) (c₂ : DvdCnstr)
+  | ofEq (x : Var) (c : EqCnstr)
+  | subst (x : Var) (c₁ : EqCnstr) (c₂ : DvdCnstr)
 
 structure LeCnstr where
   p  : Poly
@@ -48,7 +48,7 @@ inductive LeCnstrProof where
   | norm (c : LeCnstr)
   | divCoeffs (c : LeCnstr)
   | combine (c₁ c₂ : LeCnstr)
-  | subst (c₁ : EqCnstr) (c₂ : LeCnstr)
+  | subst (x : Var) (c₁ : EqCnstr) (c₂ : LeCnstr)
   -- TODO: missing constructors
 
 structure EqCnstr where
@@ -59,7 +59,7 @@ structure EqCnstr where
 inductive EqCnstrProof where
   | expr (h : Expr)
   | norm (c : EqCnstr)
-  | subst (c₁ : EqCnstr) (c₂ : EqCnstr)
+  | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
 end
 
 /-- State of the cutsat procedure. -/
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
index cce8defcb099..91c450714520 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean
@@ -176,11 +176,9 @@ abbrev caching (id : Nat) (k : ProofM Expr) : ProofM Expr := do
     modify fun s => { s with cache := s.cache.insert id h }
     return h
 
-abbrev DvdCnstr.caching (c : DvdCnstr) (k : ProofM Expr) : ProofM Expr :=
-  Cutsat.caching c.id k
-
-abbrev LeCnstr.caching (c : LeCnstr) (k : ProofM Expr) : ProofM Expr :=
-  Cutsat.caching c.id k
+abbrev DvdCnstr.caching (c : DvdCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
+abbrev LeCnstr.caching (c : LeCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
+abbrev EqCnstr.caching (c : EqCnstr) (k : ProofM Expr) : ProofM Expr := Cutsat.caching c.id k
 
 abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
   withLetDecl `ctx (mkApp (mkConst ``RArray) (mkConst ``Int)) (← toContextExpr) fun ctx => do

From a61654998005f235274a99dc2494e928d3c67fe3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 19:26:41 -0800
Subject: [PATCH 05/10] test: eq -> dvd

---
 .../Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean  |  3 +++
 tests/lean/run/grind_cutsat_eq_1.lean            | 16 ++++++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 tests/lean/run/grind_cutsat_eq_1.lean

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 011328ee32f8..3721fd03770c 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -11,6 +11,9 @@ namespace Lean.Meta.Grind.Arith.Cutsat
 def mkEqCnstr (p : Poly) (h : EqCnstrProof) : GoalM EqCnstr := do
   return { p, h, id := (← mkCnstrId) }
 
+/--
+Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.
+-/
 def _root_.Int.Linear.Poly.pickVarToElim? (p : Poly) : Option (Int × Var) :=
   match p with
   | .num _ => none
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
new file mode 100644
index 000000000000..5f5c822a28a7
--- /dev/null
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -0,0 +1,16 @@
+set_option grind.warning false
+set_option grind.debug true
+open Int.Linear
+
+-- set_option trace.grind.cutsat.assert true
+-- set_option trace.grind.cutsat.internalize true
+
+/-- info: [grind.cutsat.eq] b + 「f a」 + 1 = 0 -/
+#guard_msgs (info) in
+set_option trace.grind.cutsat.eq true in
+example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2)  : False := by
+  fail_if_success grind
+  sorry
+
+example (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
+  grind

From 114b51b36ef22dae88b62e9f643e5349033ba2a6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 19:48:14 -0800
Subject: [PATCH 06/10] feat: add `eq_norm`

---
 src/Init/Data/Int/Linear.lean                 |  6 ++++++
 .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean    | 21 +++++++++++++++++++
 .../Meta/Tactic/Grind/Arith/Cutsat/Proof.lean |  3 ++-
 tests/lean/run/grind_cutsat_eq_1.lean         |  8 ++++++-
 4 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index ab9ad55a6b64..54da561899ef 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -850,6 +850,12 @@ theorem le_unsat (ctx : Context) (p : Poly) : p.isUnsatLe → p.denote' ctx ≤
   have := Int.lt_of_le_of_lt h₂ h₁
   simp at this
 
+theorem eq_norm (ctx : Context) (p₁ p₂ : Poly) (h : p₁.norm == p₂) : p₁.denote' ctx = 0 → p₂.denote' ctx = 0 := by
+  simp at h
+  replace h := congrArg (Poly.denote ctx) h
+  simp at h
+  simp [*]
+
 def Poly.coeff (p : Poly) (x : Var) : Int :=
   match p with
   | .add a y p => bif x == y then a else coeff p x
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 3721fd03770c..8073e39b15b6 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -8,9 +8,16 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
 
 namespace Lean.Meta.Grind.Arith.Cutsat
+
 def mkEqCnstr (p : Poly) (h : EqCnstrProof) : GoalM EqCnstr := do
   return { p, h, id := (← mkCnstrId) }
 
+def EqCnstr.norm (c : EqCnstr) : GoalM EqCnstr := do
+  let c ← if c.p.isSorted then
+    pure c
+  else
+    mkEqCnstr c.p.norm (.norm c)
+
 /--
 Selects the variable in the given linear polynomial whose coefficient has the smallest absolute value.
 -/
@@ -30,8 +37,22 @@ where
         else
           go k x p
 
+/--
+Given a polynomial `p`, returns `some (x, k, c)` if `p` contains the monomial `k*x`,
+and `x` has been eliminated using the equality `c`.
+-/
+def _root_.Int.Linear.Poly.findVarToSubst (p : Poly) : GoalM (Option (Int × Var × EqCnstr)) := do
+  match p with
+  | .num _ => return none
+  | .add k x p =>
+    if let some c := (← get').elimEqs[x]! then
+      return some (k, x, c)
+    else
+      findVarToSubst p
+
 def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
   if (← isInconsistent) then return ()
+  let c ← c.norm
   -- TODO: apply substitutions
   trace[grind.cutsat.eq] "{← c.pp}"
   let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index d4bce2b55fde..bb3392d8724d 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -65,7 +65,8 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
   match c'.h with
   | .expr h =>
     return h
-  | .norm _c => throwError "NIY"
+  | .norm c =>
+    return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (toExpr c.p) (toExpr c'.p) reflBoolTrue (← c.toExprProof)
   | .subst _x _c₁ _c₂  => throwError "NIY"
 
 end
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index 5f5c822a28a7..feef3e1694ef 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -12,5 +12,11 @@ example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2)  : False := by
   fail_if_success grind
   sorry
 
-example (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
+theorem ex₁ (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
   grind
+
+theorem ex₂ (a b : Int) (_ : 2 ∣ 3*a + 1) (_ : 2*b + 3*a = 0) : False := by
+  grind
+
+#print ex₁
+#print ex₂

From ff68316026427f6fef0fe09a51af43f5c1d2b0af Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 19:59:59 -0800
Subject: [PATCH 07/10] feat: simplify `eq_eq_subst`

---
 src/Init/Data/Int/Linear.lean | 30 ++----------------------------
 1 file changed, 2 insertions(+), 28 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 54da561899ef..263429cf24d8 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -933,43 +933,17 @@ theorem eq_dvd_subst (ctx : Context) (x : Var) (p₁ : Poly) (d₂ : Int) (p₂
   apply abs_dvd
   simp [this]
 
-private theorem eq_eq_subst' {a x p b q : Int} : a*x + p = 0 → b*x + q = 0 → b*p - a*q = 0 := by
-  intro h₁ h₂
-  replace h₁ := congrArg (b*·) h₁; simp at h₁
-  replace h₂ := congrArg ((-a)*.) h₂; simp at h₂
-  rw [Int.add_comm] at h₁
-  replace h₁ := Int.neg_eq_of_add_eq_zero h₁
-  rw [← h₁]; clear h₁
-  replace h₂ := Int.neg_eq_of_add_eq_zero h₂; simp at h₂
-  rw [h₂]; clear h₂
-  rw [Int.mul_left_comm]
-  simp
-
 def eq_eq_subst_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
   let a := p₁.coeff x
   let b := p₂.coeff x
-  let p := p₁.insert (-a) x
-  let q := p₂.insert (-b) x
-  p₃ == (p.mul b |>.combine (q.mul (-a)))
+  p₃ == (p₁.mul b |>.combine (p₂.mul (-a)))
 
 theorem eq_eq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
     : eq_eq_subst_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx = 0 → p₃.denote' ctx = 0 := by
   simp [eq_eq_subst_cert]
-  have eq₁ := eq_add_coeff_insert ctx p₁ x
-  have eq₂ := eq_add_coeff_insert ctx p₂ x
-  revert eq₁ eq₂
-  generalize p₁.coeff x = a
-  generalize p₂.coeff x = b
-  generalize p₁.insert (-a) x = p
-  generalize p₂.insert (-b) x = q
-  intro eq₁; simp [eq₁]; clear eq₁
-  intro eq₂; simp [eq₂]; clear eq₂
   intro; subst p₃
   intro h₁ h₂
-  rw [Int.add_comm] at h₁ h₂
-  have := eq_eq_subst' h₁ h₂
-  rw [Int.sub_eq_add_neg] at this
-  simp [this]
+  simp [*]
 
 private theorem eq_le_subst_nonneg' {a x p b q : Int} : a ≥ 0 → a*x + p = 0 → b*x + q ≤ 0 → a*q - b*p ≤ 0 := by
   intro h h₁ h₂

From 7f15efef35498dbeec289da8b46f1e6d4dddb7f8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 20:06:20 -0800
Subject: [PATCH 08/10] feat: simplify `eq_le_subst_nonneg`

---
 src/Init/Data/Int/Linear.lean | 31 ++++---------------------------
 1 file changed, 4 insertions(+), 27 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 263429cf24d8..171c6b585ab0 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -945,43 +945,20 @@ theorem eq_eq_subst (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃
   intro h₁ h₂
   simp [*]
 
-private theorem eq_le_subst_nonneg' {a x p b q : Int} : a ≥ 0 → a*x + p = 0 → b*x + q ≤ 0 → a*q - b*p ≤ 0 := by
-  intro h h₁ h₂
-  replace h₁ := congrArg ((-b)*·) h₁; simp at h₁
-  rw [Int.add_comm, Int.mul_left_comm] at h₁
-  replace h₁ := Int.neg_eq_of_add_eq_zero h₁; simp at h₁
-  replace h₂ := Int.mul_le_mul_of_nonneg_left h₂ h
-  rw [Int.mul_add, h₁] at h₂; clear h₁
-  simp at h₂
-  rw [Int.sub_eq_add_neg]
-  assumption
-
 def eq_le_subst_nonneg_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
   let a := p₁.coeff x
   let b := p₂.coeff x
-  let p := p₁.insert (-a) x
-  let q := p₂.insert (-b) x
-  a ≥ 0 && p₃ == (q.mul a |>.combine (p.mul (-b)))
+  a ≥ 0 && p₃ == (p₂.mul a |>.combine (p₁.mul (-b)))
 
 theorem eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
     : eq_le_subst_nonneg_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
   simp [eq_le_subst_nonneg_cert]
-  have eq₁ := eq_add_coeff_insert ctx p₁ x
-  have eq₂ := eq_add_coeff_insert ctx p₂ x
-  revert eq₁ eq₂
-  generalize p₁.coeff x = a
-  generalize p₂.coeff x = b
-  generalize p₁.insert (-a) x = p
-  generalize p₂.insert (-b) x = q
-  intro eq₁; simp [eq₁]; clear eq₁
-  intro eq₂; simp [eq₂]; clear eq₂
   intro h
   intro; subst p₃
   intro h₁ h₂
-  rw [Int.add_comm] at h₁ h₂
-  have := eq_le_subst_nonneg' h h₁ h₂
-  rw [Int.sub_eq_add_neg, Int.add_comm] at this
-  simp [this]
+  replace h₂ := Int.mul_le_mul_of_nonneg_left h₂ h
+  simp at h₂
+  simp [*]
 
 private theorem eq_le_subst_nonpos' {a x p b q : Int} : a ≤ 0 → a*x + p = 0 → b*x + q ≤ 0 → b*p - a*q ≤ 0 := by
   intro h h₁ h₂

From 4b97ad56b5494581eee38e5a2a8fc128221e3d39 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 20:10:38 -0800
Subject: [PATCH 09/10] feat: simplify `eq_le_subst_nonpos`

---
 src/Init/Data/Int/Linear.lean | 37 +++++++----------------------------
 1 file changed, 7 insertions(+), 30 deletions(-)

diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index 171c6b585ab0..21a610fd7310 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -960,46 +960,23 @@ theorem eq_le_subst_nonneg (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly)
   simp at h₂
   simp [*]
 
-private theorem eq_le_subst_nonpos' {a x p b q : Int} : a ≤ 0 → a*x + p = 0 → b*x + q ≤ 0 → b*p - a*q ≤ 0 := by
-  intro h h₁ h₂
-  replace h₁ := congrArg (b*·) h₁; simp at h₁
-  rw [Int.add_comm, Int.mul_left_comm] at h₁
-  replace h₁ := Int.neg_eq_of_add_eq_zero h₁; simp at h₁
-  replace h : (-a) ≥ 0 := by
-    have := Int.neg_le_neg h
-    simp at this
-    exact this
-  replace h₂ := Int.mul_le_mul_of_nonneg_left h₂ h; simp at h₂; clear h
-  rw [h₁] at h₂
-  rw [Int.add_comm, ←Int.sub_eq_add_neg] at h₂
-  assumption
-
 def eq_le_subst_nonpos_cert (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly) : Bool :=
   let a := p₁.coeff x
   let b := p₂.coeff x
-  let p := p₁.insert (-a) x
-  let q := p₂.insert (-b) x
-  a ≤ 0 && p₃ == (p.mul b |>.combine (q.mul (-a)))
+  a ≤ 0 && p₃ == (p₁.mul b |>.combine (p₂.mul (-a)))
 
 theorem eq_le_subst_nonpos (ctx : Context) (x : Var) (p₁ : Poly) (p₂ : Poly) (p₃ : Poly)
     : eq_le_subst_nonpos_cert x p₁ p₂ p₃ → p₁.denote' ctx = 0 → p₂.denote' ctx ≤ 0 → p₃.denote' ctx ≤ 0 := by
   simp [eq_le_subst_nonpos_cert]
-  have eq₁ := eq_add_coeff_insert ctx p₁ x
-  have eq₂ := eq_add_coeff_insert ctx p₂ x
-  revert eq₁ eq₂
-  generalize p₁.coeff x = a
-  generalize p₂.coeff x = b
-  generalize p₁.insert (-a) x = p
-  generalize p₂.insert (-b) x = q
-  intro eq₁; simp [eq₁]; clear eq₁
-  intro eq₂; simp [eq₂]; clear eq₂
   intro h
   intro; subst p₃
   intro h₁ h₂
-  rw [Int.add_comm] at h₁ h₂
-  have := eq_le_subst_nonpos' h h₁ h₂
-  rw [Int.sub_eq_add_neg] at this
-  simp [this]
+  simp [*]
+  replace h₂ := Int.mul_le_mul_of_nonpos_left h₂ h; simp at h₂; clear h
+  rw [← Int.neg_zero]
+  apply Int.neg_le_neg
+  rw [Int.mul_comm]
+  assumption
 
 end Int.Linear
 

From 83114143f93eb710804474aa5addbe8adfacdbf3 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 23 Feb 2025 20:26:35 -0800
Subject: [PATCH 10/10] feat: apply substitutions

---
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean         |  1 +
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 12 +++++++++++-
 src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean   |  5 ++++-
 tests/lean/run/grind_cutsat_eq_1.lean                | 12 +++++++++++-
 4 files changed, 27 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
index 7281e354c888..88b73af07cf9 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
@@ -18,6 +18,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.EqCnstr
 namespace Lean
 
 builtin_initialize registerTraceClass `grind.cutsat
+builtin_initialize registerTraceClass `grind.cutsat.subst
 builtin_initialize registerTraceClass `grind.cutsat.eq
 builtin_initialize registerTraceClass `grind.cutsat.assert
 builtin_initialize registerTraceClass `grind.cutsat.assert.dvd
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 8073e39b15b6..f38bca8a00ed 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -50,10 +50,20 @@ def _root_.Int.Linear.Poly.findVarToSubst (p : Poly) : GoalM (Option (Int × Var
     else
       findVarToSubst p
 
+partial def applySubsts (c : EqCnstr) : GoalM EqCnstr := do
+  let some (a, x, c₁) ← c.p.findVarToSubst | return c
+  trace[grind.cutsat.subst] "{← getVar x}, {← c.pp}, {← c₁.pp}"
+  let b := c₁.p.coeff x
+  let p := c.p.mul (-b) |>.combine (c₁.p.mul a)
+  let c ← mkEqCnstr p (.subst x c₁ c)
+  applySubsts c
+
 def EqCnstr.assert (c : EqCnstr) : GoalM Unit := do
   if (← isInconsistent) then return ()
+  trace[grind.cutsat.assert] "{← c.pp}"
   let c ← c.norm
-  -- TODO: apply substitutions
+  let c ← applySubsts c
+  -- TODO: check coeffsr
   trace[grind.cutsat.eq] "{← c.pp}"
   let some (k, x) := c.p.pickVarToElim? | c.throwUnexpected
   -- TODO: eliminate `x` from lowers, uppers, and dvdCnstrs
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index bb3392d8724d..e3ae2821964c 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -67,7 +67,10 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := c'.caching do
     return h
   | .norm c =>
     return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (toExpr c.p) (toExpr c'.p) reflBoolTrue (← c.toExprProof)
-  | .subst _x _c₁ _c₂  => throwError "NIY"
+  | .subst x c₁ c₂  =>
+    return mkApp8 (mkConst ``Int.Linear.eq_eq_subst)
+      (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.p) (toExpr c'.p)
+      reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
 
 end
 end Lean.Meta.Grind.Arith.Cutsat
diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean
index feef3e1694ef..5e9982072356 100644
--- a/tests/lean/run/grind_cutsat_eq_1.lean
+++ b/tests/lean/run/grind_cutsat_eq_1.lean
@@ -1,5 +1,5 @@
 set_option grind.warning false
-set_option grind.debug true
+-- set_option grind.debug true -- TODO: enable after making more progress in `EqCnstr.lean`
 open Int.Linear
 
 -- set_option trace.grind.cutsat.assert true
@@ -18,5 +18,15 @@ theorem ex₁ (a b : Int) (_ : 2*a + 3*b = 0) (_ : 2 ∣ 3*b + 1) : False := by
 theorem ex₂ (a b : Int) (_ : 2 ∣ 3*a + 1) (_ : 2*b + 3*a = 0) : False := by
   grind
 
+set_option trace.grind.cutsat.subst true
+
+theorem ex₃ (a b c : Int) (_ : c + 3*a = 0) (_ : 2 ∣ 3*a + 1) (_ : 2*b + c = 0) : False := by
+  grind
+
+theorem ex₄ (a b c : Int) (_ : 2*c + 3*a = 0) (_ : 2*b + c = 0) (_ : 2 ∣ 3*a + 1) : False := by
+  grind
+
 #print ex₁
 #print ex₂
+#print ex₃
+#print ex₄