fix: bugs and add more tests

src/Init/Grind/Offset.lean

@@ -71,13 +71,13 @@ They are variants of the theorems for closing a goal.
 -/
 theorem Nat.lo_eq_false_of_le (u v k : Nat) : isLt 0 k = true → u ≤ v → (v + k ≤ u) = False := by
  simp [isLt]; omega
-theorem Nat.le_eq_false_of_lo (u v k : Nat) : isLt 0 k = true → v + k ≤ u → (u ≤ v) = False := by
+theorem Nat.le_eq_false_of_lo (u v k : Nat) : isLt 0 k = true → u + k ≤ v → (v ≤ u) = False := by
  simp [isLt]; omega
 theorem Nat.lo_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true → u + k₁ ≤ v → (v + k₂ ≤ u) = False := by
   simp [isLt]; omega
 theorem Nat.ro_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → (v ≤ u + k₂) = False := by
   simp [isLt]; omega
-theorem Nat.lo_eq_false_of_ro (u v k₁ k₂ : Nat) : isLt k₁ k₂ = true → v ≤ u + k₁ → (u + k₂ ≤ v) = False := by
+theorem Nat.lo_eq_false_of_ro (u v k₁ k₂ : Nat) : isLt k₁ k₂ = true → u ≤ v + k₁ → (v + k₂ ≤ u) = False := by
   simp [isLt]; omega
 
 end Lean.Grind

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

@@ -19,7 +19,9 @@ namespace Offset
 /-- Returns a proof for `true = true` -/
 def rfl_true : Expr := mkConst ``Grind.rfl_true
 
-private def toExprN (n : Int) := toExpr n.toNat
+private def toExprN (n : Int) :=
+  assert! n >= 0
+  toExpr n.toNat
 
 open Lean.Grind in
 /--
@@ -143,6 +145,7 @@ s.t. `k+k' < 0`
 def mkPropagateEqFalseProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Expr :=
   if k == 0 then
     assert! k' < 0
+    let k' := -k'
     mkApp5 (mkConst ``Grind.Nat.lo_eq_false_of_le) u v (toExprN k') rfl_true huv
   else if k < 0 then
     let k := -k
@@ -153,10 +156,11 @@ def mkPropagateEqFalseProof (u v : Expr) (k : Int) (huv : Expr) (k' : Int) : Exp
       mkApp6 (mkConst ``Grind.Nat.lo_eq_false_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
     else
       assert! k' > 0
-      mkApp6 (mkConst ``Grind.Nat.ro_eq_true_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
+      mkApp6 (mkConst ``Grind.Nat.ro_eq_false_of_lo) u v (toExprN k) (toExprN k') rfl_true huv
   else
     assert! k > 0
     assert! k' < 0
+    let k' := -k'
     mkApp6 (mkConst ``Grind.Nat.lo_eq_false_of_ro) u v (toExprN k) (toExprN k') rfl_true huv
 
 end Offset

tests/lean/run/grind_offset_cnstr.lean

@@ -276,6 +276,8 @@ fun {a4} p a1 a2 a3 =>
 open Lean Grind in
 #print ex1
 
+/-! Propagate `cnstr = False` tests -/
+
 -- The following example is solved by `grind` using constraint propagation and 0 case-splits.
 #guard_msgs (info) in
 set_option trace.grind.split true in
@@ -293,3 +295,60 @@ example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c → (a ≤ c ↔ p) → (
 set_option trace.grind.split true in
 example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c + 1 → (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → p ∧ q := by
   grind (splits := 0)
+
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → ¬p ∧ ¬r ∧ ¬s := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c → (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → ¬p ∧ ¬r := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p r : Prop) (a b : Nat) : a  ≤ b → b ≤ c + 3 → (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → ¬p ∧ ¬r := by
+  grind (splits := 0)
+
+/-! Propagate `cnstr = False` tests, but with different internalization order -/
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p q : Prop) (a b : Nat) : (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → a ≤ b → b ≤ c → p ∧ q := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p q : Prop) (a b : Nat) : (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → a ≤ b → b ≤ c + 1 → p ∧ q := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p r s : Prop) (a b : Nat) : (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → a ≤ b → b + 2 ≤ c → ¬p ∧ ¬r ∧ ¬s := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p r : Prop) (a b : Nat) : (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → a ≤ b → b ≤ c → ¬p ∧ ¬r := by
+  grind (splits := 0)
+
+-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
+#guard_msgs (info) in
+set_option trace.grind.split true in
+example (p r : Prop) (a b : Nat) : (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → a ≤ b → b ≤ c + 3 → ¬p ∧ ¬r := by
+  grind (splits := 0)