From b73b8a7edfce18b2271609ebec3a21f52de27b20 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Tue, 23 Sep 2025 20:01:19 -0700
Subject: [PATCH] feat: helper ordered ring theorems (#10529)

This PR adds some helper theorems for the upcoming `grind order` solver.
---
 src/Init/Grind/Ordered/Ring.lean | 80 ++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)

diff --git a/src/Init/Grind/Ordered/Ring.lean b/src/Init/Grind/Ordered/Ring.lean
index 9edd50d9f8..ad634de03f 100644
--- a/src/Init/Grind/Ordered/Ring.lean
+++ b/src/Init/Grind/Ordered/Ring.lean
@@ -53,6 +53,86 @@ theorem ofNat_nonneg (x : Nat) : (OfNat.ofNat x : R) ≥ 0 := by
     have := Preorder.lt_of_lt_of_le this ih
     exact Preorder.le_of_lt this
 
+attribute [local instance] Semiring.natCast Ring.intCast
+
+theorem le_of_natCast_le_natCast (a b : Nat) : (a : R) ≤ (b : R) → a ≤ b := by
+  induction a generalizing b <;> cases b <;> simp
+  next n ih =>
+    simp [Semiring.natCast_succ, Semiring.natCast_zero]
+    intro h
+    have : (n:R) ≤ 0 := by
+      have := OrderedRing.zero_lt_one (R := R)
+      replace this := OrderedAdd.add_le_right (M := R) (n:R) (Std.le_of_lt this)
+      rw [Semiring.add_zero] at this
+      exact Std.IsPreorder.le_trans _ _ _ this h
+    replace ih := ih 0
+    simp [Semiring.natCast_zero] at ih
+    replace ih := ih this
+    subst n
+    clear this
+    have := OrderedRing.zero_lt_one (R := R)
+    rw [Semiring.natCast_zero, Semiring.add_comm, Semiring.add_zero] at h
+    replace this := Std.lt_of_lt_of_le this h
+    have := Preorder.lt_irrefl (0:R)
+    contradiction
+  next ih m =>
+    simp [Semiring.natCast_succ]
+    intro h
+    have := OrderedAdd.add_le_left_iff _ |>.mpr h
+    exact ih _ this
+
+theorem le_of_intCast_le_intCast (a b : Int) : (a : R) ≤ (b : R) → a ≤ b := by
+  intro h
+  replace h := OrderedAdd.sub_nonneg_iff.mpr h
+  rw [← Ring.intCast_sub] at h
+  suffices 0 ≤ b - a by omega
+  revert h
+  generalize b - a = x
+  cases x <;> simp [Ring.intCast_natCast, Int.negSucc_eq, Ring.intCast_neg, Ring.intCast_add]
+  intro h
+  replace h := OrderedAdd.neg_nonneg_iff.mp h
+  rw [Ring.intCast_one, ← Semiring.natCast_one, ← Semiring.natCast_add, ← Semiring.natCast_zero] at h
+  replace h := le_of_natCast_le_natCast _ _ h
+  omega
+
+theorem lt_of_natCast_lt_natCast (a b : Nat) : (a : R) < (b : R) → a < b := by
+  induction a generalizing b <;> cases b <;> simp
+  next =>
+    simp [Semiring.natCast_zero]
+    exact Preorder.lt_irrefl (0:R)
+  next n ih =>
+    simp [Semiring.natCast_succ, Semiring.natCast_zero]
+    intro h
+    have : (n:R) < 0 := by
+      have := OrderedRing.zero_lt_one (R := R)
+      replace this := OrderedAdd.add_le_right (M := R) (n:R) (Std.le_of_lt this)
+      rw [Semiring.add_zero] at this
+      exact Std.lt_of_le_of_lt this h
+    replace ih := ih 0
+    simp [Semiring.natCast_zero] at ih
+    exact ih this
+  next ih m =>
+    simp [Semiring.natCast_succ]
+    intro h
+    have := OrderedAdd.add_lt_left_iff _ |>.mpr h
+    exact ih _ this
+
+theorem lt_of_intCast_lt_intCast (a b : Int) : (a : R) < (b : R) → a < b := by
+  intro h
+  replace h := OrderedAdd.sub_pos_iff.mpr h
+  rw [← Ring.intCast_sub] at h
+  suffices 0 < b - a by omega
+  revert h
+  generalize b - a = x
+  cases x <;> simp [Ring.intCast_natCast, Int.negSucc_eq, Ring.intCast_neg, Ring.intCast_add]
+  next => intro h; rw [← Semiring.natCast_zero] at h; exact lt_of_natCast_lt_natCast _ _ h
+  next =>
+    intro h
+    replace h := OrderedAdd.neg_pos_iff.mp h
+    rw [Ring.intCast_one, ← Semiring.natCast_one, ← Semiring.natCast_add, ← Semiring.natCast_zero] at h
+    replace h := lt_of_natCast_lt_natCast _ _ h
+    omega
+
 instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] :
     IsCharP R 0 := IsCharP.mk' _ _ <| by
   intro x