From febf6c10f0852bb5ccf32eb7f978494ad15eb94e Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 30 Apr 2025 02:50:54 +1000 Subject: [PATCH] fix: update Grind.CommRing to avoid constructing non-defeq NatCast instance (#8161) This PR changes `Lean.Grind.CommRing` to inline the `NatCast` instance (i.e. to be provided by the user) rather than constructing one from the existing data. Without this change we can't construct instances in Mathlib that `grind` can use. --- src/Init/Grind/CommRing/Basic.lean | 62 ++++++++++--------- src/Init/Grind/CommRing/Int.lean | 4 +- src/Init/Grind/CommRing/Poly.lean | 12 ++-- src/Init/Grind/CommRing/SInt.lean | 15 +++++ src/Init/Grind/CommRing/UInt.lean | 16 ++++- .../Tactic/Grind/Arith/CommRing/EqCnstr.lean | 2 +- .../Tactic/Grind/Arith/CommRing/Proof.lean | 2 +- .../Tactic/Grind/Arith/CommRing/Reify.lean | 10 +-- .../Tactic/Grind/Arith/CommRing/RingId.lean | 6 +- .../Tactic/Grind/Arith/CommRing/Types.lean | 6 +- .../Tactic/Grind/Arith/CommRing/Util.lean | 4 +- tests/lean/run/grind_ring_1.lean | 4 +- tests/lean/run/grind_ring_2.lean | 10 +-- 13 files changed, 91 insertions(+), 62 deletions(-) diff --git a/src/Init/Grind/CommRing/Basic.lean b/src/Init/Grind/CommRing/Basic.lean index 5153edd3d4..746c24b1a1 100644 --- a/src/Init/Grind/CommRing/Basic.lean +++ b/src/Init/Grind/CommRing/Basic.lean @@ -32,6 +32,7 @@ namespace Lean.Grind class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, 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 @@ -46,6 +47,7 @@ class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat 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 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 @@ -55,29 +57,25 @@ class CommRing (α : Type u) extends Add α, Mul α, Neg α, Sub α, HPow α Nat -- (And similarly for the other parents.) attribute [instance 100] CommRing.toAdd CommRing.toMul CommRing.toNeg CommRing.toSub CommRing.toHPow --- This is a low-priority instance, to avoid conflicts with existing `OfNat` instances. -attribute [instance 100] CommRing.ofNat - --- This is a low-priority instance, to avoid conflicts with existing `IntCast` instances. -attribute [instance 100] CommRing.intCast +-- 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 namespace CommRing variable {α : Type u} [CommRing α] -instance natCastInst : NatCast α where - natCast n := OfNat.ofNat n - -theorem natCast_zero : ((0 : Nat) : α) = 0 := rfl -theorem ofNat_eq_natCast (n : Nat) : OfNat.ofNat n = (n : α) := rfl +theorem natCast_zero : ((0 : Nat) : α) = 0 := (ofNat_eq_natCast 0).symm +theorem natCast_one : ((1 : Nat) : α) = 1 := (ofNat_eq_natCast 1).symm theorem ofNat_add (a b : Nat) : OfNat.ofNat (α := α) (a + b) = OfNat.ofNat a + OfNat.ofNat b := by induction b with | zero => simp [Nat.add_zero, add_zero] | succ b ih => rw [Nat.add_succ, ofNat_succ, ih, ofNat_succ b, add_assoc] -theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := ofNat_add _ _ -theorem natCast_add (a b : Nat) : ((a + b : Nat) : α) = ((a : α) + (b : α)) := ofNat_add _ _ +theorem natCast_add (a b : Nat) : ((a + b : Nat) : α) = ((a : α) + (b : α)) := by + rw [← ofNat_eq_natCast, ← ofNat_eq_natCast, ofNat_add, ofNat_eq_natCast, ofNat_eq_natCast] +theorem natCast_succ (n : Nat) : ((n + 1 : Nat) : α) = ((n : α) + 1) := by + rw [natCast_add, natCast_one] theorem zero_add (a : α) : 0 + a = a := by rw [add_comm, add_zero] @@ -149,7 +147,9 @@ theorem sub_eq_zero_iff {a b : α} : a - b = 0 ↔ a = b := by theorem intCast_zero : ((0 : Int) : α) = 0 := intCast_ofNat 0 theorem intCast_one : ((1 : Int) : α) = 1 := intCast_ofNat 1 theorem intCast_neg_one : ((-1 : Int) : α) = -1 := by rw [intCast_neg, intCast_ofNat] -theorem intCast_natCast (n : Nat) : ((n : Int) : α) = (n : α) := intCast_ofNat n +theorem intCast_natCast (n : Nat) : ((n : Int) : α) = (n : α) := by + erw [intCast_ofNat] + rw [ofNat_eq_natCast] theorem intCast_natCast_add_one (n : Nat) : ((n + 1 : Int) : α) = (n : α) + 1 := by rw [← Int.natCast_add_one, intCast_natCast, natCast_add, ofNat_eq_natCast] theorem intCast_negSucc (n : Nat) : ((-(n + 1) : Int) : α) = -((n : α) + 1) := by @@ -240,14 +240,15 @@ namespace IsCharP variable (p) {α : Type u} [CommRing α] [IsCharP α p] -theorem natCast_eq_zero_iff (x : Nat) : (x : α) = 0 ↔ x % p = 0 := - ofNat_eq_zero_iff p x +theorem natCast_eq_zero_iff (x : Nat) : (x : α) = 0 ↔ x % p = 0 := by + rw [← ofNat_eq_natCast] + exact ofNat_eq_zero_iff p x theorem intCast_eq_zero_iff (x : Int) : (x : α) = 0 ↔ x % p = 0 := match x with | (x : Nat) => by have := ofNat_eq_zero_iff (α := α) p (x := x) - rw [Int.ofNat_mod_ofNat, intCast_natCast] + rw [Int.ofNat_mod_ofNat, intCast_natCast, ← ofNat_eq_natCast] norm_cast | -(x + 1 : Nat) => by rw [Int.neg_emod, Int.ofNat_mod_ofNat, intCast_neg, intCast_natCast, neg_eq_zero] @@ -286,10 +287,13 @@ theorem ofNat_ext_iff {x y : Nat} : OfNat.ofNat (α := α) x = OfNat.ofNat (α : theorem ofNat_ext {x y : Nat} (h : x % p = y % p) : OfNat.ofNat (α := α) x = OfNat.ofNat (α := α) y := (ofNat_ext_iff p).mpr h -theorem natCast_ext {x y : Nat} (h : x % p = y % p) : (x : α) = (y : α) := ofNat_ext _ h +theorem natCast_ext {x y : Nat} (h : x % p = y % p) : (x : α) = (y : α) := by + rw [← ofNat_eq_natCast, ← ofNat_eq_natCast] + exact ofNat_ext p h -theorem natCast_ext_iff {x y : Nat} : (x : α) = (y : α) ↔ x % p = y % p := - ofNat_ext_iff p +theorem natCast_ext_iff {x y : Nat} : (x : α) = (y : α) ↔ x % p = y % p := by + rw [← ofNat_eq_natCast, ← ofNat_eq_natCast] + exact ofNat_ext_iff p theorem intCast_emod (x : Int) : ((x % p : Int) : α) = (x : α) := by rw [intCast_ext_iff p, Int.emod_emod] @@ -298,8 +302,9 @@ theorem natCast_emod (x : Nat) : ((x % p : Nat) : α) = (x : α) := by simp only [← intCast_natCast] rw [Int.natCast_emod, intCast_emod] -theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x := - natCast_emod _ _ +theorem ofNat_emod (x : Nat) : OfNat.ofNat (α := α) (x % p) = OfNat.ofNat x := by + rw [ofNat_eq_natCast, ofNat_eq_natCast] + exact natCast_emod p x theorem ofNat_eq_zero_iff_of_lt {x : Nat} (h : x < p) : OfNat.ofNat (α := α) x = 0 ↔ x = 0 := by rw [ofNat_eq_zero_iff p, Nat.mod_eq_of_lt h] @@ -320,24 +325,25 @@ end IsCharP /-- Special case of Mathlib's `NoZeroSMulDivisors Nat α`. -/ -class NoZeroNatDivisors (α : Type u) [CommRing α] where - no_zero_nat_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0 +class NoNatZeroDivisors (α : Type u) [CommRing α] where + no_nat_zero_divisors : ∀ (k : Nat) (a : α), k ≠ 0 → OfNat.ofNat (α := α) k * a = 0 → a = 0 -export NoZeroNatDivisors (no_zero_nat_divisors) +export NoNatZeroDivisors (no_nat_zero_divisors) -theorem no_zero_int_divisors {α : Type u} [CommRing α] [NoZeroNatDivisors α] {k : Int} {a : α} +theorem no_int_zero_divisors {α : Type u} [CommRing α] [NoNatZeroDivisors α] {k : Int} {a : α} : k ≠ 0 → k * a = 0 → a = 0 := by match k with | (k : Nat) => simp [intCast_natCast] intro h₁ h₂ replace h₁ : k ≠ 0 := by intro h; simp [h] at h₁ - exact no_zero_nat_divisors k a h₁ h₂ + rw [← ofNat_eq_natCast] at h₂ + exact no_nat_zero_divisors k a h₁ h₂ | -(k+1 : Nat) => rw [Int.natCast_add, ← Int.natCast_add, intCast_neg, intCast_natCast] intro _ h replace h := congrArg (-·) h; simp at h - rw [← neg_mul, neg_neg, neg_zero] at h - exact no_zero_nat_divisors (k+1) a (Nat.succ_ne_zero _) h + rw [← neg_mul, neg_neg, neg_zero, ← ofNat_eq_natCast] at h + exact no_nat_zero_divisors (k+1) a (Nat.succ_ne_zero _) h end Lean.Grind diff --git a/src/Init/Grind/CommRing/Int.lean b/src/Init/Grind/CommRing/Int.lean index d2d3d77b7f..5a4c4ac860 100644 --- a/src/Init/Grind/CommRing/Int.lean +++ b/src/Init/Grind/CommRing/Int.lean @@ -29,8 +29,8 @@ instance : CommRing Int where instance : IsCharP Int 0 where ofNat_eq_zero_iff {x} := by erw [Int.ofNat_eq_zero]; simp -instance : NoZeroNatDivisors Int where - no_zero_nat_divisors k a h₁ h₂ := by +instance : NoNatZeroDivisors Int where + no_nat_zero_divisors k a h₁ h₂ := by cases Int.mul_eq_zero.mp h₂ next h => rw [← Int.natCast_zero] at h diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index 4854b3b95e..64e9c69d91 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -737,7 +737,7 @@ theorem NullCert.ne_unsat {α} [CommRing α] (ctx : Context α) (nc : NullCert) def NullCert.eq_nzdiv_cert (nc : NullCert) (k : Int) (lhs rhs : Expr) : Bool := k ≠ 0 && (lhs.sub rhs).toPoly.mulConst k == nc.toPoly -theorem NullCert.eq_nzdiv {α} [CommRing α] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) +theorem NullCert.eq_nzdiv {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_cert k lhs rhs → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by simp [eq_nzdiv_cert] intro h₁ h₂ @@ -745,11 +745,11 @@ theorem NullCert.eq_nzdiv {α} [CommRing α] [NoZeroNatDivisors α] (ctx : Conte intro h₃ replace h₂ := congrArg (Poly.denote ctx) h₂ simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, h₃, Expr.denote] at h₂ - replace h₂ := no_zero_int_divisors h₁ h₂ + replace h₂ := no_int_zero_divisors h₁ h₂ rw [sub_eq_zero_iff] at h₂ assumption -theorem NullCert.ne_nzdiv_unsat {α} [CommRing α] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) +theorem NullCert.ne_nzdiv_unsat {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_cert k lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by intro h₁ h₂ exact eqsImplies_helper' (eq_nzdiv ctx nc k lhs rhs h₁) h₂ @@ -918,7 +918,7 @@ theorem NullCert.ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α def NullCert.eq_nzdiv_certC (nc : NullCert) (k : Int) (lhs rhs : Expr) (c : Nat) : Bool := k ≠ 0 && ((lhs.sub rhs).toPolyC c).mulConstC k c == nc.toPolyC c -theorem NullCert.eq_nzdivC {α c} [CommRing α] [IsCharP α c] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) +theorem NullCert.eq_nzdivC {α c} [CommRing α] [IsCharP α c] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_certC k lhs rhs c → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by simp [eq_nzdiv_certC] intro h₁ h₂ @@ -926,11 +926,11 @@ theorem NullCert.eq_nzdivC {α c} [CommRing α] [IsCharP α c] [NoZeroNatDivisor intro h₃ replace h₂ := congrArg (Poly.denote ctx) h₂ simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₃, Expr.denote] at h₂ - replace h₂ := no_zero_int_divisors h₁ h₂ + replace h₂ := no_int_zero_divisors h₁ h₂ rw [sub_eq_zero_iff] at h₂ assumption -theorem NullCert.ne_nzdiv_unsatC {α c} [CommRing α] [IsCharP α c] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) +theorem NullCert.ne_nzdiv_unsatC {α c} [CommRing α] [IsCharP α c] [NoNatZeroDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr) : nc.eq_nzdiv_certC k lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by intro h₁ h₂ exact eqsImplies_helper' (eq_nzdivC ctx nc k lhs rhs h₁) h₂ diff --git a/src/Init/Grind/CommRing/SInt.lean b/src/Init/Grind/CommRing/SInt.lean index 4ab5cd8ec4..2b8740f002 100644 --- a/src/Init/Grind/CommRing/SInt.lean +++ b/src/Init/Grind/CommRing/SInt.lean @@ -11,6 +11,9 @@ import Init.Data.SInt.Lemmas namespace Lean.Grind +instance : NatCast Int8 where + natCast x := Int8.ofNat x + instance : IntCast Int8 where intCast x := Int8.ofInt x @@ -37,6 +40,9 @@ instance : IsCharP Int8 (2 ^ 8) where simp [Int8.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +instance : NatCast Int16 where + natCast x := Int16.ofNat x + instance : IntCast Int16 where intCast x := Int16.ofInt x @@ -62,6 +68,9 @@ instance : IsCharP Int16 (2 ^ 16) where simp [Int16.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +instance : NatCast Int32 where + natCast x := Int32.ofNat x + instance : IntCast Int32 where intCast x := Int32.ofInt x @@ -87,6 +96,9 @@ instance : IsCharP Int32 (2 ^ 32) where simp [Int32.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +instance : NatCast Int64 where + natCast x := Int64.ofNat x + instance : IntCast Int64 where intCast x := Int64.ofInt x @@ -112,6 +124,9 @@ instance : IsCharP Int64 (2 ^ 64) where simp [Int64.ofInt_eq_iff_bmod_eq_toInt, ← Int.dvd_iff_bmod_eq_zero, ← Nat.dvd_iff_mod_eq_zero, Int.ofNat_dvd_right] +instance : NatCast ISize where + natCast x := ISize.ofNat x + instance : IntCast ISize where intCast x := ISize.ofInt x diff --git a/src/Init/Grind/CommRing/UInt.lean b/src/Init/Grind/CommRing/UInt.lean index c3c7e0e18f..1f6fe6ffcc 100644 --- a/src/Init/Grind/CommRing/UInt.lean +++ b/src/Init/Grind/CommRing/UInt.lean @@ -14,6 +14,9 @@ namespace UInt8 /-- Variant of `UInt8.ofNat_mod_size` replacing `2 ^ 8` with `256`.-/ theorem ofNat_mod_size' : ofNat (x % 256) = ofNat x := ofNat_mod_size +instance : NatCast UInt8 where + natCast x := UInt8.ofNat x + instance : IntCast UInt8 where intCast x := UInt8.ofInt x @@ -34,6 +37,9 @@ namespace UInt16 /-- Variant of `UInt16.ofNat_mod_size` replacing `2 ^ 16` with `65536`.-/ theorem ofNat_mod_size' : ofNat (x % 65536) = ofNat x := ofNat_mod_size +instance : NatCast UInt16 where + natCast x := UInt16.ofNat x + instance : IntCast UInt16 where intCast x := UInt16.ofInt x @@ -54,6 +60,9 @@ namespace UInt32 /-- Variant of `UInt32.ofNat_mod_size` replacing `2 ^ 32` with `4294967296`.-/ theorem ofNat_mod_size' : ofNat (x % 4294967296) = ofNat x := ofNat_mod_size +instance : NatCast UInt32 where + natCast x := UInt32.ofNat x + instance : IntCast UInt32 where intCast x := UInt32.ofInt x @@ -74,6 +83,9 @@ namespace UInt64 /-- Variant of `UInt64.ofNat_mod_size` replacing `2 ^ 64` with `18446744073709551616`.-/ theorem ofNat_mod_size' : ofNat (x % 18446744073709551616) = ofNat x := ofNat_mod_size +instance : NatCast UInt64 where + natCast x := UInt64.ofNat x + instance : IntCast UInt64 where intCast x := UInt64.ofInt x @@ -91,6 +103,9 @@ end UInt64 namespace USize +instance : NatCast USize where + natCast x := USize.ofNat x + instance : IntCast USize where intCast x := USize.ofInt x @@ -108,7 +123,6 @@ theorem intCast_ofNat (x : Nat) : (OfNat.ofNat (α := Int) x : USize) = OfNat.of end USize namespace Lean.Grind - instance : CommRing UInt8 where add_assoc := UInt8.add_assoc add_comm := UInt8.add_comm diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index 338fe04f67..98152b5273 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -208,7 +208,7 @@ if the ring has a nonzero characteristic `p` and `gcd k p = 1`, then It also handles the easy case where `k` is `-1`. -Remark: if the ring implements the class `NoZeroNatDivisors`, then +Remark: if the ring implements the class `NoNatZeroDivisors`, then the coefficients are divided by the gcd of all coefficients. -/ def EqCnstr.toMonic (c : EqCnstr) : RingM EqCnstr := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 072ff5644f..372d885867 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -207,7 +207,7 @@ private def getNoZeroDivInstIfNeeded? (k : Int) : RingM (Option Expr) := do return none else let some inst ← noZeroDivisorsInst? - | throwError "`grind` internal error, `NoZeroNatDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}" + | throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}" return some inst def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean index 2e95679b09..b891bfc976 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean @@ -65,10 +65,7 @@ partial def reify? (e : Expr) : RingM (Option RingExpr) := do asVar e | OfNat.ofNat _ n _ => let some k ← getNatValue? n | toVar e - if (← withDefault <| isDefEq e (mkApp (← getRing).natCastFn n)) then - return .num k - else - asVar e + return .num k | _ => toVar e let asNone (e : Expr) : GoalM (Option RingExpr) := do reportAppIssue e @@ -99,10 +96,7 @@ partial def reify? (e : Expr) : RingM (Option RingExpr) := do asNone e | OfNat.ofNat _ n _ => let some k ← getNatValue? n | return none - if (← withDefault <| isDefEq e (mkApp (← getRing).natCastFn n)) then - return some (.num k) - else - asNone e + return some (.num k) | _ => return none end Lean.Meta.Grind.Arith.CommRing diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean index 6947a137c5..de719e5a98 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean @@ -70,7 +70,7 @@ private def getNatCastFn (type : Expr) (u : Level) (commRingInst : Expr) : GoalM 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.natCastInst [u]) type commRingInst + let inst' := mkApp2 (mkConst ``Grind.CommRing.natCast [u]) type commRingInst unless (← withDefault <| isDefEq inst inst') do throwError "instance for natCast{indentExpr inst}\nis not definitionally equal to the `Grind.CommRing` one{indentExpr inst'}" internalizeFn <| mkApp2 (mkConst ``NatCast.natCast [u]) type inst @@ -105,9 +105,9 @@ where | 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.NoZeroNatDivisors [u]) type commRingInst + let noZeroDivType := mkApp2 (mkConst ``Grind.NoNatZeroDivisors [u]) type commRingInst let noZeroDivInst? := (← trySynthInstance noZeroDivType).toOption - trace_goal[grind.ring] "NoZeroNatDivisors available: {noZeroDivInst?.isSome}" + 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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index 77a9cf6dd9..1179cff3b7 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -81,7 +81,7 @@ inductive PolyDerivation where The coefficient `k₁` is used because the leading monomial in `c` may not be monic. Thus, if we follow the chain back to the input polynomial, we have that `p = C * input_p` for a `C` that is equal to the product of all `k₁`s in the chain. - We have that `C ≠ 1` only if the ring does not implement `NoZeroNatDivisors`. + We have that `C ≠ 1` only if the ring does not implement `NoNatZeroDivisors`. Here is a small example where we simplify `x+y` using the equations `2*x - 1 = 0` (`c₁`), `3*y - 1 = 0` (`c₂`), and `6*z + 5 = 0` (`c₃`) ``` @@ -103,7 +103,7 @@ inductive PolyDerivation where ``` 0 = 6*(x + y + z) ``` - Recall that if the ring implement `NoZeroNatDivisors`, then the following property holds: + Recall that if the ring implement `NoNatZeroDivisors`, then the following property holds: ``` ∀ (k : Int) (a : α), k ≠ 0 → (intCast k) * a = 0 → a = 0 ``` @@ -136,7 +136,7 @@ structure Ring where commRingInst : Expr /-- `IsCharP` instance for `type` if available. -/ charInst? : Option (Expr × Nat) := .none - /-- `NoZeroNatDivisors` instance for `type` if available. -/ + /-- `NoNatZeroDivisors` instance for `type` if available. -/ noZeroDivInst? : Option Expr := .none addFn : Expr mulFn : Expr diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean index 07474bcd1e..b5ff936856 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean @@ -27,11 +27,11 @@ structure RingM.Context where If `checkCoeffDvd` is `true`, then when using a polynomial `k*m - p` to simplify `.. + k'*m*m_2 + ...`, the substitution is performed IF - `k` divides `k'`, OR - - Ring implements `NoZeroNatDivisors`. + - Ring implements `NoNatZeroDivisors`. We need this check when simplifying disequalities. In this case, if we perform the simplification anyway, we may end up with a proof that `k * q = 0`, but - we cannot deduce `q = 0` since the ring does not implement `NoZeroNatDivisors` + we cannot deduce `q = 0` since the ring does not implement `NoNatZeroDivisors` See comment at `PolyDerivation`. -/ checkCoeffDvd : Bool := false diff --git a/tests/lean/run/grind_ring_1.lean b/tests/lean/run/grind_ring_1.lean index 426a730257..a213f6ad6a 100644 --- a/tests/lean/run/grind_ring_1.lean +++ b/tests/lean/run/grind_ring_1.lean @@ -18,7 +18,7 @@ example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by /-- info: [grind.ring] new ring: Int [grind.ring] characteristic: 0 -[grind.ring] NoZeroNatDivisors available: true +[grind.ring] NoNatZeroDivisors available: true -/ #guard_msgs (info) in set_option trace.grind.ring true in @@ -31,7 +31,7 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by /-- info: [grind.ring] new ring: BitVec 8 [grind.ring] characteristic: 256 -[grind.ring] NoZeroNatDivisors available: false +[grind.ring] NoNatZeroDivisors available: false -/ #guard_msgs (info) in set_option trace.grind.ring true in diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean index 7805344b72..1cdacd7602 100644 --- a/tests/lean/run/grind_ring_2.lean +++ b/tests/lean/run/grind_ring_2.lean @@ -2,7 +2,7 @@ set_option grind.warning false set_option grind.debug true open Lean.Grind -example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by +example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by grind +ring example [CommRing α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by @@ -22,7 +22,7 @@ example [CommRing α] [IsCharP α 8] (x y : α) : 2*x = 1 → 2*y = 1 → x + y fail_if_success grind +ring sorry -example [CommRing α] [IsCharP α 8] [NoZeroNatDivisors α] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by +example [CommRing α] [IsCharP α 8] [NoNatZeroDivisors α] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by grind +ring example (x y : UInt8) : 3*x = 1 → 3*y = 2 → x + y = 1 := by @@ -32,10 +32,10 @@ example (x y : UInt8) : 3*x = 1 → 3*y = 2 → False := by fail_if_success grind +ring sorry -example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 6*x = 1 → 3*y = 2 → 2*x + y = 1 := by +example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 6*x = 1 → 3*y = 2 → 2*x + y = 1 := by grind +ring -example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 600000*x = 1 → 300*y = 2 → 200000*x + 100*y = 1 := by +example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y = 2 → 200000*x + 100*y = 1 := by grind +ring example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by @@ -86,7 +86,7 @@ info: [grind.ring.assert.basis] a + b + c + -3 = 0 [grind.ring.assert.basis] 3 * c ^ 3 + -9 * c ^ 2 + 6 * c + 2 = 0 -/ #guard_msgs (info) in -example [CommRing α] [NoZeroNatDivisors α] (a b c : α) +example [CommRing α] [NoNatZeroDivisors α] (a b c : α) : a + b + c = 3 → a^2 + b^2 + c^2 = 5 → a^3 + b^3 + c^3 = 7 →