feat: proof-by-reflection support for converting semiring terms into ring ones (#8845)

This PR implements the proof-by-reflection infrastructure for embedding
semiring terms as ring ones.

src/Init/Grind/Ring.lean

@@ -10,3 +10,4 @@ import Init.Grind.Ring.Basic
 import Init.Grind.Ring.Poly
 import Init.Grind.Ring.Field
 import Init.Grind.Ring.Envelope
+import Init.Grind.Ring.OfSemiring

src/Init/Grind/Ring/Envelope.lean

@@ -258,7 +258,7 @@ theorem toQ_mul (a b : α) : toQ (a * b) = toQ a * toQ b := by
 theorem toQ_natCast (n : Nat) : toQ (natCast (α := α) n) = natCast n := by
   simp; apply Quot.sound; simp [natCast]; refine ⟨0, ?_⟩; rfl
 
-theorem toQ_ofNat (n : Nat) : toQ (OfNat.ofNat (α := α) n) = natCast n := by
+theorem toQ_ofNat (n : Nat) : toQ (OfNat.ofNat (α := α) n) = OfNat.ofNat (α := Q α) n := by
   simp; apply Quot.sound; rw [Semiring.ofNat_eq_natCast]; simp
 
 theorem toQ_pow (a : α) (n : Nat) : toQ (a ^ n) = toQ a ^ n := by
@@ -291,7 +291,7 @@ theorem Q.exact : Q.mk a = Q.mk b → r α a b := by
   constructor; exact r_rfl; exact r_sym; exact r_trans
 
 -- If the CommSemiring has the `AddRightCancel` property then `toQ` is injective
-theorem toQ_inj [AddRightCancel α] (a b : α) : toQ a = toQ b → a = b := by
+theorem toQ_inj [AddRightCancel α] {a b : α} : toQ a = toQ b → a = b := by
   simp; intro h₁
   replace h₁ := Q.exact h₁
   simp at h₁

src/Init/Grind/Ring/OfSemiring.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+
+prelude
+import Init.Grind.Ring.Envelope
+import Init.Data.Hashable
+import Init.Data.RArray
+
+namespace Lean.Grind.Ring.OfSemiring
+/-!
+Helper definitions and theorems for converting `Semiring` expressions into `Ring` ones.
+We use them to implement `grind`
+-/
+abbrev Var := Nat
+inductive Expr where
+  | num  (v : Nat)
+  | var  (i : Var)
+  | add  (a b : Expr)
+  | mul (a b : Expr)
+  | pow (a : Expr) (k : Nat)
+  deriving Inhabited, BEq, Hashable
+
+abbrev Context (α : Type u) := RArray α
+
+def Var.denote {α} (ctx : Context α) (v : Var) : α :=
+  ctx.get v
+
+def Expr.denote {α} [Semiring α] (ctx : Context α) : Expr → α
+  | .num k    => OfNat.ofNat (α := α) k
+  | .var v    => v.denote ctx
+  | .add a b  => denote ctx a + denote ctx b
+  | .mul a b  => denote ctx a * denote ctx b
+  | .pow a k  => denote ctx a ^ k
+
+attribute [local instance] ofSemiring
+
+def Expr.denoteAsRing {α} [Semiring α] (ctx : Context α) : Expr → Q α
+  | .num k    => OfNat.ofNat (α := Q α) k
+  | .var v    => toQ (v.denote ctx)
+  | .add a b  => denoteAsRing ctx a + denoteAsRing ctx b
+  | .mul a b  => denoteAsRing ctx a * denoteAsRing ctx b
+  | .pow a k  => denoteAsRing ctx a ^ k
+
+attribute [local simp] toQ_add toQ_mul toQ_ofNat toQ_pow
+
+theorem Expr.denoteAsRing_eq {α} [Semiring α] (ctx : Context α) (e : Expr) : e.denoteAsRing ctx = toQ (e.denote ctx) := by
+  induction e <;> simp [denote, denoteAsRing, *]
+
+theorem of_eq {α} [Semiring α] (ctx : Context α) (lhs rhs : Expr)
+    : lhs.denote ctx = rhs.denote ctx → lhs.denoteAsRing ctx = rhs.denoteAsRing ctx := by
+  intro h; replace h := congrArg toQ h
+  simpa [← Expr.denoteAsRing_eq] using h
+
+theorem of_diseq {α} [Semiring α] [AddRightCancel α] (ctx : Context α) (lhs rhs : Expr)
+    : lhs.denote ctx ≠ rhs.denote ctx → lhs.denoteAsRing ctx ≠ rhs.denoteAsRing ctx := by
+  intro h₁ h₂
+  simp [Expr.denoteAsRing_eq] at h₂
+  replace h₂ := toQ_inj h₂
+  contradiction
+
+end Lean.Grind.Ring.OfSemiring