chore: fix test

src/Lean/Meta/Tactic/Grind/Arith/Model.lean

@@ -9,31 +9,63 @@ import Lean.Meta.Tactic.Grind.Types
 import Lean.Meta.Tactic.Grind.Util
 
 namespace Lean.Meta.Grind.Arith.Offset
+
+
 /-- Construct a model that statisfies all offset constraints -/
 def mkModel (goal : Goal) : MetaM (Array (Expr × Nat)) := do
   let s := goal.arith.offset
+  let dbg := grind.debug.get (← getOptions)
   let nodes := s.nodes
+  let isInterpreted (u : Nat) : Bool := isNatNum s.nodes[u]!
   let mut pre : Array (Option Int) := mkArray nodes.size none
+  /-
+  `needAdjust[u]` is true if `u` assignment is not connected to an interpreted value in the graph.
+  That is, its assignment may be negative.
+  -/
+  let mut needAdjust : Array Bool := mkArray nodes.size true
+  -- Initialize `needAdjust`
+  for u in [: nodes.size] do
+    if isInterpreted u then
+      -- Interpreted values have a fixed value.
+      needAdjust := needAdjust.set! u false
+    else if s.sources[u]!.any fun v _ => isInterpreted v then
+      needAdjust := needAdjust.set! u false
+    else if s.targets[u]!.any fun v _ => isInterpreted v then
+      needAdjust := needAdjust.set! u false
+  -- Set interpreted values
+  for h : u in [:nodes.size] do
+    let e := nodes[u]
+    if let some v ← getNatValue? e then
+      pre := pre.set! u (Int.ofNat v)
+  -- Set remaining values
   for u in [:nodes.size] do
-    let val? := s.sources[u]!.foldl (init := @none Int) fun val? v k => Id.run do
+    let lower? := s.sources[u]!.foldl (init := none) fun val? v k => Id.run do
       let some va := pre[v]! | return val?
       let val' := va - k
       let some val := val? | return val'
       if val' > val then return val' else val?
-    let val? := s.targets[u]!.foldl (init := val?) fun val? v k => Id.run do
+    let upper? := s.targets[u]!.foldl (init := none) fun val? v k => Id.run do
       let some va := pre[v]! | return val?
       let val' := va + k
       let some val := val? | return val'
       if val' < val then return val' else val?
-    let val := val?.getD 0
-    pre := pre.set! u (some val)
+    if dbg then
+      let some upper := upper? | pure ()
+      let some lower := lower? | pure ()
+      assert! lower ≤ upper
+      let some val := pre[u]! | pure ()
+      assert! lower ≤ val
+      assert! val ≤ upper
+    unless pre[u]!.isSome do
+      let val := lower?.getD (upper?.getD 0)
+      pre := pre.set! u (some val)
   let min := pre.foldl (init := 0) fun min val? => Id.run do
     let some val := val? | return min
     if val < min then val else min
   let mut r := {}
   for u in [:nodes.size] do
     let some val := pre[u]! | unreachable!
-    let val := (val - min).toNat
+    let val := if needAdjust[u]! then (val - min).toNat else val.toNat
     let e := nodes[u]!
     /-
     We should not include the assignment for auxiliary offset terms since

tests/lean/run/grind_offset_model.lean

@@ -0,0 +1,119 @@
+def g (i : Nat) (j : Nat) := i + j
+
+set_option grind.debug true
+set_option grind.debug.proofs true
+
+/--
+error: `grind` failed
+case grind
+i j : Nat
+h : j + 1 ≤ i
+x✝ : ¬g (i + 1) j = i + 1
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] j + 1 ≤ i
+    [prop] ¬g (i + 1) j = i + 1
+  [eqc] True propositions
+    [prop] j + 1 ≤ i
+  [eqc] False propositions
+    [prop] g (i + 1) j = i + 1
+  [offset] Assignment satisfying offset contraints
+    [assign] j := 0
+    [assign] i := 1
+    [assign] i + 1 := 2
+    [assign] 0 := 0
+-/
+#guard_msgs (error) in
+example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = i + 1 := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+i : Nat
+x✝ : 101 ≤ i
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] 101 ≤ i
+  [eqc] True propositions
+    [prop] 101 ≤ i
+  [offset] Assignment satisfying offset contraints
+    [assign] 0 := 0
+    [assign] i := 101
+-/
+#guard_msgs (error) in
+example (i : Nat) : i ≤ 100 := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+i : Nat
+x✝ : i ≤ 99
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] i ≤ 99
+  [eqc] True propositions
+    [prop] i ≤ 99
+  [offset] Assignment satisfying offset contraints
+    [assign] i := 99
+    [assign] 0 := 0
+-/
+#guard_msgs (error) in
+example (i : Nat) : 100 ≤ i := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+n m a j i : Nat
+a✝ : g (n + 1) m = a
+x✝ : i ≤ j + 99
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] g (n + 1) m = a
+    [prop] i ≤ j + 99
+  [eqc] True propositions
+    [prop] i ≤ j + 99
+  [eqc] Equivalence classes
+    [eqc] {g (n + 1) m, a}
+  [offset] Assignment satisfying offset contraints
+    [assign] n + 1 := 1
+    [assign] n := 0
+    [assign] 0 := 0
+    [assign] i := 99
+    [assign] j := 0
+-/
+#guard_msgs (error) in
+example (i : Nat) : g (n + 1) m = a → 100 + j ≤ i := by
+  grind
+
+/--
+error: `grind` failed
+case grind
+n m a j i : Nat
+a✝ : g (n + 1) m = a
+x✝ : i + 101 ≤ j
+⊢ False
+[grind] Diagnostics
+  [facts] Asserted facts
+    [prop] g (n + 1) m = a
+    [prop] i + 101 ≤ j
+  [eqc] True propositions
+    [prop] i + 101 ≤ j
+  [eqc] Equivalence classes
+    [eqc] {g (n + 1) m, a}
+  [offset] Assignment satisfying offset contraints
+    [assign] n + 1 := 1
+    [assign] n := 0
+    [assign] 0 := 0
+    [assign] i := 0
+    [assign] j := 101
+-/
+#guard_msgs (error) in
+example (i : Nat) : g (n + 1) m = a → j ≤ i + 100 := by
+  grind

tests/lean/run/grind_pre.lean

@@ -94,10 +94,12 @@ x✝ : ¬g (i + 1) j ⋯ = i + j + 1
   [offset] Assignment satisfying offset contraints
     [assign] j := 0
     [assign] i := 1
-    [assign] i + j := 1
+    [assign] i + 1 := 2
+    [assign] 0 := 0
+    [assign] i + j + 1 := 1
+    [assign] i + j := 0
 -/
 #guard_msgs (error) in
-set_option grind.debug false in
 example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
   grind