feat: basic theory of ordered modules over Nat (#8809)

This PR introduces the basic theory of ordered modules over Nat (i.e.
without subtraction), for `grind`. We'll solve problems here by
embedding them in the `IntModule` envelope.

src/Init/Grind/Module/Basic.lean

@@ -37,6 +37,15 @@ class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M w
   neg_add_cancel : ∀ a : M, -a + a = 0
   sub_eq_add_neg : ∀ a b : M, a - b = a + -b
 
+namespace NatModule
+
+variable {M : Type u} [NatModule M]
+
+theorem zero_add (a : M) : 0 + a = a := by
+  rw [add_comm, add_zero]
+
+end NatModule
+
 namespace IntModule
 
 attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul

src/Init/Grind/Ordered/Module.lean

@@ -12,12 +12,57 @@ import Init.Grind.Ordered.Order
 
 namespace Lean.Grind
 
+class NatModule.IsOrdered (M : Type u) [Preorder M] [NatModule M] where
+  add_le_left_iff : ∀ {a b : M} (c : M), a ≤ b ↔ a + c ≤ b + c
+  hmul_pos : ∀ (k : Nat) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
+  hmul_nonneg : ∀ {k : Nat} {a : M}, 0 ≤ a → 0 ≤ k * a
+
 class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
   neg_le_iff : ∀ a b : M, -a ≤ b ↔ -b ≤ a
   add_le_left : ∀ {a b : M}, a ≤ b → (c : M) → a + c ≤ b + c
   hmul_pos : ∀ (k : Int) {a : M}, 0 < a → (0 < k ↔ 0 < k * a)
   hmul_nonneg : ∀ {k : Int} {a : M}, 0 ≤ k → 0 ≤ a → 0 ≤ k * a
 
+namespace NatModule.IsOrdered
+
+variable {M : Type u} [Preorder M] [NatModule M] [NatModule.IsOrdered M]
+
+theorem add_le_right_iff {a b : M} (c : M) : a ≤ b ↔ c + a ≤ c + b := by
+  rw [add_comm c a, add_comm c b,add_le_left_iff]
+
+theorem add_le_left {a b : M} (h : a ≤ b) (c : M) : a + c ≤ b + c :=
+  (add_le_left_iff c).mp h
+
+theorem add_le_right {a b : M} (h : a ≤ b) (c : M) : c + a ≤ c + b :=
+  (add_le_right_iff c).mp h
+
+theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
+  simp only [Preorder.lt_iff_le_not_le] at h ⊢
+  constructor
+  · exact add_le_left h.1 _
+  · intro w
+    apply h.2
+    exact (add_le_left_iff c).mpr w
+
+theorem add_lt_right {a b : M} (h : a < b) (c : M) : c + a < c + b := by
+  rw [add_comm c a, add_comm c b]
+  exact add_lt_left h c
+
+theorem add_lt_left_iff {a b : M} (c : M) : a < b ↔ a + c < b + c := by
+  constructor
+  · exact fun h => add_lt_left h c
+  · intro w
+    simp only [Preorder.lt_iff_le_not_le] at w ⊢
+    constructor
+    · exact (add_le_left_iff c).mpr w.1
+    · intro h
+      exact w.2 ((add_le_left_iff c).mp h)
+
+theorem add_lt_right_iff {a b : M} (c : M) : a < b ↔ c + a < c + b := by
+  rw [add_comm c a, add_comm c b, add_lt_left_iff]
+
+end NatModule.IsOrdered
+
 namespace IntModule.IsOrdered
 
 variable {M : Type u} [Preorder M] [IntModule M] [IntModule.IsOrdered M]
@@ -41,7 +86,7 @@ theorem neg_pos_iff {a : M} : 0 < -a ↔ a < 0 := by
   rw [lt_neg_iff, neg_zero]
 
 theorem add_lt_left {a b : M} (h : a < b) (c : M) : a + c < b + c := by
-  simp [Preorder.lt_iff_le_not_le] at h ⊢
+  simp only [Preorder.lt_iff_le_not_le] at h ⊢
   constructor
   · exact add_le_left h.1 _
   · intro w