test: model for Nat

src/Init/Data/Int/Linear.lean

@@ -1827,6 +1827,14 @@ theorem eq_def (ctx : Context) (x : Var) (xPoly : Poly) (p : Poly)
   simp [eq_def_cert]; intro _ h; subst p; simp [h]
   rw [← Int.sub_eq_add_neg, Int.sub_self]
 
+def eq_def'_cert (x : Var) (e : Expr) (p : Poly) : Bool :=
+  p == .add (-1) x e.norm
+
+theorem eq_def' (ctx : Context) (x : Var) (e : Expr) (p : Poly)
+    : eq_def'_cert x e p → x.denote ctx = e.denote ctx → p.denote' ctx = 0 := by
+  simp [eq_def'_cert]; intro _ h; subst p; simp [h]
+  rw [← Int.sub_eq_add_neg, Int.sub_self]
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by

src/Init/Data/Int/OfNat.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Int.Lemmas
 import Init.Data.Int.DivMod
+import Init.Data.Int.Linear
 import Init.Data.RArray
 
 namespace Int.OfNat
@@ -47,6 +48,9 @@ def Expr.denoteAsInt (ctx : Context) : Expr → Int
 theorem Expr.denoteAsInt_eq (ctx : Context) (e : Expr) : e.denoteAsInt ctx = e.denote ctx := by
   induction e <;> simp [denote, denoteAsInt, Int.ofNat_ediv, *] <;> rfl
 
+theorem Expr.eq_denoteAsInt (ctx : Context) (e : Expr) : e.denote ctx = e.denoteAsInt ctx := by
+  apply Eq.symm; apply denoteAsInt_eq
+
 theorem Expr.eq (ctx : Context) (lhs rhs : Expr)
     : (lhs.denote ctx = rhs.denote ctx) = (lhs.denoteAsInt ctx = rhs.denoteAsInt ctx) := by
   simp [denoteAsInt_eq, Int.ofNat_inj]

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

@@ -390,6 +390,27 @@ private def propagateToNat (e : Expr) : GoalM Unit := do
   let_expr Int.toNat a := e | return ()
   pushNewFact <| mkApp (mkConst ``Int.OfNat.ofNat_toNat) a
 
+private def internalizeNat (e : Expr) : GoalM Unit := do
+  let e' : Int.OfNat.Expr ← Int.OfNat.toOfNatExpr e
+  let gen ← getGeneration e
+  let ctx ← getForeignVars .nat
+  let e'' : Expr ← e'.denoteAsIntExpr ctx
+  -- If `e''` is of the form `NatCast.natCast e`, then it is wasteful to
+  -- assert an equality
+  match_expr e'' with
+  | NatCast.natCast _ _ a => if e == a then return ()
+  | _ => pure ()
+  let e'' : Int.Linear.Expr ← toLinearExpr e'' gen
+  let p := e''.norm
+  let natCast_e ← shareCommon (mkIntNatCast e)
+  trace[grind.cutsat.internalize] "natCast: {natCast_e}"
+  internalize natCast_e gen
+  trace[grind.cutsat.internalize] "{aquote natCast_e}:= {← p.pp}"
+  let x ← mkVar natCast_e
+  modify' fun s => { s with foreignDef := s.foreignDef.insert { expr := e } x }
+  let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }
+  c.assert
+
 /--
 Internalizes an integer (and `Nat`) expression. Here are the different cases that are handled.
 
@@ -410,11 +431,13 @@ def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
     | .num => pure ()
     | _ => internalizeInt e
   else if type.isConstOf ``Nat then
+    if (← hasForeignVar e) then return ()
     discard <| mkForeignVar e .nat
     match k with
     | .sub => propagateNatSub e
     | .natAbs => propagateNatAbs e
     | .toNat => propagateToNat e
-    | _ => pure ()
+    | .num => pure ()
+    | _ => internalizeNat e
 
 end Lean.Meta.Grind.Arith.Cutsat

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

@@ -148,6 +148,7 @@ asserts that it is nonnegative.
 def assertNatCast (e : Expr) (x : Var) : GoalM Unit := do
   let_expr NatCast.natCast _ inst a := e | return ()
   let_expr instNatCastInt := inst | return ()
+  if (← get').foreignDef.contains { expr := a } then return ()
   trace[grind.debug.cutsat.natCast] "{a}"
   let n ← mkForeignVar a .nat
   let p := .add (-1) x (.num 0)

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

@@ -142,6 +142,9 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
   | .defn e p =>
     let some x := (← get').varMap.find? { expr := e } | throwError "`grind` internal error, missing cutsat variable{indentExpr e}"
     return mkApp6 (mkConst ``Int.Linear.eq_def) (← getContext) (toExpr x) (← mkPolyDecl p) (← mkPolyDecl c'.p) reflBoolTrue (← mkEqRefl e)
+  | .defnNat e x e' =>
+    let h := mkApp2 (mkConst ``Int.OfNat.Expr.eq_denoteAsInt) (← getForeignContext .nat) (← mkNatExprDecl e)
+    return mkApp6 (mkConst ``Int.Linear.eq_def') (← getContext) (toExpr x) (← mkExprDecl e') (← mkPolyDecl c'.p) reflBoolTrue h
   | .norm c =>
     return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) reflBoolTrue (← c.toExprProof)
   | .divCoeffs c =>
@@ -419,7 +422,7 @@ private def markAsFound (fvarId : FVarId) : CollectDecVarsM Unit := do
 mutual
 partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core0 .. | .core .. | .coreNat .. | .defn .. => return () -- Equalities coming from the core never contain cutsat decision variables
+  | .core0 .. | .core .. | .coreNat .. | .defn .. | .defnNat .. => return () -- Equalities coming from the core never contain cutsat decision variables
   | .norm c | .divCoeffs c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 

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

@@ -85,12 +85,13 @@ inductive EqCnstrProof where
     -/
     core (a b : Expr) (p₁ p₂ : Poly)
   | coreNat (a b : Expr) (lhs rhs : Int.OfNat.Expr) (lhs' rhs' : Int.Linear.Expr)
+  | /-- `e` is `p` -/
+    defn (e : Expr) (p : Poly)
+  | defnNat (e : Int.OfNat.Expr) (x : Var) (e' : Int.Linear.Expr)
   | norm (c : EqCnstr)
   | divCoeffs (c : EqCnstr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | ofLeGe (c₁ : LeCnstr) (c₂ : LeCnstr)
-  | /-- `e` is `p` -/
-    defn (e : Expr) (p : Poly)
 
 /-- A divisibility constraint and its justification/proof. -/
 structure DvdCnstr where
@@ -237,6 +238,12 @@ structure State where
   foreignVarMap : PHashMap ENodeKey (Var × ForeignType) := {}
   foreignVars : PHashMap ForeignType (PArray Expr) := {}
   /--
+  Some foreign variables encode nested terms such as `b+1`.
+  This is a mapping from this kind of variable to the integer variable
+  representing `natCast (b+1)`.
+  -/
+  foreignDef : PHashMap ENodeKey Var := {}
+  /--
   Mapping from variables to divisibility constraints. Recall that we keep the divisibility constraint in solved form.
   Thus, we have at most one divisibility per variable. -/
   dvds : PArray (Option DvdCnstr) := {}

tests/lean/run/grind_cutsat_nat_eq.lean

@@ -113,3 +113,13 @@ example (x y : Int) : x ^ 0 - y = 0 → y = 1 := by
 
 example (x y : Nat) : x ^ 0 + y = 0 → False := by
   grind
+
+/--
+info: [grind.cutsat.model] x := 4
+[grind.cutsat.model] y := 1
+-/
+#guard_msgs (info) in
+set_option trace.grind.cutsat.model true in
+example (x y : Nat) : x = y + 3 → y > 0 → False := by
+  fail_if_success grind
+  sorry