feat: draft typeclasses/tests for grind handling fields (#8417)

This PR introduces `Lean.Grind.Field`, proves that a `IsCharP 0` field
satisfies `NoNatZeroDivisors`, and sets up some basic (currently
failing) tests for `grind`.

src/Init/Grind/CommRing.lean

@@ -13,3 +13,4 @@ import Init.Grind.CommRing.SInt
 import Init.Grind.CommRing.Fin
 import Init.Grind.CommRing.BitVec
 import Init.Grind.CommRing.Poly
+import Init.Grind.CommRing.Field

src/Init/Grind/CommRing/Field.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+module
+
+prelude
+import Init.Grind.CommRing.Basic
+
+namespace Lean.Grind
+
+class Field (α : Type u) extends CommRing α, Inv α, Div α where
+  div_eq_mul_inv : ∀ a b : α, a / b = a * b⁻¹
+  inv_zero : (0 : α)⁻¹ = 0
+  inv_one : (1 : α)⁻¹ = 1
+  mul_inv_cancel : ∀ {a : α}, a ≠ 0 → a * a⁻¹ = 1
+
+attribute [instance 100] Field.toInv Field.toDiv
+
+namespace Field
+
+variable [Field α] {a : α}
+
+theorem inv_mul_cancel (h : a ≠ 0) : a⁻¹ * a = 1 := by
+  rw [CommSemiring.mul_comm, mul_inv_cancel h]
+
+instance [IsCharP α 0] : NoNatZeroDivisors α where
+  no_nat_zero_divisors := by
+    intro a b h w
+    have := IsCharP.natCast_eq_zero_iff (α := α) 0 a
+    simp only [Nat.mod_zero, h, iff_false] at this
+    if h : b = 0 then
+      exact h
+    else
+      rw [Semiring.ofNat_eq_natCast] at w
+      replace w := congrArg (fun x => x * b⁻¹) w
+      dsimp only [] at w
+      rw [Semiring.hmul_eq_ofNat_mul, Semiring.mul_assoc, Field.mul_inv_cancel h, Semiring.mul_one,
+        Semiring.natCast_zero, Semiring.zero_mul, Semiring.ofNat_eq_natCast] at w
+      contradiction
+
+end Field
+
+end Lean.Grind

tests/lean/grind/field_normalization.lean

@@ -0,0 +1,31 @@
+open Lean.Grind
+
+variable (R : Type u) [Field R]
+
+example (a : R) : (1 / 2) * a = a / 2 := by grind
+example (a : R) : 2⁻¹ * a = a / 2 := by grind
+example (a : R) : a⁻¹⁻¹ = a := by grind
+
+example (a : R) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind
+
+example [IsCharP R 0] (a : R) : a / 2 + a / 3 = 5 * a / 6 := by grind
+
+example (_ : x ≠ 0) (_ : z ≠ 0) : w / x + y / z = (w * z + y * x) / (x * z) := by grind
+example (_ : x * z ≠ 0) : w / x + y / z = (w * z + y * x) / (x * z) := by grind
+
+example {x y z w : R} (h : x / y = z / w) (hy : y ≠ 0) (hw : w ≠ 0) : x * w = z * y := by
+  grind
+
+example (a : R) (_ : 2 * a ≠ 0) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
+example [IsCharP R 0] (a : R) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
+example [NoNatZeroDivisors R] (a : R) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
+example (a : R) (_ : (2 : R) ≠ 0) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
+
+example (a b : R) (_ : a ≠ 0) (_ : b ≠ 0) : a / (a / b) = b := by grind
+example (a b : R) (_ : a ≠ 0) : a / (a / b) = b := by grind
+
+-- TODO: create a mock implementation of `ℚ` for testing purposes.
+variable (ℚ : Type) [Field ℚ] [IsCharP ℚ 0]
+
+example (x : ℚ) (h₀ : x ≠ 0) :
+    (4 / x)⁻¹ * ((3 * x^3) / x)^2 * ((1 / (2 * x))⁻¹)^3 = 18 * x^8 := by grind

tests/lean/run/7170.lean

@@ -188,6 +188,7 @@ def matchTooFew₂ (f : Foo) : Nat :=
   | .foo2, .foo2 => 32
   | .foo => 41
 
+set_option pp.mvars false in
 /--
 error: Not enough patterns in match alternative: Expected 2, but found 1:
   .(_)
@@ -195,7 +196,7 @@ error: Not enough patterns in match alternative: Expected 2, but found 1:
 error: type mismatch
   fun b => True
 has type
-  ?m.892 → Prop : Sort (max 1 ?u.891)
+  ?_ → Prop : Sort (max 1 _)
 but is expected to have type
   Prop : Type
 -/

tests/lean/run/infoFromFailure.lean

@@ -27,7 +27,11 @@ trace: [Meta.synthInstance] ❌️ Add 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] new goal Lean.Grind.CommRing String
+      [Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing String ≟ Lean.Grind.CommRing String
+    [Meta.synthInstance] no instances for Lean.Grind.Field 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
@@ -35,8 +39,6 @@ trace: [Meta.synthInstance] ❌️ Add 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] ✅️ apply @Lean.Grind.IntModule.toAdd to Add String
     [Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
     [Meta.synthInstance] new goal Lean.Grind.IntModule String
@@ -72,7 +74,11 @@ trace: [Meta.synthInstance] ❌️ Add 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] new goal Lean.Grind.CommRing Bool
+      [Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
+  [Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
+    [Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing Bool ≟ Lean.Grind.CommRing Bool
+    [Meta.synthInstance] no instances for Lean.Grind.Field 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
@@ -80,8 +86,6 @@ trace: [Meta.synthInstance] ❌️ Add 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] ✅️ apply @Lean.Grind.IntModule.toAdd to Add Bool
     [Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
     [Meta.synthInstance] new goal Lean.Grind.IntModule Bool