chore: update tests

src/Init/Grind/Norm.lean

@@ -178,6 +178,7 @@ init_grind_norm
   Nat.add_eq Nat.sub_eq Nat.mul_eq Nat.zero_eq Nat.le_eq
   Nat.div_zero Nat.mod_zero Nat.div_one Nat.mod_one
   Nat.sub_sub Nat.pow_zero Nat.pow_one Nat.sub_self
+  Nat.one_pow
   -- Int
   Int.lt_eq
   Int.emod_neg Int.ediv_neg
@@ -186,7 +187,7 @@ init_grind_norm
   Int.negSucc_eq
   natCast_eq natCast_div natCast_mod
   natCast_add natCast_mul
-
+  Int.one_pow
   Int.pow_zero Int.pow_one
   -- GT GE
   ge_eq gt_eq

src/Lean/Meta/Tactic/Grind/Arith/CommRing/Reify.lean

@@ -92,13 +92,13 @@ partial def reify? (e : Expr) (skipVar := true) : RingM (Option RingExpr) := do
     if isNegInst (← getRing) i then return some (.neg (← go a)) else asTopVar e
   | IntCast.intCast _ i a =>
     if isIntCastInst (← getRing) i then
-      let some k ← getIntValue? a | asTopVar e
+      let some k ← getIntValue? a | toTopVar e
       return some (.num k)
     else
       asTopVar e
   | NatCast.natCast _ i a =>
     if isNatCastInst (← getRing) i then
-      let some k ← getNatValue? a | asTopVar e
+      let some k ← getNatValue? a | toTopVar e
       return some (.num k)
     else
       asTopVar e

tests/lean/grind/algebra/field_normalization.lean

@@ -1,6 +1,8 @@
 open Lean.Grind
 
 variable (R : Type u) [Field R]
+-- We need to store equalities/disequalities such as `2 = 0` when characteristic is not unknown.
+-- The current implementation discards them.
 
 example (a : R) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind
 

tests/lean/grind/ring_regressions.lean

@@ -1,8 +1,5 @@
 -- These are test cases extracted from Mathlib, where `ring` works but `grind` does not (yet!)
-
-example (n : Nat) :
-  1 ^ (n / 3) * 2 ^ t = 2 ^ t := by grind
-
+-- We need a semiring normalizer
 example (a b : Nat) : 3 * a * b = a * b * 3 := by grind
 
 example (k z : Nat) : k * (z * 2 * (z * 2 + 1)) = z * (k * (2 * (z * 2 + 1))) := by grind

tests/lean/run/grind_semiring.lean

@@ -0,0 +1,3 @@
+example (n t : Nat) : 1 ^ (n / 3) * 2 ^ t = 2 ^ t := by grind
+
+example (n t : Nat) : (1 : Int) ^ (n / 3) * 2 ^ t = 2 ^ t := by grind