feat: implement setUnsat in Grind/Arith/Offset.lean

src/Init/Grind/Offset.lean

@@ -19,17 +19,15 @@ theorem Nat.lo_le (u w v k : Nat) : u + k ≤ w → w ≤ v → u + k ≤ v := b
 theorem Nat.lo_lo (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w + k₂ ≤ v → u + (k₁ + k₂) ≤ v := by
   omega
 theorem Nat.lo_ro_1 (u w v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ w → w ≤ v + k₂ → u + (k₁ - k₂) ≤ v := by
-  simp [isLt]
-  omega
+  simp [isLt]; omega
 theorem Nat.lo_ro_2 (u w v k₁ k₂ : Nat) : u + k₁ ≤ w → w ≤ v + k₂ → u ≤ v + (k₂ - k₁) := by
   omega
 theorem Nat.ro_le (u w v k : Nat) : u ≤ w + k → w ≤ v → u ≤ v + k := by
   omega
 theorem Nat.ro_lo_1 (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w + k₂ ≤ v → u ≤ v + (k₁ - k₂) := by
   omega
 theorem Nat.ro_lo_2 (u w v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ w + k₁ → w + k₂ ≤ v → u + (k₂ - k₁) ≤ v := by
-  simp [isLt]
-  omega
+  simp [isLt]; omega
 theorem Nat.ro_ro (u w v k₁ k₂ : Nat) : u ≤ w + k₁ → w ≤ v + k₂ → u ≤ v + (k₁ + k₂) := by
   omega
 
@@ -42,4 +40,11 @@ theorem Nat.of_lo_eq_false (u v k : Nat) : ((u + k ≤ v) = False) → v ≤ u +
 theorem Nat.of_ro_eq_false (u v k : Nat) : ((u ≤ v + k) = False) → v + (k+1) ≤ u := by
   simp; omega
 
+theorem Nat.unsat_le_lo (u v k : Nat) : isLt 0 k = true → u ≤ v → v + k ≤ u → False := by
+  simp [isLt]; omega
+theorem Nat.unsat_lo_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False := by
+  simp [isLt]; omega
+theorem Nat.unsat_lo_ro (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → v ≤ u + k₂ → False := by
+  simp [isLt]; omega
+
 end Lean.Grind

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

@@ -50,9 +50,6 @@ def mkNode (expr : Expr) : GoalM NodeId := do
   }
   return nodeId
 
-def isUnsat : GoalM Bool :=
-  return (← get').unsat.isSome
-
 private def getDist? (u v : NodeId) : GoalM (Option Int) := do
   return (← get').targets[u]!.find? v
 
@@ -69,11 +66,26 @@ where
       let p' := (← getProof? u p.w).get!
       go (mkTrans (← get').nodes p' p v)
 
-private def setUnsat (u v : NodeId) (k : Int) (p : Expr) : GoalM Unit := do
-  trace[Meta.debug] "unsat #{u}-({k})->#{v}"
-  modify' fun s => { s with
-    unsat := p -- TODO
-  }
+private def setUnsat (u v : NodeId) (kuv : Int) (huv : Expr) (kvu : Int) : GoalM Unit := do
+  assert! kuv + kvu < 0
+  let hvu ← extractProof v u
+  let u := (← get').nodes[u]!
+  let v := (← get').nodes[v]!
+  if kuv == 0 then
+    assert! kvu < 0
+    closeGoal (mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) u v (toExpr (-kvu).toNat) rfl_true huv hvu)
+  else if kvu == 0 then
+    assert! kuv < 0
+    closeGoal (mkApp6 (mkConst ``Grind.Nat.unsat_le_lo) v u (toExpr (-kuv).toNat) rfl_true hvu huv)
+  else if kuv < 0 then
+    if kvu > 0 then
+      closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) u v (toExpr (-kuv).toNat) (toExpr kvu.toNat) rfl_true huv hvu)
+    else
+      assert! kvu < 0
+      closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_lo) u v (toExpr (-kuv).toNat) (toExpr (-kvu).toNat) rfl_true huv hvu)
+  else
+    assert! kuv > 0 && kvu < 0
+    closeGoal (mkApp7 (mkConst ``Grind.Nat.unsat_lo_ro) v u (toExpr (-kvu).toNat) (toExpr kuv.toNat) rfl_true hvu huv)
 
 private def setDist (u v : NodeId) (k : Int) : GoalM Unit := do
   trace[grind.offset.dist] "{({ a := u, b := v, k : Cnstr NodeId})}"
@@ -107,10 +119,10 @@ private def updateIfShorter (u v : NodeId) (k : Int) (w : NodeId) : GoalM Unit :
     setProof u v (← getProof? w v).get!
 
 def addEdge (u : NodeId) (v : NodeId) (k : Int) (p : Expr) : GoalM Unit := do
-  if (← isUnsat) then return ()
+  if (← isInconsistent) then return ()
   if let some k' ← getDist? v u then
     if k'+k < 0 then
-      setUnsat u v k p
+      setUnsat u v k p k'
       return ()
   if (← isShorter u v k) then
     setDist u v k

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

@@ -46,7 +46,6 @@ structure State where
   the last edge.
   -/
   proofs  : PArray (AssocList NodeId ProofInfo) := {}
-  unsat   : Option Expr := none
   deriving Inhabited
 
 end Offset

tests/lean/run/grind_offset_cnstr.lean

@@ -242,3 +242,17 @@ set_option trace.grind.offset.dist true in
 example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 1 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
   fail_if_success grind
   sorry
+
+
+example (a b : Nat) : a ≤ b → b + 2 ≤ c → a + 1 ≤ c := by
+  grind
+example (a b : Nat) : a ≤ b → b ≤ c → a ≤ c := by
+  grind
+example (a b : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 2 ≤ c := by
+  grind
+example (a b : Nat) : a + 1 ≤ b → b + 1 ≤ c → a + 1 ≤ c := by
+  grind
+example (a b : Nat) : a + 1 ≤ b → b ≤ c + 2 → a ≤ c + 1 := by
+  grind
+example (a b : Nat) : a + 2 ≤ b → b ≤ c + 2 → a ≤ c := by
+  grind