From 8154aaa1b3fba27f4880e1d9148042c467e13813 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 15 May 2025 19:25:57 +0800 Subject: [PATCH] feat: preparation for semirings and noncommutative rings in grind (#8343) This PR splits `Lean.Grind.CommRing` into 4 typeclasses, for semirings and noncommutative rings. This does not yet change the behaviour of `grind`, which expects to find all 4 typeclasses. Later we will make some generalizations. --- src/Init/Data/BitVec/Lemmas.lean | 4 + src/Init/Grind/CommRing/Basic.lean | 95 ++++++++++++------- src/Init/Grind/CommRing/BitVec.lean | 3 + src/Init/Grind/CommRing/Int.lean | 3 + src/Init/Grind/CommRing/Poly.lean | 2 + src/Init/Grind/CommRing/SInt.lean | 15 +++ src/Init/Grind/CommRing/UInt.lean | 15 +++ .../Grind/Arith/CommRing/DenoteExpr.lean | 2 +- .../Tactic/Grind/Arith/CommRing/RingId.lean | 72 +++++++------- .../Tactic/Grind/Arith/CommRing/Types.lean | 6 ++ tests/lean/run/infoFromFailure.lean | 40 +++++++- 11 files changed, 184 insertions(+), 73 deletions(-) diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 9fcb809103..6171ebda51 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -3731,6 +3731,10 @@ theorem mul_add {x y z : BitVec w} : rw [Nat.mul_mod, Nat.mod_mod (y.toNat + z.toNat), ← Nat.mul_mod, Nat.mul_add] +theorem add_mul {x y z : BitVec w} : + (x + y) * z = x * z + y * z := by + rw [BitVec.mul_comm, mul_add, BitVec.mul_comm z, BitVec.mul_comm z] + theorem mul_succ {x y : BitVec w} : x * (y + 1#w) = x * y + x := by simp [mul_add] theorem succ_mul {x y : BitVec w} : (x + 1#w) * y = x * y + y := by simp [BitVec.mul_comm, BitVec.mul_add] diff --git a/src/Init/Grind/CommRing/Basic.lean b/src/Init/Grind/CommRing/Basic.lean index 746c24b1a1..4607bce615 100644 --- a/src/Init/Grind/CommRing/Basic.lean +++ b/src/Init/Grind/CommRing/Basic.lean @@ -30,39 +30,51 @@ theorem ofNat_eq_iff_of_lt {x y : Nat} (h₁ : x < p) (h₂ : y < p) : namespace Lean.Grind -class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat α where +class Semiring (α : Type u) extends Add α, Mul α, HPow α Nat α where [ofNat : ∀ n, OfNat α n] [natCast : NatCast α] - [intCast : IntCast α] add_assoc : ∀ a b c : α, a + b + c = a + (b + c) add_comm : ∀ a b : α, a + b = b + a add_zero : ∀ a : α, a + 0 = a - neg_add_cancel : ∀ a : α, -a + a = 0 mul_assoc : ∀ a b c : α, a * b * c = a * (b * c) - mul_comm : ∀ a b : α, a * b = b * a mul_one : ∀ a : α, a * 1 = a + one_mul : ∀ a : α, 1 * a = a left_distrib : ∀ a b c : α, a * (b + c) = a * b + a * c + right_distrib : ∀ a b c : α, (a + b) * c = a * c + b * c zero_mul : ∀ a : α, 0 * a = 0 - sub_eq_add_neg : ∀ a b : α, a - b = a + -b + mul_zero : ∀ a : α, a * 0 = 0 pow_zero : ∀ a : α, a ^ 0 = 1 pow_succ : ∀ a : α, ∀ n : Nat, a ^ (n + 1) = (a ^ n) * a ofNat_succ : ∀ a : Nat, OfNat.ofNat (α := α) (a + 1) = OfNat.ofNat a + 1 := by intros; rfl ofNat_eq_natCast : ∀ n : Nat, OfNat.ofNat (α := α) n = Nat.cast n := by intros; rfl + +class Ring (α : Type u) extends Semiring α, Neg α, Sub α where + [intCast : IntCast α] + neg_add_cancel : ∀ a : α, -a + a = 0 + sub_eq_add_neg : ∀ a b : α, a - b = a + -b intCast_ofNat : ∀ n : Nat, Int.cast (OfNat.ofNat (α := Int) n) = OfNat.ofNat (α := α) n := by intros; rfl intCast_neg : ∀ i : Int, Int.cast (R := α) (-i) = -Int.cast i := by intros; rfl +class CommSemiring (α : Type u) extends Semiring α where + mul_comm : ∀ a b : α, a * b = b * a + one_mul := by intro a; rw [mul_comm, mul_one] + mul_zero := by intro a; rw [mul_comm, zero_mul] + right_distrib := by intro a b c; rw [mul_comm, left_distrib, mul_comm c, mul_comm c] + +class CommRing (α : Type u) extends Ring α, CommSemiring α + -- We reduce the priority of these parent instances, -- so that in downstream libraries with their own `CommRing` class, -- the path `CommRing -> Add` is found before `CommRing -> Lean.Grind.CommRing -> Add`. -- (And similarly for the other parents.) -attribute [instance 100] CommRing.toAdd CommRing.toMul CommRing.toNeg CommRing.toSub CommRing.toHPow +attribute [instance 100] Semiring.toAdd Semiring.toMul Semiring.toHPow Ring.toNeg Ring.toSub -- This is a low-priority instance, to avoid conflicts with existing `OfNat`, `NatCast`, and `IntCast` instances. -attribute [instance 100] CommRing.ofNat CommRing.natCast CommRing.intCast +attribute [instance 100] Semiring.ofNat Semiring.natCast Ring.intCast -namespace CommRing +namespace Semiring -variable {α : Type u} [CommRing α] +variable {α : Type u} [Semiring α] theorem natCast_zero : ((0 : Nat) : α) = 0 := (ofNat_eq_natCast 0).symm theorem natCast_one : ((1 : Nat) : α) = 1 := (ofNat_eq_natCast 1).symm @@ -80,24 +92,9 @@ theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by theorem zero_add (a : α) : 0 + a = a := by rw [add_comm, add_zero] -theorem add_neg_cancel (a : α) : a + -a = 0 := by - rw [add_comm, neg_add_cancel] - theorem add_left_comm (a b c : α) : a + (b + c) = b + (a + c) := by rw [← add_assoc, ← add_assoc, add_comm a] -theorem one_mul (a : α) : 1 * a = a := by - rw [mul_comm, mul_one] - -theorem right_distrib (a b c : α) : (a + b) * c = a * c + b * c := by - rw [mul_comm, left_distrib, mul_comm c, mul_comm c] - -theorem mul_zero (a : α) : a * 0 = 0 := by - rw [mul_comm, zero_mul] - -theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by - rw [← mul_assoc, ← mul_assoc, mul_comm a] - theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * OfNat.ofNat b := by induction b with | zero => simp [Nat.mul_zero, mul_zero] @@ -106,6 +103,22 @@ theorem ofNat_mul (a b : Nat) : OfNat.ofNat (α := α) (a * b) = OfNat.ofNat a * theorem natCast_mul (a b : Nat) : ((a * b : Nat) : α) = ((a : α) * (b : α)) := by rw [← ofNat_eq_natCast, ofNat_mul, ofNat_eq_natCast, ofNat_eq_natCast] +theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ := by + induction k₂ + next => simp [pow_zero, mul_one] + next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc] + +end Semiring + +namespace Ring + +open Semiring + +variable {α : Type u} [Ring α] + +theorem add_neg_cancel (a : α) : a + -a = 0 := by + rw [add_comm, neg_add_cancel] + theorem add_left_inj {a b : α} (c : α) : a + c = b + c ↔ a = b := ⟨fun h => by simpa [add_assoc, add_neg_cancel, add_zero] using (congrArg (· + -c) h), fun g => congrArg (· + c) g⟩ @@ -198,11 +211,17 @@ theorem neg_eq_neg_one_mul (a : α) : -a = (-1) * a := by rw [← right_distrib, ← intCast_neg_one, ← intCast_one (α := α)] simp [← intCast_add, intCast_zero, zero_mul] +theorem neg_eq_mul_neg_one (a : α) : -a = a * (-1) := by + rw [← add_left_inj a, neg_add_cancel] + conv => rhs; arg 2; rw [← mul_one a] + rw [← left_distrib, ← intCast_neg_one, ← intCast_one (α := α)] + simp [← intCast_add, intCast_zero, mul_zero] + theorem neg_mul (a b : α) : (-a) * b = -(a * b) := by rw [neg_eq_neg_one_mul a, neg_eq_neg_one_mul (a * b), mul_assoc] theorem mul_neg (a b : α) : a * (-b) = -(a * b) := by - rw [mul_comm, neg_mul, mul_comm] + rw [neg_eq_mul_neg_one b, neg_eq_mul_neg_one (a * b), mul_assoc] theorem intCast_nat_mul (x y : Nat) : ((x * y : Int) : α) = ((x : α) * (y : α)) := by rw [Int.ofNat_mul_ofNat, intCast_natCast, natCast_mul] @@ -224,21 +243,27 @@ theorem intCast_pow (x : Int) (k : Nat) : ((x ^ k : Int) : α) = (x : α) ^ k := next => simp [pow_zero, Int.pow_zero, intCast_one] next k ih => simp [pow_succ, Int.pow_succ, intCast_mul, *] -theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂ := by - induction k₂ - next => simp [pow_zero, mul_one] - next k₂ ih => rw [Nat.add_succ, pow_succ, pow_succ, ih, mul_assoc] +end Ring -end CommRing +namespace CommSemiring -open CommRing +open Semiring -class IsCharP (α : Type u) [CommRing α] (p : outParam Nat) where +variable {α : Type u} [CommSemiring α] + +theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by + rw [← mul_assoc, ← mul_assoc, mul_comm a] + +end CommSemiring + +open Semiring Ring CommSemiring CommRing + +class IsCharP (α : Type u) [Ring α] (p : outParam Nat) where ofNat_eq_zero_iff (p) : ∀ (x : Nat), OfNat.ofNat (α := α) x = 0 ↔ x % p = 0 namespace IsCharP -variable (p) {α : Type u} [CommRing α] [IsCharP α p] +variable (p) {α : Type u} [Ring α] [IsCharP α p] theorem natCast_eq_zero_iff (x : Nat) : (x : α) = 0 ↔ x % p = 0 := by rw [← ofNat_eq_natCast] @@ -325,12 +350,12 @@ end IsCharP /-- Special case of Mathlib's `NoZeroSMulDivisors Nat α`. -/ -class NoNatZeroDivisors (α : Type u) [CommRing α] where +class NoNatZeroDivisors (α : Type u) [Ring α] where no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0 export NoNatZeroDivisors (no_nat_zero_divisors) -theorem no_int_zero_divisors {α : Type u} [CommRing α] [NoNatZeroDivisors α] {k : Int} {a : α} +theorem no_int_zero_divisors {α : Type u} [Ring α] [NoNatZeroDivisors α] {k : Int} {a : α} : k ≠ 0 → k * a = 0 → a = 0 := by match k with | (k : Nat) => diff --git a/src/Init/Grind/CommRing/BitVec.lean b/src/Init/Grind/CommRing/BitVec.lean index 8bb889b953..e853c0fff5 100644 --- a/src/Init/Grind/CommRing/BitVec.lean +++ b/src/Init/Grind/CommRing/BitVec.lean @@ -19,8 +19,11 @@ instance : CommRing (BitVec w) where mul_assoc := BitVec.mul_assoc mul_comm := BitVec.mul_comm mul_one := BitVec.mul_one + one_mul := BitVec.one_mul left_distrib _ _ _ := BitVec.mul_add + right_distrib _ _ _ := BitVec.add_mul zero_mul _ := BitVec.zero_mul + mul_zero _ := BitVec.mul_zero sub_eq_add_neg := BitVec.sub_eq_add_neg pow_zero _ := BitVec.pow_zero pow_succ _ _ := BitVec.pow_succ diff --git a/src/Init/Grind/CommRing/Int.lean b/src/Init/Grind/CommRing/Int.lean index 5a4c4ac860..915a50d18e 100644 --- a/src/Init/Grind/CommRing/Int.lean +++ b/src/Init/Grind/CommRing/Int.lean @@ -19,8 +19,11 @@ instance : CommRing Int where mul_assoc := Int.mul_assoc mul_comm := Int.mul_comm mul_one := Int.mul_one + one_mul := Int.one_mul left_distrib := Int.mul_add + right_distrib := Int.add_mul zero_mul := Int.zero_mul + mul_zero := Int.mul_zero pow_zero _ := rfl pow_succ _ _ := rfl ofNat_succ _ := rfl diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index 0b5104e524..330c62ab21 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -508,6 +508,8 @@ def NullCert.toPolyC (nc : NullCert) (c : Nat) : Poly := Theorems for justifying the procedure for commutative rings in `grind`. -/ +open Semiring Ring CommSemiring + theorem denoteInt_eq {α} [CommRing α] (k : Int) : denoteInt (α := α) k = k := by simp [denoteInt, cond_eq_if] <;> split next h => rw [ofNat_eq_natCast, ← intCast_natCast, ← intCast_neg, ← Int.eq_neg_natAbs_of_nonpos (Int.le_of_lt h)] diff --git a/src/Init/Grind/CommRing/SInt.lean b/src/Init/Grind/CommRing/SInt.lean index 2b8740f002..f004617e1f 100644 --- a/src/Init/Grind/CommRing/SInt.lean +++ b/src/Init/Grind/CommRing/SInt.lean @@ -25,8 +25,11 @@ instance : CommRing Int8 where mul_assoc := Int8.mul_assoc mul_comm := Int8.mul_comm mul_one := Int8.mul_one + one_mul := Int8.one_mul left_distrib _ _ _ := Int8.mul_add + right_distrib _ _ _ := Int8.add_mul zero_mul _ := Int8.zero_mul + mul_zero _ := Int8.mul_zero sub_eq_add_neg := Int8.sub_eq_add_neg pow_zero := Int8.pow_zero pow_succ := Int8.pow_succ @@ -54,8 +57,11 @@ instance : CommRing Int16 where mul_assoc := Int16.mul_assoc mul_comm := Int16.mul_comm mul_one := Int16.mul_one + one_mul := Int16.one_mul left_distrib _ _ _ := Int16.mul_add + right_distrib _ _ _ := Int16.add_mul zero_mul _ := Int16.zero_mul + mul_zero _ := Int16.mul_zero sub_eq_add_neg := Int16.sub_eq_add_neg pow_zero := Int16.pow_zero pow_succ := Int16.pow_succ @@ -82,8 +88,11 @@ instance : CommRing Int32 where mul_assoc := Int32.mul_assoc mul_comm := Int32.mul_comm mul_one := Int32.mul_one + one_mul := Int32.one_mul left_distrib _ _ _ := Int32.mul_add + right_distrib _ _ _ := Int32.add_mul zero_mul _ := Int32.zero_mul + mul_zero _ := Int32.mul_zero sub_eq_add_neg := Int32.sub_eq_add_neg pow_zero := Int32.pow_zero pow_succ := Int32.pow_succ @@ -110,8 +119,11 @@ instance : CommRing Int64 where mul_assoc := Int64.mul_assoc mul_comm := Int64.mul_comm mul_one := Int64.mul_one + one_mul := Int64.one_mul left_distrib _ _ _ := Int64.mul_add + right_distrib _ _ _ := Int64.add_mul zero_mul _ := Int64.zero_mul + mul_zero _ := Int64.mul_zero sub_eq_add_neg := Int64.sub_eq_add_neg pow_zero := Int64.pow_zero pow_succ := Int64.pow_succ @@ -138,8 +150,11 @@ instance : CommRing ISize where mul_assoc := ISize.mul_assoc mul_comm := ISize.mul_comm mul_one := ISize.mul_one + one_mul := ISize.one_mul left_distrib _ _ _ := ISize.mul_add + right_distrib _ _ _ := ISize.add_mul zero_mul _ := ISize.zero_mul + mul_zero _ := ISize.mul_zero sub_eq_add_neg := ISize.sub_eq_add_neg pow_zero := ISize.pow_zero pow_succ := ISize.pow_succ diff --git a/src/Init/Grind/CommRing/UInt.lean b/src/Init/Grind/CommRing/UInt.lean index 1f6fe6ffcc..691ed10d4f 100644 --- a/src/Init/Grind/CommRing/UInt.lean +++ b/src/Init/Grind/CommRing/UInt.lean @@ -131,8 +131,11 @@ instance : CommRing UInt8 where mul_assoc := UInt8.mul_assoc mul_comm := UInt8.mul_comm mul_one := UInt8.mul_one + one_mul := UInt8.one_mul left_distrib _ _ _ := UInt8.mul_add + right_distrib _ _ _ := UInt8.add_mul zero_mul _ := UInt8.zero_mul + mul_zero _ := UInt8.mul_zero sub_eq_add_neg := UInt8.sub_eq_add_neg pow_zero := UInt8.pow_zero pow_succ := UInt8.pow_succ @@ -153,8 +156,11 @@ instance : CommRing UInt16 where mul_assoc := UInt16.mul_assoc mul_comm := UInt16.mul_comm mul_one := UInt16.mul_one + one_mul := UInt16.one_mul left_distrib _ _ _ := UInt16.mul_add + right_distrib _ _ _ := UInt16.add_mul zero_mul _ := UInt16.zero_mul + mul_zero _ := UInt16.mul_zero sub_eq_add_neg := UInt16.sub_eq_add_neg pow_zero := UInt16.pow_zero pow_succ := UInt16.pow_succ @@ -175,8 +181,11 @@ instance : CommRing UInt32 where mul_assoc := UInt32.mul_assoc mul_comm := UInt32.mul_comm mul_one := UInt32.mul_one + one_mul := UInt32.one_mul left_distrib _ _ _ := UInt32.mul_add + right_distrib _ _ _ := UInt32.add_mul zero_mul _ := UInt32.zero_mul + mul_zero _ := UInt32.mul_zero sub_eq_add_neg := UInt32.sub_eq_add_neg pow_zero := UInt32.pow_zero pow_succ := UInt32.pow_succ @@ -197,8 +206,11 @@ instance : CommRing UInt64 where mul_assoc := UInt64.mul_assoc mul_comm := UInt64.mul_comm mul_one := UInt64.mul_one + one_mul := UInt64.one_mul left_distrib _ _ _ := UInt64.mul_add + right_distrib _ _ _ := UInt64.add_mul zero_mul _ := UInt64.zero_mul + mul_zero _ := UInt64.mul_zero sub_eq_add_neg := UInt64.sub_eq_add_neg pow_zero := UInt64.pow_zero pow_succ := UInt64.pow_succ @@ -219,8 +231,11 @@ instance : CommRing USize where mul_assoc := USize.mul_assoc mul_comm := USize.mul_comm mul_one := USize.mul_one + one_mul := USize.one_mul left_distrib _ _ _ := USize.mul_add + right_distrib _ _ _ := USize.add_mul zero_mul _ := USize.zero_mul + mul_zero _ := USize.mul_zero sub_eq_add_neg := USize.sub_eq_add_neg pow_zero := USize.pow_zero pow_succ := USize.pow_succ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean index 61b7d37077..6f9565c1a1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean @@ -17,7 +17,7 @@ variable [Monad M] [MonadGetRing M] private def denoteNum (k : Int) : M Expr := do let ring ← getRing let n := mkRawNatLit k.natAbs - let ofNatInst := mkApp3 (mkConst ``Grind.CommRing.ofNat [ring.u]) ring.type ring.commRingInst n + let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst if k < 0 then return mkApp ring.negFn n diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean index de719e5a98..a54de84da1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean @@ -12,67 +12,67 @@ namespace Lean.Meta.Grind.Arith.CommRing private def internalizeFn (fn : Expr) : GoalM Expr := do shareCommon (← canon fn) -private def getAddFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getAddFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do let instType := mkApp3 (mkConst ``HAdd [u, u, u]) type type type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring addition{indentExpr instType}" - let inst' := mkApp2 (mkConst ``instHAdd [u]) type <| mkApp2 (mkConst ``Grind.CommRing.toAdd [u]) type commRingInst + let inst' := mkApp2 (mkConst ``instHAdd [u]) type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [u]) type semiringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for addition{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for addition{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}" internalizeFn <| mkApp4 (mkConst ``HAdd.hAdd [u, u, u]) type type type inst -private def getMulFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getMulFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do let instType := mkApp3 (mkConst ``HMul [u, u, u]) type type type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring multiplication{indentExpr instType}" - let inst' := mkApp2 (mkConst ``instHMul [u]) type <| mkApp2 (mkConst ``Grind.CommRing.toMul [u]) type commRingInst + let inst' := mkApp2 (mkConst ``instHMul [u]) type <| mkApp2 (mkConst ``Grind.Semiring.toMul [u]) type semiringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for multiplication{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for multiplication{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}" internalizeFn <| mkApp4 (mkConst ``HMul.hMul [u, u, u]) type type type inst -private def getSubFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getSubFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Expr := do let instType := mkApp3 (mkConst ``HSub [u, u, u]) type type type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring subtraction{indentExpr instType}" - let inst' := mkApp2 (mkConst ``instHSub [u]) type <| mkApp2 (mkConst ``Grind.CommRing.toSub [u]) type commRingInst + let inst' := mkApp2 (mkConst ``instHSub [u]) type <| mkApp2 (mkConst ``Grind.Ring.toSub [u]) type ringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for subtraction{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for subtraction{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}" internalizeFn <| mkApp4 (mkConst ``HSub.hSub [u, u, u]) type type type inst -private def getNegFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getNegFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Expr := do let instType := mkApp (mkConst ``Neg [u]) type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring negation{indentExpr instType}" - let inst' := mkApp2 (mkConst ``Grind.CommRing.toNeg [u]) type commRingInst + let inst' := mkApp2 (mkConst ``Grind.Ring.toNeg [u]) type ringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for negation{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for negation{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}" internalizeFn <| mkApp2 (mkConst ``Neg.neg [u]) type inst -private def getPowFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getPowFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do let instType := mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring power operator{indentExpr instType}" - let inst' := mkApp2 (mkConst ``Grind.CommRing.toHPow [u]) type commRingInst + let inst' := mkApp2 (mkConst ``Grind.Semiring.toHPow [u]) type semiringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for power operator{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for power operator{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}" internalizeFn <| mkApp4 (mkConst ``HPow.hPow [u, 0, u]) type Nat.mkType type inst -private def getIntCastFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getIntCastFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Expr := do let instType := mkApp (mkConst ``IntCast [u]) type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring intCast{indentExpr instType}" - let inst' := mkApp2 (mkConst ``Grind.CommRing.intCast [u]) type commRingInst + let inst' := mkApp2 (mkConst ``Grind.Ring.intCast [u]) type ringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for intCast{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for intCast{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}" internalizeFn <| mkApp2 (mkConst ``IntCast.intCast [u]) type inst -private def getNatCastFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM Expr := do +private def getNatCastFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do let instType := mkApp (mkConst ``NatCast [u]) type let .some inst ← trySynthInstance instType | throwError "failed to find instance for ring natCast{indentExpr instType}" - let inst' := mkApp2 (mkConst ``Grind.CommRing.natCast [u]) type commRingInst + let inst' := mkApp2 (mkConst ``Grind.Semiring.natCast [u]) type semiringInst unless (← withDefault <| isDefEq inst inst') do - throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" + throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}" internalizeFn <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst /-- @@ -93,30 +93,36 @@ def getRingId? (type : Expr) : GoalM (Option Nat) := do where go? : GoalM (Option Nat) := do let u ← getDecLevel type - let ring := mkApp (mkConst ``Grind.CommRing [u]) type - let .some commRingInst ← trySynthInstance ring | return none + let semiring := mkApp (mkConst ``Grind.Semiring [u]) type + let .some semiringInst ← trySynthInstance semiring | return none + let ring := mkApp (mkConst ``Grind.Ring [u]) type + let .some ringInst ← trySynthInstance ring | return none + let commSemiring := mkApp (mkConst ``Grind.CommSemiring [u]) type + let .some commSemiringInst ← trySynthInstance commSemiring | return none + let commRing := mkApp (mkConst ``Grind.CommRing [u]) type + let .some commRingInst ← trySynthInstance commRing | return none trace_goal[grind.ring] "new ring: {type}" let charInst? ← withNewMCtxDepth do let n ← mkFreshExprMVar (mkConst ``Nat) - let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type commRingInst n + let charType := mkApp3 (mkConst ``Grind.IsCharP [u]) type ringInst n let .some charInst ← trySynthInstance charType | pure none let n ← instantiateMVars n let some n ← evalNat n |>.run | trace_goal[grind.ring] "found instance for{indentExpr charType}\nbut characteristic is not a natural number"; pure none trace_goal[grind.ring] "characteristic: {n}" pure <| some (charInst, n) - let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type commRingInst + let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type ringInst let noZeroDivInst? := (← trySynthInstance noZeroDivType).toOption trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}" - let addFn ← getAddFn type u commRingInst - let mulFn ← getMulFn type u commRingInst - let subFn ← getSubFn type u commRingInst - let negFn ← getNegFn type u commRingInst - let powFn ← getPowFn type u commRingInst - let intCastFn ← getIntCastFn type u commRingInst - let natCastFn ← getNatCastFn type u commRingInst + let addFn ← getAddFn type u semiringInst + let mulFn ← getMulFn type u semiringInst + let subFn ← getSubFn type u ringInst + let negFn ← getNegFn type u ringInst + let powFn ← getPowFn type u semiringInst + let intCastFn ← getIntCastFn type u ringInst + let natCastFn ← getNatCastFn type u semiringInst let id := (← get').rings.size - let ring : Ring := { id, type, u, commRingInst, charInst?, noZeroDivInst?, addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn } + let ring : Ring := { id, type, u, semiringInst, ringInst, commSemiringInst, commRingInst, charInst?, noZeroDivInst?, addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn } modify' fun s => { s with rings := s.rings.push ring } return some id diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index ab842736a0..36bc6e6dbd 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -132,6 +132,12 @@ structure Ring where type : Expr /-- Cached `getDecLevel type` -/ u : Level + /-- `Semiring` instance for `type` -/ + semiringInst : Expr + /-- `Ring` instance for `type` -/ + ringInst : Expr + /-- `CommSemiring` instance for `type` -/ + commSemiringInst : Expr /-- `CommRing` instance for `type` -/ commRingInst : Expr /-- `IsCharP` instance for `type` if available. -/ diff --git a/tests/lean/run/infoFromFailure.lean b/tests/lean/run/infoFromFailure.lean index d425b4e8d3..12d10ef081 100644 --- a/tests/lean/run/infoFromFailure.lean +++ b/tests/lean/run/infoFromFailure.lean @@ -16,9 +16,25 @@ info: B.foo "hello" : String × String --- trace: [Meta.synthInstance] ❌️ Add String [Meta.synthInstance] new goal Add String - [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd] - [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add String + [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd] + [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String + [Meta.synthInstance] new goal Lean.Grind.Semiring String + [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring] + [Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String + [Meta.synthInstance] new goal Lean.Grind.CommSemiring String + [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring] + [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring String ≟ Lean.Grind.CommSemiring String + [Meta.synthInstance] no instances for Lean.Grind.CommRing String + [Meta.synthInstance.instances] #[] + [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String + [Meta.synthInstance] new goal Lean.Grind.Ring String + [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing] + [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String [Meta.synthInstance] no instances for Lean.Grind.CommRing String [Meta.synthInstance.instances] #[] [Meta.synthInstance] result @@ -31,9 +47,25 @@ trace: [Meta.synthInstance] ❌️ Add String /-- trace: [Meta.synthInstance] ❌️ Add Bool [Meta.synthInstance] new goal Add Bool - [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd] - [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add Bool + [Meta.synthInstance.instances] #[@Lean.Grind.Semiring.toAdd] + [Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool + [Meta.synthInstance] new goal Lean.Grind.Semiring Bool + [Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring] + [Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool + [Meta.synthInstance] new goal Lean.Grind.CommSemiring Bool + [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring] + [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring Bool ≟ Lean.Grind.CommSemiring Bool + [Meta.synthInstance] no instances for Lean.Grind.CommRing Bool + [Meta.synthInstance.instances] #[] + [Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool + [Meta.synthInstance] new goal Lean.Grind.Ring Bool + [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing] + [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool + [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool [Meta.synthInstance] no instances for Lean.Grind.CommRing Bool [Meta.synthInstance.instances] #[] [Meta.synthInstance] result