chore: update tests

src/Init/Grind/Tactics.lean

@@ -177,7 +177,7 @@ structure Config where
   /--
   When `true` (default: `false`), uses procedure for handling equalities over commutative rings.
   -/
-  ring := false
+  ring := true
   ringSteps := 10000
   /--
   When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise

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

@@ -27,9 +27,19 @@ private def getType? (e : Expr) : Option Expr :=
 
 private def isForbiddenParent (parent? : Option Expr) : Bool :=
   if let some parent := parent? then
-    getType? parent |>.isSome
+    if getType? parent |>.isSome then
+      true
+    else
+      -- We also ignore the following parents.
+      -- Remark: `HDiv` should appear in `getType?` as soon as we add support for `Field`,
+      -- `LE.le` linear combinations
+      match_expr parent with
+      | LE.le _ _ _ _ => true
+      | HDiv.hDiv _ _ _ _ _ _ => true
+      | HMod.hMod _ _ _ _ _ _ => true
+      | _ => false
   else
-    false
+    true
 
 def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do
   if !(← getConfig).ring && !(← getConfig).ringNull then return ()

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

@@ -51,15 +51,15 @@ partial def reify? (e : Expr) : RingM (Option RingExpr) := do
       if isPowInst (← getRing) i then return .pow (← go a) k else asVar e
     | Neg.neg _ i a =>
       if isNegInst (← getRing) i then return .neg (← go a) else asVar e
-    | IntCast.intCast _ i e =>
+    | IntCast.intCast _ i a =>
       if isIntCastInst (← getRing) i then
-        let some k ← getIntValue? e | toVar e
+        let some k ← getIntValue? a | toVar e
         return .num k
       else
         asVar e
-    | NatCast.natCast _ i e =>
+    | NatCast.natCast _ i a =>
       if isNatCastInst (← getRing) i then
-        let some k ← getNatValue? e | toVar e
+        let some k ← getNatValue? a | toVar e
         return .num k
       else
         asVar e

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -288,7 +288,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
 
 /-- Different kinds of terms internalized by this module. -/
 private inductive SupportedTermKind where
-  | add | mul | num | div | mod | sub | natAbs | toNat
+  | add | mul | num | div | mod | sub | pow | natAbs | toNat
   deriving BEq
 
 private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@@ -298,6 +298,7 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
   | HMul.hMul α _ _ _ _ _ => some (.mul, α)
   | HDiv.hDiv α _ _ _ _ _ => some (.div, α)
   | HMod.hMod α _ _ _ _ _ => some (.mod, α)
+  | HPow.hPow α _ _ _ _ _ => some (.pow, α)
   | OfNat.ofNat α _ _ => some (.num, α)
   | Neg.neg α _ a =>
     let_expr OfNat.ofNat _ _ _ := a | none
@@ -312,12 +313,14 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
   -- TODO: document `NatCast.natCast` case.
   -- Remark: we added it to prevent natCast_sub from being expanded twice.
   if declName == ``NatCast.natCast then return true
-  if k matches .div | .mod | .sub | .natAbs | .toNat then return false
+  if k matches .div | .mod | .sub | .pow | .natAbs | .toNat then return false
   if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
   match k with
   | .add => return false
   | .mul => return declName == ``HMul.hMul
-  | .num => return declName == ``HMul.hMul
+  | .num =>
+    -- Recall that we don't want to internalize numerals occurring at terms such as `x^3`.
+    return declName == ``HMul.hMul || declName == ``HPow.hPow
   | _ => unreachable!
 
 private def internalizeInt (e : Expr) : GoalM Unit := do

tests/lean/run/grind_ring_1.lean

@@ -4,16 +4,16 @@ set_option grind.debug true
 open Lean.Grind
 
 example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 - 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] [IsCharP α 256] (x : α) : (x + 16)*(x - 16) = x^2 := by
-  grind +ring
+  grind
 
 example (x : Int) : (x + 1)*(x - 1) = x^2 - 1 := by
-  grind +ring
+  grind
 
 example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by
-  grind +ring
+  grind
 
 /--
 trace: [grind.ring] new ring: Int
@@ -23,49 +23,46 @@ trace: [grind.ring] new ring: Int
 #guard_msgs (trace) in
 set_option trace.grind.ring true in
 example (x : Int) : (x + 1)^2 - 1 = x^2 + 2*x := by
-  grind +ring
+  grind
 
 example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by
-  grind +ring
+  grind
 
 /--
-trace: [grind.ring] new ring: Int
-[grind.ring] characteristic: 0
-[grind.ring] NoNatZeroDivisors available: true
-[grind.ring] new ring: BitVec 8
+trace: [grind.ring] new ring: BitVec 8
 [grind.ring] characteristic: 256
 [grind.ring] NoNatZeroDivisors available: false
 -/
 #guard_msgs (trace) in
 set_option trace.grind.ring true in
 example (x : BitVec 8) : (x + 1)^2 - 1 = x^2 + 2*x := by
-  grind +ring
+  grind
 
 example (x : Int) : (x + 1)*(x - 1) = x^2 → False := by
-  grind +ring
+  grind
 
 example (x y : Int) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
-  grind +ring
+  grind
 
 example (x : UInt8) : (x + 1)*(x - 1) = x^2 → False := by
-  grind +ring
+  grind
 
 example (x y : BitVec 8) : (x + 1)*(x - 1)*y + y = y*x^2 + 1 → False := by
-  grind +ring
+  grind
 
 example [CommRing α] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
-  fail_if_success grind +ring
+  fail_if_success grind
   sorry
 
 example [CommRing α] [IsCharP α 0] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
-  grind +ring
+  grind
 
 example [CommRing α] [IsCharP α 8] (x : α) : (x + 1)*(x - 1) = x^2 → False := by
-  grind +ring
+  grind
 
 /-- trace: [grind.ring.assert.queue] -7 * x ^ 2 + 16 * y ^ 2 + x = 0 -/
 #guard_msgs (trace) in
 set_option trace.grind.ring.assert.queue true in
 example (x y : Int) : x + 16*y^2 - 7*x^2 = 0 → False := by
-  fail_if_success grind +ring
+  fail_if_success grind
   sorry

tests/lean/run/grind_ring_2.lean

@@ -3,74 +3,74 @@ set_option grind.debug true
 open Lean.Grind
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  fail_if_success grind +ring
+  fail_if_success grind
   sorry
 
 example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by
-  grind +ring
+  grind
 
 example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] [IsCharP α 7] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] [IsCharP α 8] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
-  fail_if_success grind +ring
+  fail_if_success grind
   sorry
 
 example [CommRing α] [IsCharP α 8] [NoNatZeroDivisors α] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
-  grind +ring
+  grind
 
 example (x y : UInt8) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind +ring
+  grind
 
 example (x y : UInt8) : 3*x = 1 → 3*y = 2 → False := by
-  fail_if_success grind +ring
+  fail_if_success grind
   sorry
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 6*x = 1 → 3*y = 2 → 2*x + y = 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y = 2 → 200000*x + 100*y = 1 := by
-  grind +ring
+  grind
 
 example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
-  grind +ring
+  grind
 
 example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
   grind +ringNull
 
 example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
-  grind +ring
+  grind
 
 example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
   grind +ringNull
 
 example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] (x y : α) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
-  grind +ring
+  grind
 
 example (x y : BitVec 16) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 = y → f (y*x) = f 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] (x y : α) (f : α → Nat) : x^2*y = 1 → x*y^2 - y = 0 → f (y*x) = f (y*x*y) := by
-  grind +ring
+  grind
 
 example [CommRing α] (a b c : α)
   : a + b + c = 3 →
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     a^4 + b^4 + c^4 = 9 := by
-  grind +ring
+  grind
 
 /--
 trace: [grind.ring.assert.basis] a + b + c + -3 = 0
@@ -84,7 +84,7 @@ example [CommRing α] (a b c : α)
     a^3 + b^3 + c^3 = 7 →
     a^4 + b^4 = 9 - c^4 := by
   set_option trace.grind.ring.assert.basis true in
-  grind +ring
+  grind
 
 /--
 trace: [grind.ring.assert.basis] a + b + c + -3 = 0
@@ -98,25 +98,25 @@ example [CommRing α] [NoNatZeroDivisors α] (a b c : α)
     a^3 + b^3 + c^3 = 7 →
     a^4 + b^4 = 9 - c^4 := by
   set_option trace.grind.ring.assert.basis true in
-  grind +ring
+  grind
 
 example [CommRing α] (a b : α) (f : α → Nat) : a - b = 0 → f a = f b := by
-  grind +ring
+  grind
 
 example (a b : BitVec 8) (f : BitVec 8 → Nat) : a - b = 0 → f a = f b := by
-  grind +ring
+  grind
 
 example (a b c : BitVec 8) (f : BitVec 8 → Nat) : c = 255 → - a + b - 1 = c → f a = f b := by
-  grind +ring
+  grind
 
 example (a b c : BitVec 8) (f : BitVec 8 → Nat) : c = 255 → - a + b - 1 = c → f (2*a) = f (b + a) := by
-  grind +ring
+  grind
 
 /-- trace: [grind.ring.impEq] skip: b = a, k: 2, noZeroDivisors: false -/
 #guard_msgs (trace) in
 example (a b c : BitVec 8) (f : BitVec 8 → Nat) : 2*a = 1 → 2*b = 1 → f (a) = f (b) := by
   set_option trace.grind.ring.impEq true in
-  fail_if_success grind +ring
+  fail_if_success grind
   sorry
 
 example (a b c : Int) (f : Int → Nat)
@@ -124,38 +124,38 @@ example (a b c : Int) (f : Int → Nat)
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] (a b c : α) (f : α → Nat)
   : a + b + c = 3 →
     a^2 + b^2 + c^2 = 5 →
     a^3 + b^3 + c^3 = 7 →
     f (a^4 + b^4) + f (9 - c^4) ≠ 1 := by
-  grind +ring
+  grind
 
 example [CommRing α] [NoNatZeroDivisors α] (x y z : α) : 3*x = 1 → 3*z = 2 → 2*y = 2 → x + z + 3*y = 4 := by
-  grind +ring
+  grind
 
 example (x y : Fin 11) : x^2*y = 1 → x*y^2 = y → y*x = 1 := by
-  grind +ring
+  grind
 
 example (x y : Fin 11) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
-  grind +ring
+  grind
 
 example (x y z : Fin 13) :
     (x + y + z) ^ 2 = x ^ 2 + y ^ 2 + z ^ 2 + 2 * (x * y + y * z + z * x) := by
-  grind +ring
+  grind
 
 example (x y : Fin 17) : (x + y) ^ 3 = x ^ 3 + y ^ 3 + 3 * x * y * (x + y) := by
-  grind +ring
+  grind
 
 example (x y : Fin 19) : (x - y) * (x ^ 2 + x * y + y ^ 2) = x ^ 3 - y ^ 3 := by
-  grind +ring
+  grind
 
 example (x : Fin 19) : (1 + x) ^ 5 = x ^ 5 + 5 * x ^ 4 + 10 * x ^ 3 + 10 * x ^ 2 + 5 * x + 1 := by
-  grind +ring
+  grind
 
 example (x : Fin 10) : (1 + x) ^ 5 = x ^ 5 + 5 * x ^ 4 - 5 * x + 1 := by
-  grind +ring
+  grind
 
-example (x y : Fin 3) (h : x = y) : ((x + y) ^ 3 : Fin 3) = - x^3 := by grind +ring
+example (x y : Fin 3) (h : x = y) : ((x + y) ^ 3 : Fin 3) = - x^3 := by grind

tests/lean/run/grind_ring_3.lean

@@ -6,14 +6,14 @@ example {α} [CommRing α] [IsCharP α 0]
     (d t : α)
   (Δ40 : d + t + d * t = 0)
   (Δ41 : d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4 = 0) :
-  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind +ring
+  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind
 
 example {α} [CommRing α] [IsCharP α 0]
     (d t d_inv : α)
   (Δ40 : d * (d + t + d * t) = 0)
   (Δ41 : d * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
   (_ : d * d_inv = 1) :
-  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind +ring
+  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind
 
 -- The theorems above hold in any `CommRing`
 
@@ -21,11 +21,11 @@ example {α} [CommRing α]
     (d t : α)
   (Δ40 : d + t + d * t = 0)
   (Δ41 : d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4 = 0) :
-  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind +ring
+  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind
 
 example {α} [CommRing α]
     (d t d_inv : α)
   (Δ40 : d * (d + t + d * t) = 0)
   (Δ41 : d * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
   (_ : d * d_inv = 1) :
-  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind +ring
+  t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by grind

tests/lean/run/grind_ring_4.lean

@@ -7,7 +7,7 @@ example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
   (Δ40 : d + t + d * t = 0)
   (Δ41 : 2 * d + 2 * d * t - 4 * d * t^2 + 2 * d * t^4 + 2 * d^2 * t^4 = 0) :
   t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by
-  grind +ring
+  grind
 
 example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
     (d t d_inv : α)
@@ -15,4 +15,4 @@ example {α} [CommRing α] [IsCharP α 0] [NoNatZeroDivisors α]
   (Δ41 : d^2 * (d + d * t - 2 * d * t^2 + d * t^4 + d^2 * t^4) = 0)
   (_ : d * d_inv = 1) :
   t + 2 * t^2 - t^3 - 2 * t^4 + t^5 = 0 := by
-  grind +ring
+  grind

tests/lean/run/grind_ring_5.lean

@@ -8,4 +8,4 @@ example {α} [CommRing α] [IsCharP α 0] (d t c : α) (d_inv PSO3_inv : α)
     (2 * d + 2 * d * t - 4 * d * t^2 + 2 * d * t^4 + 2 * d^2 * t^4 - c * (d + t + d * t)) = 0)
   (_ : d * d_inv = 1)
   (_ : (d + t - d * t - 2) * PSO3_inv = 1) :
-  t^2 = t + 1 := by grind +ring
+  t^2 = t + 1 := by grind

tests/lean/run/grind_trig.lean

@@ -14,23 +14,23 @@ grind_pattern trig_identity => sin x
 -- That's a polynomial, so it is sent to the Grobner basis module.
 -- And we can prove equalities modulo that relation!
 example : (cos x + sin x)^2 = 2 * cos x * sin x + 1 := by
-  grind +ring
+  grind
 
 -- `grind` notices that the two arguments of `f` are equal,
 -- and hence the function applications are too.
 example (f : R → Nat) : f ((cos x + sin x)^2) = f (2 * cos x * sin x + 1) := by
-  grind +ring
+  grind
 
 -- After that, we can use basic modularity conditions:
 -- this reduces to `4 * x ≠ 2 + x` for some `x : ℕ`
 example (f : R → Nat) : 4 * f ((cos x + sin x)^2) ≠ 2 + f (2 * cos x * sin x + 1) := by
-  grind +ring
+  grind
 
 -- A bit of case splitting is also fine.
 -- If `max = 3`, then `f _ = 0`, and we're done.
 -- Otherwise, the previous argument applies.
 example (f : R → Nat) : max 3 (4 * f ((cos x + sin x)^2)) ≠ 2 + f (2 * cos x * sin x + 1) := by
-  grind +ring
+  grind
 
 -- See https://github.com/leanprover-community/mathlib4/blob/nightly-testing/MathlibTest/grind/trig.lean
 -- for the Mathlib version of this test, using the real `ℝ`, `cos`, `sin`, and `cos_sq_and_sin_sq` declarations.