From bc21b57396b8bc0d0933b017f92f8b428aedc91a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 20 May 2025 14:22:06 +1000 Subject: [PATCH] chore: use HMul in Lean.Grind.Module (#8414) --- src/Init/Grind/Module/Basic.lean | 54 +++++++++++++++++--------------- src/Init/Grind/Module/Int.lean | 22 ++++++------- 2 files changed, 40 insertions(+), 36 deletions(-) diff --git a/src/Init/Grind/Module/Basic.lean b/src/Init/Grind/Module/Basic.lean index fa0e280deb..3b21e6b895 100644 --- a/src/Init/Grind/Module/Basic.lean +++ b/src/Init/Grind/Module/Basic.lean @@ -10,47 +10,51 @@ import Init.Data.Int.Order namespace Lean.Grind -class NatModule (M : Type u) extends Zero M, Add M, HSMul Nat M M where +class NatModule (M : Type u) extends Zero M, Add M, HMul Nat M M where add_zero : ∀ a : M, a + 0 = a zero_add : ∀ a : M, 0 + a = a add_comm : ∀ a b : M, a + b = b + a add_assoc : ∀ a b c : M, a + b + c = a + (b + c) - zero_smul : ∀ a : M, 0 • a = 0 - one_smul : ∀ a : M, 1 • a = a - add_smul : ∀ n m : Nat, ∀ a : M, (n + m) • a = n • a + m • a - smul_zero : ∀ n : Nat, n • (0 : M) = 0 - smul_add : ∀ n : Nat, ∀ a b : M, n • (a + b) = n • a + n • b - mul_smul : ∀ n m : Nat, ∀ a : M, (n * m) • a = n • (m • a) + zero_hmul : ∀ a : M, 0 * a = 0 + one_hmul : ∀ a : M, 1 * a = a + add_hmul : ∀ n m : Nat, ∀ a : M, (n + m) * a = n * a + m * a + hmul_zero : ∀ n : Nat, n * (0 : M) = 0 + hmul_add : ∀ n : Nat, ∀ a b : M, n * (a + b) = n * a + n * b + mul_hmul : ∀ n m : Nat, ∀ a : M, (n * m) * a = n * (m * a) -class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HSMul Int M M where +attribute [instance 100] NatModule.toZero NatModule.toAdd NatModule.toHMul + +class IntModule (M : Type u) extends Zero M, Add M, Neg M, Sub M, HMul Int M M where add_zero : ∀ a : M, a + 0 = a zero_add : ∀ a : M, 0 + a = a add_comm : ∀ a b : M, a + b = b + a add_assoc : ∀ a b c : M, a + b + c = a + (b + c) - zero_smul : ∀ a : M, (0 : Int) • a = 0 - one_smul : ∀ a : M, (1 : Int) • a = a - add_smul : ∀ n m : Int, ∀ a : M, (n + m) • a = n • a + m • a - neg_smul : ∀ n : Int, ∀ a : M, (-n) • a = - (n • a) - smul_zero : ∀ n : Int, n • (0 : M) = 0 - smul_add : ∀ n : Int, ∀ a b : M, n • (a + b) = n • a + n • b - mul_smul : ∀ n m : Int, ∀ a : M, (n * m) • a = n • (m • a) + zero_hmul : ∀ a : M, (0 : Int) * a = 0 + one_hmul : ∀ a : M, (1 : Int) * a = a + add_hmul : ∀ n m : Int, ∀ a : M, (n + m) * a = n * a + m * a + neg_hmul : ∀ n : Int, ∀ a : M, (-n) * a = - (n * a) + hmul_zero : ∀ n : Int, n * (0 : M) = 0 + hmul_add : ∀ n : Int, ∀ a b : M, n * (a + b) = n * a + n * b + mul_hmul : ∀ n m : Int, ∀ a : M, (n * m) * a = n * (m * a) neg_add_cancel : ∀ a : M, -a + a = 0 sub_eq_add_neg : ∀ a b : M, a - b = a + -b +attribute [instance 100] IntModule.toZero IntModule.toAdd IntModule.toNeg IntModule.toSub IntModule.toHMul + instance IntModule.toNatModule (M : Type u) [i : IntModule M] : NatModule M := { i with - hSMul a x := (a : Int) • x - smul_zero := by simp [IntModule.smul_zero] - add_smul := by simp [IntModule.add_smul] - smul_add := by simp [IntModule.smul_add] - mul_smul := by simp [IntModule.mul_smul] } + hMul a x := (a : Int) * x + hmul_zero := by simp [IntModule.hmul_zero] + add_hmul := by simp [IntModule.add_hmul] + hmul_add := by simp [IntModule.hmul_add] + mul_hmul := by simp [IntModule.mul_hmul] } /-- We keep track of rational linear combinations as integer linear combinations, but with the assurance that we can cancel the GCD of the coefficients. -/ class RatModule (M : Type u) extends IntModule M where - no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k • a = 0 → a = 0 + no_int_zero_divisors : ∀ (k : Int) (a : M), k ≠ 0 → k * a = 0 → a = 0 /-- A preorder is a reflexive, transitive relation `≤` with `a < b` defined in the obvious way. -/ class Preorder (α : Type u) extends LE α, LT α where @@ -64,9 +68,9 @@ class IntModule.IsOrdered (M : Type u) [Preorder M] [IntModule M] where neg_lt_iff : ∀ a b : M, -a < b ↔ -b < a add_lt_left : ∀ a b c : M, a < b → a + c < b + c add_lt_right : ∀ a b c : M, a < b → c + a < c + b - smul_pos : ∀ (k : Int) (a : M), 0 < a → (0 < k ↔ 0 < k • a) - smul_neg : ∀ (k : Int) (a : M), a < 0 → (0 < k ↔ k • a < 0) - smul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k • a - smul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k • a ≤ 0 + hmul_pos : ∀ (k : Int) (a : M), 0 < a → (0 < k ↔ 0 < k * a) + hmul_neg : ∀ (k : Int) (a : M), a < 0 → (0 < k ↔ k * a < 0) + hmul_nonneg : ∀ (k : Int) (a : M), 0 ≤ a → 0 ≤ k → 0 ≤ k * a + hmul_nonpos : ∀ (k : Int) (a : M), a ≤ 0 → 0 ≤ k → k * a ≤ 0 end Lean.Grind diff --git a/src/Init/Grind/Module/Int.lean b/src/Init/Grind/Module/Int.lean index ef450e1f4f..628546983a 100644 --- a/src/Init/Grind/Module/Int.lean +++ b/src/Init/Grind/Module/Int.lean @@ -20,13 +20,13 @@ instance : IntModule Int where zero_add := Int.zero_add add_comm := Int.add_comm add_assoc := Int.add_assoc - zero_smul := Int.zero_mul - one_smul := Int.one_mul - add_smul := Int.add_mul - neg_smul := Int.neg_mul - smul_zero := Int.mul_zero - smul_add := Int.mul_add - mul_smul := Int.mul_assoc + zero_hmul := Int.zero_mul + one_hmul := Int.one_mul + add_hmul := Int.add_mul + neg_hmul := Int.neg_mul + hmul_zero := Int.mul_zero + hmul_add := Int.mul_add + mul_hmul := Int.mul_assoc neg_add_cancel := Int.add_left_neg sub_eq_add_neg _ _ := Int.sub_eq_add_neg @@ -40,9 +40,9 @@ instance : IntModule.IsOrdered Int where neg_lt_iff := by omega add_lt_left := by omega add_lt_right := by omega - smul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩ - smul_neg k a ha := ⟨fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha⟩ - smul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha - smul_nonneg k a ha hk := Int.mul_nonneg hk ha + hmul_pos k a ha := ⟨fun hk => Int.mul_pos hk ha, fun h => Int.pos_of_mul_pos_left h ha⟩ + hmul_neg k a ha := ⟨fun hk => Int.mul_neg_of_pos_of_neg hk ha, fun h => Int.pos_of_mul_neg_left h ha⟩ + hmul_nonpos k a ha hk := Int.mul_nonpos_of_nonneg_of_nonpos hk ha + hmul_nonneg k a ha hk := Int.mul_nonneg hk ha end Lean.Grind