feat: resolveCooperPred

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Cooper.lean

@@ -1,24 +0,0 @@
-/-
-Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-
-namespace Lean.Meta.Grind.Arith.Cutsat
-
-def CooperSplit.numCases (s : CooperSplit) : Nat :=
-  let a  := s.c₁.p.leadCoeff
-  let b  := s.c₂.p.leadCoeff
-  match s.c₃? with
-  | none => if s.left then a.natAbs else b.natAbs
-  | some c₃ =>
-    let c  := c₃.p.leadCoeff
-    let d  := c₃.d
-    if s.left then
-      Int.lcm a (a * d / Int.gcd (a * d) c)
-    else
-      Int.lcm b (b * d / Int.gcd (b * d) c)
-
-end Lean.Meta.Grind.Arith.Cutsat

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
-import Lean.Meta.Tactic.Grind.Arith.Cutsat.Cooper
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -66,25 +65,27 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := c'.caching do
     return mkApp10 (mkConst ``Int.Linear.eq_dvd_subst)
       (← getContext) (toExpr x) (toExpr c₁.p) (toExpr c₂.d) (toExpr c₂.p) (toExpr c'.d) (toExpr c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
-  | .cooper₁ c =>
-    let p₁ := c.c₁.p
-    let p₂ := c.c₂.p
-    match c.c₃? with
+  | .cooper₁ s =>
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    match c₃? with
     | none =>
-      let thmName := if c.left then ``Int.Linear.cooper_left_split_dvd else ``Int.Linear.cooper_right_split_dvd
+      let thmName := if left then ``Int.Linear.cooper_left_split_dvd else ``Int.Linear.cooper_right_split_dvd
       return mkApp8 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
     | some c₃ =>
-      let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_dvd1 else ``Int.Linear.cooper_dvd_right_split_dvd1
+      let thmName := if left then ``Int.Linear.cooper_dvd_left_split_dvd1 else ``Int.Linear.cooper_dvd_right_split_dvd1
       return mkApp10 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
-  | .cooper₂ c =>
-    let p₁ := c.c₁.p
-    let p₂ := c.c₂.p
-    let some c₃ := c.c₃? | throwError "`grind` internal error, unexpected `cooper₂` proof"
-    let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_dvd2 else ``Int.Linear.cooper_dvd_right_split_dvd2
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
+  | .cooper₂ s =>
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    let some c₃ := c₃? | throwError "`grind` internal error, unexpected `cooper₂` proof"
+    let thmName := if left then ``Int.Linear.cooper_dvd_left_split_dvd2 else ``Int.Linear.cooper_dvd_right_split_dvd2
     return mkApp10 (mkConst thmName)
-      (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr c'.d) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+      (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
 
 partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
   match c'.h with
@@ -122,19 +123,20 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := c'.caching do
     let hNot := mkLambda `h .default (mkIntLE (← p₂.denoteExpr') (mkIntLit 0)) (hFalse.abstract #[mkFVar fvarId])
     return mkApp7 (mkConst ``Int.Linear.diseq_split_resolve)
       (← getContext) (toExpr c₁.p) (toExpr p₂) (toExpr c'.p) reflBoolTrue (← c₁.toExprProof) hNot
-  | .cooper c =>
-    let p₁ := c.c₁.p
-    let p₂ := c.c₂.p
-    let coeff := if c.left then p₁.leadCoeff else p₂.leadCoeff
-    match c.c₃? with
+  | .cooper s =>
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    let coeff := if left then p₁.leadCoeff else p₂.leadCoeff
+    match c₃? with
     | none =>
-      let thmName := if c.left then ``Int.Linear.cooper_left_split_ineq else ``Int.Linear.cooper_right_split_ineq
+      let thmName := if left then ``Int.Linear.cooper_left_split_ineq else ``Int.Linear.cooper_right_split_ineq
       return mkApp8 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c.k) (toExpr coeff) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr s.k) (toExpr coeff) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
     | some c₃ =>
-      let thmName := if c.left then ``Int.Linear.cooper_dvd_left_split_ineq else ``Int.Linear.cooper_dvd_right_split_ineq
+      let thmName := if left then ``Int.Linear.cooper_dvd_left_split_ineq else ``Int.Linear.cooper_dvd_right_split_ineq
       return mkApp10 (mkConst thmName)
-        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr c.k) (toExpr coeff) (toExpr c'.p) (← c.toExprProof) reflBoolTrue
+        (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr coeff) (toExpr c'.p) (← s.toExprProof) reflBoolTrue
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := c'.caching do
   match c'.h with
@@ -158,24 +160,25 @@ partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s
   match s.h with
   | .dec h => return mkFVar h
   | .last hs _ =>
-    let p₁ := s.c₁.p
-    let p₂ := s.c₂.p
-    let n := s.numCases
+    let { c₁, c₂, c₃?, left } := s.pred
+    let p₁ := c₁.p
+    let p₂ := c₂.p
+    let n := s.pred.numCases
     unless hs.size + 1 == n do
       throwError "`grind` internal error, unexpected number of cases at `CopperSplit`"
-    let (base, pred) ← match s.c₃? with
+    let (base, pred) ← match c₃? with
       | none =>
-        let thmName := if s.left then ``Int.Linear.cooper_left else ``Int.Linear.cooper_right
-        let predName := if s.left then ``Int.Linear.cooper_left_split else ``Int.Linear.cooper_right_split
+        let thmName := if left then ``Int.Linear.cooper_left else ``Int.Linear.cooper_right
+        let predName := if left then ``Int.Linear.cooper_left_split else ``Int.Linear.cooper_right_split
         let base := mkApp7 (mkConst thmName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr n)
-          reflBoolTrue (← s.c₁.toExprProof) (← s.c₂.toExprProof)
+          reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
         let pred := mkApp3 (mkConst predName) (← getContext) (toExpr p₁) (toExpr p₂)
         pure (base, pred)
       | some c₃ =>
-        let thmName := if s.left then ``Int.Linear.cooper_dvd_left else ``Int.Linear.cooper_dvd_right
-        let predName := if s.left then ``Int.Linear.cooper_dvd_left_split else ``Int.Linear.cooper_dvd_right_split
+        let thmName := if left then ``Int.Linear.cooper_dvd_left else ``Int.Linear.cooper_dvd_right
+        let predName := if left then ``Int.Linear.cooper_dvd_left_split else ``Int.Linear.cooper_dvd_right_split
         let base := mkApp10 (mkConst thmName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d) (toExpr n)
-          reflBoolTrue (← s.c₁.toExprProof) (← s.c₂.toExprProof) (← c₃.toExprProof)
+          reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof) (← c₃.toExprProof)
         let pred := mkApp5 (mkConst predName) (← getContext) (toExpr p₁) (toExpr p₂) (toExpr c₃.p) (toExpr c₃.d)
         pure (base, pred)
     -- `pred` is an expressions of the form `cooper_*_split ...` with type `Nat → Prop`
@@ -256,8 +259,8 @@ partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do u
   | .norm c | .divCoeffs c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
-partial def CooperSplit.collectDecVars (c' : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited c'.id) do
-  match c'.h with
+partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited s.id) do
+  match s.h with
   | .dec h => markAsFound h
   | .last (decVars := decVars) .. => decVars.forM markAsFound
 

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Search.lean

@@ -14,6 +14,39 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
+/-- Asserts constraints implied by a `CooperSplit`. -/
+def CooperSplit.assert (cs : CooperSplit) : GoalM Unit := do
+  let { c₁, c₂, c₃?, left, .. } := cs.pred
+  let k   := cs.k
+  let p₁  := c₁.p
+  let p₂  := c₂.p
+  let p   := p₁.tail
+  let q   := p₂.tail
+  let a   := p₁.leadCoeff
+  let b   := p₂.leadCoeff
+  let p₁' := p.mul b |>.combine (q.mul (-a))
+  let p₁' := p₁'.addConst <| if left then b*k else (-a)*k
+  let c₁' ← mkLeCnstr p₁' (.cooper cs)
+  c₁'.assert
+  let p₂' := if left then p else q
+  let p₂' := p₂'.addConst k
+  let c₂' ← mkDvdCnstr (if left then a else b) p₂' (.cooper₁ cs)
+  c₂'.assert
+  let some c₃ := c₃? | return ()
+  let p₃  := c₃.p
+  let d   := c₃.d
+  let s   := p₃.tail
+  let c   := p₃.leadCoeff
+  let c₃' ← if left then
+    let p₃' := p.mul c |>.combine (s.mul (-a))
+    let p₃' := p₃'.addConst (c*k)
+    mkDvdCnstr (a*d) p₃' (.cooper₂ cs)
+  else
+    let p₃' := q.mul (-c) |>.combine (s.mul b)
+    let p₃' := p₃'.addConst (-c*k)
+    mkDvdCnstr (b*d) p₃' (.cooper₂ cs)
+  c₃'.assert
+
 private def checkIsNextVar (x : Var) : GoalM Unit := do
   if x != (← get').assignment.size then
     throwError "`grind` internal error, assigning variable out of order"
@@ -239,29 +272,19 @@ def resolveRealLowerUpperConflict (c₁ c₂ : LeCnstr) : GoalM Bool := do
     c.assert
     return true
 
-def resolveCooperLeft (c₁ c₂ : LeCnstr) : GoalM Unit := do
-  throwError "Cooper-left NIY {← c₁.pp}, {← c₂.pp}"
+def resolveCooperPred (pred : CooperSplitPred) : SearchM Unit := do
+  let n := pred.numCases
+  let fvarId ← mkCase (.cooper pred #[])
+  let s : CooperSplit := { pred, k := n - 1, id := (← mkCnstrId), h := .dec fvarId }
+  s.assert
 
-def resolveCooperRight (c₁ c₂ : LeCnstr) : GoalM Unit := do
-  throwError "Cooper-right NIY {← c₁.pp}, {← c₂.pp}"
+def resolveCooper (c₁ c₂ : LeCnstr) : SearchM Unit := do
+  let left : Bool := c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs
+  resolveCooperPred { c₁, c₂, left, c₃? := none }
 
-def resolveCooper (c₁ c₂ : LeCnstr) : GoalM Unit := do
-  if c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs then
-    resolveCooperLeft c₁ c₂
-  else
-    resolveCooperRight c₁ c₂
-
-def resolveCooperDvdLeft (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do
-  throwError "Cooper-dvd-left NIY {← c₁.pp}, {← c₂.pp}, {← c.pp}"
-
-def resolveCooperDvdRight (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do
-  throwError "Cooper-dvd-right NIY {← c₁.pp}, {← c₂.pp}, {← c.pp}"
-
-def resolveCooperDvd (c₁ c₂ : LeCnstr) (c : DvdCnstr) : GoalM Unit := do
-  if c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs then
-    resolveCooperDvdLeft c₁ c₂ c
-  else
-    resolveCooperDvdRight c₁ c₂ c
+def resolveCooperDvd (c₁ c₂ : LeCnstr) (c₃ : DvdCnstr) : SearchM Unit := do
+  let left : Bool := c₁.p.leadCoeff.natAbs < c₂.p.leadCoeff.natAbs
+  resolveCooperPred { c₁, c₂, left, c₃? := some c₃ }
 
 def resolveCooperDiseq (c₁ : DiseqCnstr) (c₂ : LeCnstr) (_c? : Option DvdCnstr) : GoalM Unit := do
   throwError "Cooper-diseq NIY {← c₁.pp}, {← c₂.pp}"

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/SearchM.lean

@@ -5,7 +5,6 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
--- import Lean.Meta.Tactic.Grind.Arith.Cutsat.Cooper
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 /--
@@ -15,10 +14,7 @@ In principle, we only need to support two kinds of case split.
 -/
 inductive CaseKind where
   | diseq (d : DiseqCnstr)
-  | copperLeft
-  | copperDvdLeft
-  | cooperRight
-  | cooperDvdRight
+  | cooper (s : CooperSplitPred) (hs : Array (FVarId × UnsatProof))
   deriving Inhabited
 
 structure Case where

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean

@@ -103,16 +103,22 @@ The specific predicate used is determined as follows:
 - `cooper_dvd_left_split` (if `left` is `true` and `c₃?` is `some`)
 - `cooper_dvd_right_split` (if `left` is `false` and `c₃?` is `some`)
 
-See `CooperSplitProof` for additional explanations.
+See `CooperSplit`
 -/
-structure CooperSplit where
+structure CooperSplitPred where
   left     : Bool
   c₁       : LeCnstr
   c₂       : LeCnstr
   c₃?      : Option DvdCnstr
-  k        : Nat
-  h        : CooperSplitProof
-  id       : Nat
+
+/--
+An instance of the `CooperSplitPred` at `k`.
+-/
+structure CooperSplit where
+  pred  : CooperSplitPred
+  k     : Nat
+  h     : CooperSplitProof
+  id    : Nat
 
 /--
 The `cooper_left`, `cooper_right`, `cooper_dvd_left`, and `cooper_dvd_right` theorems have a resulting type
@@ -191,6 +197,12 @@ instance : Inhabited LeCnstr where
 instance : Inhabited DvdCnstr where
   default := { d := 0, p := .num 0, h := .expr default, id := 0 }
 
+instance : Inhabited CooperSplitPred where
+  default := { left := false, c₁ := default, c₂ := default, c₃? := none }
+
+instance : Inhabited CooperSplit where
+  default := { pred := default, k := 0, h := .dec default, id := 0 }
+
 abbrev VarSet := RBTree Var compare
 
 /-- State of the cutsat procedure. -/

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Util.lean

@@ -278,4 +278,17 @@ def _root_.Int.Linear.Poly.findVarToSubst (p : Poly) : GoalM (Option (Int × Var
     else
       findVarToSubst p
 
+def CooperSplitPred.numCases (pred : CooperSplitPred) : Nat :=
+  let a  := pred.c₁.p.leadCoeff
+  let b  := pred.c₂.p.leadCoeff
+  match pred.c₃? with
+  | none => if pred.left then a.natAbs else b.natAbs
+  | some c₃ =>
+    let c  := c₃.p.leadCoeff
+    let d  := c₃.d
+    if pred.left then
+      Int.lcm a (a * d / Int.gcd (a * d) c)
+    else
+      Int.lcm b (b * d / Int.gcd (b * d) c)
+
 end Lean.Meta.Grind.Arith.Cutsat