chore: omega notices that 0 ≤ (x : Int) % (y : Int) (#3736)

src/Init/Omega/Int.lean

@@ -50,6 +50,9 @@ theorem ofNat_shiftLeft_eq {x y : Nat} : (x <<< y : Int) = (x : Int) * (2 ^ y :
 theorem ofNat_shiftRight_eq_div_pow {x y : Nat} : (x >>> y : Int) = (x : Int) / (2 ^ y : Nat) := by
   simp only [Nat.shiftRight_eq_div_pow, Int.ofNat_ediv]
 
+theorem emod_ofNat_nonneg {x : Nat} {y : Int} : 0 ≤ (x : Int) % y :=
+  Int.ofNat_zero_le _
+
 -- FIXME these are insane:
 theorem lt_of_not_ge {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h
 theorem lt_of_not_le {x y : Int} (h : ¬ (x ≤ y)) : y < x := Int.not_le.mp h

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -218,7 +218,12 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
             (mkApp3 (.const ``Int.emod_nonneg []) x k
                 (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) cast_pos)) |>.insert
               (mkApp3 (.const ``Int.emod_lt_of_pos []) x k cast_pos)
-      | _ => pure ∅
+      | _ =>  match x.getAppFnArgs with
+        | (``Nat.cast, #[.const ``Int [], _, x']) =>
+          -- Since we push coercions inside `%`, we need to record here that
+          -- `(x : Int) % (y : Int)` is non-negative.
+          pure <| HashSet.empty.insert (mkApp2 (.const ``Int.emod_ofNat_nonneg []) x' k)
+        | _ => pure ∅
     | _ => pure ∅
   | (``Min.min, #[_, _, x, y]) =>
     pure <| HashSet.empty.insert (mkApp2 (.const ``Int.min_le_left []) x y) |>.insert

tests/lean/run/omega.lean

@@ -24,7 +24,7 @@ example {x : Int} : x / 2 + x / (-2) = 0 := by omega
 
 example {x : Nat} (_ : x ≠ 0) : 0 < x := by omega
 
-example {x y z : Nat} (_ : a ≤ c) (_ : b ≤ c) : a < Nat.succ c := by omega
+example (_ : a ≤ c) (_ : b ≤ c) : a < Nat.succ c := by omega
 
 example (_ : 7 < 3) : False := by omega
 example (_ : 0 < 0) : False := by omega
@@ -374,6 +374,9 @@ example (i j : Nat) (p : i ≥ j) : True := by
   have _ : i ≥ k := by omega
   trivial
 
+-- From https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Nat.2Emul_sub_mod/near/428107094
+example (a b : Nat) (h : a % b + 1 = 0) : False := by omega
+
 /-! ### Fin -/