test: more tests

src/Init/Grind/Ring/Field.lean

@@ -80,6 +80,45 @@ theorem inv_eq_zero_iff {a : α} : a⁻¹ = 0 ↔ a = 0 := by
 theorem zero_eq_inv_iff {a : α} : 0 = a⁻¹ ↔ 0 = a := by
   rw [eq_comm, inv_eq_zero_iff, eq_comm]
 
+theorem of_mul_eq_zero {a b : α} : a*b = 0 → a = 0 ∨ b = 0 := by
+  cases (Classical.em (a = 0)); simp [*, Semiring.zero_mul]
+  cases (Classical.em (b = 0)); simp [*, Semiring.mul_zero]
+  next h₁ h₂ =>
+  replace h₁ := Field.mul_inv_cancel h₁
+  replace h₂ := Field.mul_inv_cancel h₂
+  intro h
+  replace h := congrArg (· * b⁻¹ * a⁻¹) h; simp [Semiring.zero_mul] at h
+  rw [Semiring.mul_assoc, Semiring.mul_assoc, ← Semiring.mul_assoc b, h₂, Semiring.one_mul, h₁] at h
+  have := Field.zero_ne_one (α := α)
+  simp [h] at this
+
+theorem mul_inv (a b : α) : (a*b)⁻¹ = a⁻¹*b⁻¹ := by
+  cases (Classical.em (a = 0)); simp [*, Semiring.zero_mul, Field.inv_zero]
+  cases (Classical.em (b = 0)); simp [*, Semiring.mul_zero, Field.inv_zero]
+  cases (Classical.em (a*b = 0)); simp [*, Field.inv_zero]
+  next h => cases (of_mul_eq_zero h) <;> contradiction
+  next h₁ h₂ h₃ =>
+    replace h₁ := Field.inv_mul_cancel h₁
+    replace h₂ := Field.inv_mul_cancel h₂
+    replace h₃ := Field.mul_inv_cancel h₃
+    replace h₃ := congrArg (b⁻¹*a⁻¹* ·) h₃; simp at h₃
+    rw [Semiring.mul_assoc, Semiring.mul_assoc, ← Semiring.mul_assoc (a⁻¹), h₁, Semiring.one_mul,
+      ← Semiring.mul_assoc, h₂, Semiring.one_mul, Semiring.mul_one, CommRing.mul_comm (b⁻¹)] at h₃
+    assumption
+
+theorem of_pow_eq_zero (a : α) (n : Nat) : a^n = 0 → a = 0 := by
+  induction n
+  next => simp [Semiring.pow_zero]; intro h; have := zero_ne_one (α := α); exfalso; exact this h.symm
+  next n ih =>
+    simp [Semiring.pow_succ]; intro h
+    apply Classical.byContradiction
+    intro hne
+    have := Field.mul_inv_cancel hne
+    replace h := congrArg (· * a⁻¹) h; simp at h
+    rw [Semiring.mul_assoc, this, Semiring.mul_one, Semiring.zero_mul] at h
+    have := ih h
+    contradiction
+
 instance [IsCharP α 0] : NoNatZeroDivisors α := NoNatZeroDivisors.mk' <| by
   intro a b h w
   have := IsCharP.natCast_eq_zero_iff (α := α) 0 a

src/Lean/Meta/DecLevel.lean

@@ -70,6 +70,9 @@ def decLevel (u : Level) : MetaM Level := do
 def getDecLevel (type : Expr) : MetaM Level := do
   decLevel (← getLevel type)
 
+def getDecLevel? (type : Expr) : MetaM (Option Level) := do
+  decLevel? (← getLevel type)
+
 builtin_initialize
   registerTraceClass `Meta.isLevelDefEq.step
 

src/Lean/Meta/Tactic/Grind/Arith/Simproc.lean

@@ -10,20 +10,42 @@ import Lean.Meta.Tactic.Simp.Simproc
 
 namespace Lean.Meta.Grind.Arith
 
-/-- Applies `a^(m+n) = a^m * a^n` -/
+private def mkSemiringThm (declName : Name) (α : Expr) : MetaM (Option Expr) := do
+  let some u ← getDecLevel? α | return none
+  let semiring := mkApp (mkConst ``Grind.Semiring [u]) α
+  let .some semiringInst ← trySynthInstance semiring | return none
+  return mkApp2 (mkConst declName [u]) α semiringInst
+
+/--
+Applies `a^(m+n) = a^m * a^n`, `a^0 = 1`, `a^1 = a`.
+
+We do normalize `a^0` and `a^1` when converting expressions into polynomials,
+but we need to normalize them here when for other preprocessing steps such as
+`a / b = a*b⁻¹`. If `b` is of the form `c^1`, it will be treated as an
+atom in the comm ring module.
+-/
 builtin_simproc_decl expandPowAdd (_ ^ _) := fun e => do
   let_expr HPow.hPow α nat α' _ a k := e | return .continue
-  let_expr HAdd.hAdd _ _ _ _ m n := k | return .continue
   let_expr Nat ← nat | return .continue
-  unless (← isDefEq α α') do return .continue
-  let u ← getLevel α
-  let some u ← decLevel? u | return .continue
-  let semiring := mkApp (mkConst ``Grind.Semiring [u]) α
-  let .some semiringInst ← trySynthInstance semiring | return .continue
-  let pwFn := e.appFn!.appFn!
-  let r ← mkMul (mkApp2 pwFn a m) (mkApp2 pwFn a n)
-  let h := mkApp5 (mkConst ``Grind.Semiring.pow_add [u]) α semiringInst a m n
-  return .visit { expr := r, proof? := some h }
+  if let some k ← getNatValue? k then
+    if k == 0 then
+      unless (← isDefEq α α') do return .continue
+      let some h ← mkSemiringThm ``Grind.Semiring.pow_zero α | return .continue
+      let r ← mkNumeral α 1
+      return .done { expr := r, proof? := some (mkApp h a) }
+    else if k == 1 then
+      unless (← isDefEq α α') do return .continue
+      let some h ← mkSemiringThm ``Grind.Semiring.pow_one α | return .continue
+      return .done { expr := a, proof? := some (mkApp h a) }
+    else
+      return .continue
+  else
+    let_expr HAdd.hAdd _ _ _ _ m n := k | return .continue
+    unless (← isDefEq α α') do return .continue
+    let some h ← mkSemiringThm ``Grind.Semiring.pow_add α | return .continue
+    let pwFn := e.appFn!.appFn!
+    let r ← mkMul (mkApp2 pwFn a m) (mkApp2 pwFn a n)
+    return .visit { expr := r, proof? := some (mkApp3 h a m n) }
 
 def addSimproc (s : Simprocs) : CoreM Simprocs := do
   s.add ``expandPowAdd (post := true)

tests/lean/run/grind_pow_zero.lean

@@ -1,7 +1,9 @@
 open Lean Grind
 
-example [CommRing α] (a : α) : a^0 = 1 := by
-  grind
+example [CommRing α] (a : α) : a^0 = 1 := by grind
 
-example [CommSemiring α] [AddRightCancel α] (a : α) : a^0 = 1 := by
-  grind
+example [CommSemiring α] [AddRightCancel α] (a : α) : a^0 = 1 := by grind
+example [CommRing α] (a : α) : a^1 = a := by grind
+example [CommRing α] (a : α) : a^2 = a*a := by grind
+
+example [Field α] (a : α) : b ≠ 0 → a ≠ 0 → a * (b / a) / b = 1 := by grind