wip

src/Init/Grind/Module/Basic.lean

@@ -44,6 +44,33 @@ variable {M : Type u} [NatModule M]
 theorem zero_add (a : M) : 0 + a = a := by
   rw [add_comm, add_zero]
 
+abbrev PreEnvelope (M : Type u) [NatModule M] : Type u := M × M
+instance setoid (M : Type u) [NatModule M] : Setoid (PreEnvelope M) where
+  r x y := x.1 + y.2 = x.2 + y.1
+  iseqv := sorry
+
+abbrev Envelope (M : Type u) [NatModule M] : Type u := Quotient (setoid M)
+
+instance : IntModule (Envelope M) where
+  zero := Quotient.mk' ((0 : M), (0 : M))
+  add := Quotient.lift₂ (fun (a, b) (c, d) => Quotient.mk' (a + c, b + d)) sorry
+  neg := Quotient.lift (fun (a, b) => Quotient.mk' (b, a)) sorry
+  sub := Quotient.lift₂ (fun (a, b) (c, d) => Quotient.mk' (a + d, b + c)) sorry
+  hMul
+  | (i : Nat) => Quotient.lift (fun (a, b) => Quotient.mk' (i * a, i * b)) sorry
+  | -(i + 1 : Nat) => Quotient.lift (fun (a, b) => Quotient.mk' ((i + 1) * b, (i + 1) * a)) sorry
+  add_zero := sorry
+  add_comm := sorry
+  add_assoc := sorry
+  neg_add_cancel := sorry
+  sub_eq_add_neg := sorry
+  zero_hmul := sorry
+  add_hmul := sorry
+  one_hmul := sorry
+  mul_hmul := sorry
+  hmul_zero := sorry
+  hmul_add := sorry
+
 end NatModule
 
 namespace IntModule

src/Init/Grind/Ordered/Module.lean

@@ -23,6 +23,19 @@ class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where
   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
+
+variable {M : Type u} [Preorder M] [NatModule M]
+
+instance : Preorder (Envelope M) where
+  le := Quotient.lift₂ (fun x y => x.1 + y.2 ≤ y.1 + x.2) sorry
+  lt := Quotient.lift₂ (fun x y => x.1 < y.1) sorry
+  le_refl := sorry
+  le_trans := sorry
+  lt_iff_le_not_le := sorry
+
+end NatModule
+
 namespace NatModule.IsOrdered
 
 variable {M : Type u} [Preorder M] [NatModule M] [NatModule.IsOrdered M]