feat: cleanup denominators in grind linarith (#11375)

This PR adds support for cleaning up denominators in `grind linarith` when the type is a `Field`. Examples: ```lean open Std Lean.Grind section variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] example (a b : α) (h : a < b / 2) : 2 * a < b := by grind example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind example (a b : α) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind example (a b : α) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind example (a b : α) (h : a < b / (2^2 - 3/2 + -1 + 1/2)) : 2 * a < b := by grind end example (a b : Rat) (h : a < b / 2) : a + a < b := by grind example (a b : Rat) (h : a < b / 2) : a + a ≤ b := by grind example (a b : Rat) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind example (a b : Rat) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind ```
2025-11-25 21:21:55 -08:00 · 2025-11-25 21:21:55 -08:00 · 5ac0931c8f
commit 5ac0931c8f
parent 6f4bee8421
12 changed files with 317 additions and 25 deletions
--- a/src/Init/Grind/Ordered/Ring.lean
+++ b/src/Init/Grind/Ordered/Ring.lean
@ -236,20 +236,21 @@ instance [Ring R] [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R]

 end Preorder

+theorem mul_pos [LE R] [LT R] [IsPreorder R] [OrderedRing R] {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
+  simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
+
+theorem zero_le_one [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : (0 : R) ≤ 1 :=
+  Preorder.le_of_lt zero_lt_one
+
+theorem not_one_lt_zero [LE R] [LT R] [LawfulOrderLT R] [IsPreorder R] [OrderedRing R] : ¬ ((1 : R) < 0) :=
+  fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
+
 section PartialOrder

 variable [LE R] [LT R] [IsPartialOrder R] [OrderedRing R]

-theorem mul_pos {a b : R} (h₁ : 0 < a) (h₂ : 0 < b) : 0 < a * b := by
-  simpa [Semiring.zero_mul] using mul_lt_mul_of_pos_right h₁ h₂
-
 variable [LawfulOrderLT R]

-theorem zero_le_one : (0 : R) ≤ 1 := Preorder.le_of_lt zero_lt_one
-
-theorem not_one_lt_zero : ¬ ((1 : R) < 0) :=
-  fun h => Preorder.lt_irrefl (0 : R) (Preorder.lt_trans zero_lt_one h)
-
 theorem mul_le_mul_of_nonneg_left {a b c : R} (h : a ≤ b) (h' : 0 ≤ c) : c * a ≤ c * b := by
  rw [PartialOrder.le_iff_lt_or_eq] at h'
  cases h' with
--- a/src/Init/Grind/Ring/Basic.lean
+++ b/src/Init/Grind/Ring/Basic.lean
@ -204,6 +204,11 @@ theorem pow_add (a : α) (k₁ k₂ : Nat) : a ^ (k₁ + k₂) = a^k₁ * a^k₂
 theorem pow_add_congr (a r : α) (k k₁ k₂ : Nat) : k = k₁ + k₂ → a^k₁ * a^k₂ = r → a ^ k = r := by
  intros; subst k r; rw [pow_add]

+theorem one_pow (n : Nat) : (1 : α) ^ n = 1 := by
+  induction n
+  next => simp [pow_zero]
+  next => simp [pow_succ, *, mul_one]
+
 theorem natCast_pow (x : Nat) (k : Nat) : ((x ^ k : Nat) : α) = (x : α) ^ k := by
  induction k
  next => simp [pow_zero, Nat.pow_zero, natCast_one]
@ -376,6 +381,11 @@ variable {α : Type u} [CommSemiring α]
 theorem mul_left_comm (a b c : α) : a * (b * c) = b * (a * c) := by
  rw [← mul_assoc, ← mul_assoc, mul_comm a]

+theorem mul_pow (a b : α) (n : Nat) : (a*b)^n = a^n * b^n := by
+  induction n
+  next => simp [pow_zero, mul_one]
+  next n ih => simp [pow_succ, ih, mul_comm, mul_assoc, mul_left_comm]
+
 end CommSemiring

 open Semiring hiding add_comm add_assoc add_zero
--- a/src/Init/Grind/Ring/CommSolver.lean
+++ b/src/Init/Grind/Ring/CommSolver.lean
@ -656,6 +656,29 @@ noncomputable def Expr.toPoly_k (e : Expr) : Poly :=
      (k.beq 0))
    e

+def Mon.degreeOf (m : Mon) (x : Var) : Nat :=
+  match m with
+  | .unit => 0
+  | .mult pw m => bif pw.x == x then pw.k else degreeOf m x
+
+def Mon.cancelVar (m : Mon) (x : Var) : Mon :=
+  match m with
+  | .unit => .unit
+  | .mult pw m => bif pw.x == x then m else .mult pw (cancelVar m x)
+
+def Poly.cancelVar' (c : Int) (x : Var) (p : Poly) (acc : Poly) : Poly :=
+  match p with
+  | .num k => acc.addConst k
+  | .add k m p =>
+    let n := m.degreeOf x
+    bif n > 0 && c^n ∣ k then
+      cancelVar' c x p (acc.insert (k / (c^n)) (m.cancelVar x))
+    else
+      cancelVar' c x p (acc.insert k m)
+
+def Poly.cancelVar (c : Int) (x : Var) (p : Poly) : Poly :=
+  cancelVar' c x p (.num 0)
+
@[simp] theorem Expr.toPoly_k_eq_toPoly (e : Expr) : e.toPoly_k = e.toPoly := by
  induction e <;> simp only [toPoly, toPoly_k]
  next a ih => rw [Poly.mulConst_k_eq_mulConst]; congr
@ -1175,6 +1198,72 @@ theorem Expr.eq_of_toPoly_nc_eq {α} [Ring α] (ctx : Context α) (a b : Expr) (
  simp [denote_toPoly_nc] at h
  assumption

+section
+attribute [local simp] Semiring.pow_zero Semiring.mul_one Semiring.one_mul cond_eq_ite
+
+theorem Mon.denote_cancelVar [CommSemiring α] (ctx : Context α) (m : Mon) (x : Var)
+    : m.denote ctx = x.denote ctx ^ (m.degreeOf x) * (m.cancelVar x).denote ctx := by
+  fun_induction cancelVar <;> simp [degreeOf]
+  next h =>
+    simp at h; simp [*, denote, Power.denote_eq]
+  next h ih =>
+    simp at h; simp [*, denote, Semiring.mul_assoc, CommSemiring.mul_comm, CommSemiring.mul_left_comm]
+
+theorem Poly.denote_cancelVar' {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var) (acc : Poly)
+    : c ≠ 0 → c * x.denote ctx = 1 → (p.cancelVar' c x acc).denote ctx = p.denote ctx + acc.denote ctx := by
+  intro h₁ h₂
+  fun_induction cancelVar'
+  next acc k => simp [denote_addConst, denote, Semiring.add_comm]
+  next h ih =>
+    simp [ih, denote_insert, denote]
+    conv => rhs; rw [Mon.denote_cancelVar (x := x)]
+    simp [← Semiring.add_assoc]
+    congr 1
+    rw [Semiring.add_comm, Ring.zsmul_eq_intCast_mul,]
+    congr 1
+    simp +zetaDelta [Int.dvd_def] at h
+    have ⟨d, h⟩ := h.2
+    simp +zetaDelta [h]
+    rw [Int.mul_ediv_cancel_left _ (Int.pow_ne_zero h₁)]
+    rw [Ring.intCast_mul]
+    conv => rhs; lhs; rw [CommSemiring.mul_comm]
+    rw [Semiring.mul_assoc, Ring.intCast_pow]
+    congr 1
+    rw [← Semiring.mul_assoc, ← CommSemiring.mul_pow, h₂, Semiring.one_pow, Semiring.one_mul]
+  next ih =>
+    simp [ih, denote_insert, denote, Ring.zsmul_eq_intCast_mul, Semiring.add_assoc,
+      Semiring.add_comm, add_left_comm]
+
+theorem Poly.denote_cancelVar {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Int) (x : Var)
+    : c ≠ 0 → c * x.denote ctx = 1 → (p.cancelVar c x).denote ctx = p.denote ctx := by
+  intro h₁ h₂
+  have := denote_cancelVar' ctx p c x (.num 0) h₁ h₂
+  rw [cancelVar, this, denote, Ring.intCast_zero, Semiring.add_zero]
+
+noncomputable def cancel_var_cert (c : Int) (x : Var) (p₁ p₂ : Poly) : Bool :=
+  c != 0 && p₂.beq' (p₁.cancelVar c x)
+
+theorem eq_cancel_var {α} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
+    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx = 0 → p₂.denote ctx = 0 := by
+  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
+  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
+
+theorem diseq_cancel_var {α} [CommRing α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
+    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx ≠ 0 → p₂.denote ctx ≠ 0 := by
+  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
+  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
+
+theorem le_cancel_var {α} [CommRing α] [LE α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
+    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx ≤ 0 → p₂.denote ctx ≤ 0 := by
+  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
+  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
+
+theorem lt_cancel_var {α} [CommRing α] [LT α] (ctx : Context α) (c : Int) (x : Var) (p₁ p₂ : Poly)
+    : cancel_var_cert c x p₁ p₂ → c * x.denote ctx = 1 → p₁.denote ctx < 0 → p₂.denote ctx < 0 := by
+  simp [cancel_var_cert]; intros h₁ _ h₂ _; subst p₂
+  simp [Poly.denote_cancelVar ctx p₁ c x h₁ h₂]; assumption
+
+end
 /-!
 Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
 -/
@ -1398,6 +1487,21 @@ theorem mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : P
  simp [mul_cert]; intro _ h; subst p
  simp [Poly.denote_mulConst, *, mul_zero]

+theorem eq_mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+    : mul_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by
+  apply mul
+
+noncomputable def mul_ne_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
+  k != 0 && (p₁.mulConst_k k |>.beq' p)
+
+theorem diseq_mul {α} [CommRing α] [NoNatZeroDivisors α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+    : mul_ne_cert p₁ k p → p₁.denote ctx ≠ 0 → p.denote ctx ≠ 0 := by
+  simp [mul_ne_cert]; intro h₁ _ h₂; subst p
+  simp [Poly.denote_mulConst]; intro h₃
+  rw [← zsmul_eq_intCast_mul] at h₃
+  have := no_int_zero_divisors h₁ h₃
+  contradiction
+
 theorem inv {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (p : Poly)
    : mul_cert p₁ (-1) p → p₁.denote ctx = 0 → p.denote ctx = 0 :=
  mul ctx p₁ (-1) p
@ -1608,6 +1712,16 @@ theorem le_int_module {α} [CommRing α] [LE α] (ctx : Context α) (p : Poly)
    : p.denote ctx ≤ 0 → p.denoteAsIntModule ctx ≤ 0 := by
  simp [Poly.denoteAsIntModule_eq_denote]

+noncomputable def mul_ineq_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool :=
+  k > 0 && (p₁.mulConst_k k |>.beq' p)
+
+theorem le_mul {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+    : mul_ineq_cert p₁ k p → p₁.denote ctx ≤ 0 → p.denote ctx ≤ 0 := by
+  simp [mul_ineq_cert]; intro h₁ _ h₂; subst p; simp [Poly.denote_mulConst]
+  replace h₂ := zsmul_nonpos (Int.le_of_lt h₁) h₂
+  simp [Ring.zsmul_eq_intCast_mul] at h₂
+  assumption
+
 theorem lt_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
    : core_cert lhs rhs p → lhs.denote ctx < rhs.denote ctx → p.denote ctx < 0 := by
  simp [core_cert]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote]
@ -1619,6 +1733,13 @@ theorem lt_int_module {α} [CommRing α] [LT α] (ctx : Context α) (p : Poly)
    : p.denote ctx < 0 → p.denoteAsIntModule ctx < 0 := by
  simp [Poly.denoteAsIntModule_eq_denote]

+theorem lt_mul {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly)
+    : mul_ineq_cert p₁ k p → p₁.denote ctx < 0 → p.denote ctx < 0 := by
+  simp [mul_ineq_cert]; intro h₁ _ h₂; subst p; simp [Poly.denote_mulConst]
+  replace h₂ := zsmul_neg_iff k h₂ |>.mpr h₁
+  simp [Ring.zsmul_eq_intCast_mul] at h₂
+  assumption
+
 theorem not_le_norm {α} [CommRing α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly)
    : core_cert rhs lhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → p.denote ctx < 0 := by
  simp [core_cert]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]
@ -1642,6 +1763,13 @@ theorem inv_int_eq [Field α] [IsCharP α 0] (b : Int) : b != 0 → (denoteInt b
    have := IsCharP.intCast_eq_zero_iff (α := α) 0 b; simp [*] at this
  rw [Field.mul_inv_cancel this]

+theorem intCast_eq_denoteInt [Field α] (b : Int) : (IntCast.intCast b : α) = denoteInt b := by
+  simp [denoteInt_eq]
+
+theorem inv_int_eq' [Field α] [IsCharP α 0] (b : Int) : b != 0 → (IntCast.intCast b : α) * (denoteInt b)⁻¹ = 1 := by
+  rw [intCast_eq_denoteInt]
+  apply inv_int_eq
+
 theorem inv_int_eqC {α c} [Field α] [IsCharP α c] (b : Int) : b % c != 0 → (denoteInt b : α) * (denoteInt b)⁻¹ = 1 := by
  simp; intro h
  have : (denoteInt b : α) ≠ 0 := by
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Poly.lean
@ -274,4 +274,12 @@ where
    | .num k => .add acc (.num k)
    | .add k m p => go p (.add acc (goTerm k m))

+def Poly.maxDegreeOf (p : Poly) (x : Var) : Nat :=
+  go p 0
+where
+  go (p : Poly) (max : Nat) : Nat :=
+    match p with
+    | .num _ => max
+    | .add _ m p => go p (Nat.max max (m.degreeOf x))
+
 end Lean.Grind.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/SafePoly.lean
@ -115,4 +115,23 @@ def _root_.Lean.Grind.CommRing.Poly.spolM (p₁ p₂ : Poly) : RingM Grind.CommR
    return { spol, m₁, m₂, k₁ := c₁, k₂ := c₂ }
  | _, _ => return {}

+/-- Returns `some (val, x)` if `m` contains a variable `x` whose the denotation is `val⁻¹`. -/
+def _root_.Lean.Grind.CommRing.Mon.findInvNumeralVar? (m : Mon) : RingM (Option (Nat × Var)) := do
+  match m with
+  | .unit => return none
+  | .mult pw m =>
+    let e := (← getRing).vars[pw.x]!
+    let_expr Inv.inv _ _ a := e | m.findInvNumeralVar?
+    let_expr OfNat.ofNat _ n _ := a | m.findInvNumeralVar?
+    let some n ← getNatValue? n | m.findInvNumeralVar?
+    return some (n, pw.x)
+
+/-- Returns `some (val, x)` if `p` contains a variable `x` whose the denotation is `val⁻¹`. -/
+def _root_.Lean.Grind.CommRing.Poly.findInvNumeralVar? (p : Poly) : RingM (Option (Nat × Var)) := do
+  match p with
+  | .num _ => return none
+  | .add _ m p =>
+    let some r ← m.findInvNumeralVar? | p.findInvNumeralVar?
+    return some r
+
 end Lean.Meta.Grind.Arith.CommRing
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Den.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Den.lean
@ -0,0 +1,43 @@
+/-
+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
+public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.CommRing.SafePoly
+namespace Lean.Meta.Grind.Arith.Linear
+
+partial def cleanupDenominators' (c : α)
+    (getPoly : α → CommRing.Poly)
+    (updateCnstr : α → CommRing.Poly → Int → Var → Nat → α)
+    : LinearM α := do
+  let s ← getStruct
+  if s.fieldInst?.isNone then return c
+  let some (_, char) := s.charInst? | return c
+  unless char == 0 do return c
+  withRingM <| go c
+where
+  go (c : α) : CommRing.RingM α := do
+    let p := getPoly c
+    let some (val, x) ← p.findInvNumeralVar? | return c
+    let n := p.maxDegreeOf x
+    let p := p.mulConst (val ^ n)
+    let p := p.cancelVar val x
+    go (updateCnstr c p val x n)
+
+public def RingIneqCnstr.cleanupDenominators (c : RingIneqCnstr) : LinearM RingIneqCnstr :=
+  cleanupDenominators' c (·.p) fun c p val x n => { c with p, h := .cancelDen c val x n }
+
+public def RingEqCnstr.cleanupDenominators (c : RingEqCnstr) : LinearM RingEqCnstr :=
+  cleanupDenominators' c (·.p) fun c p val x n => { c with p, h := .cancelDen c val x n }
+
+public def RingDiseqCnstr.cleanupDenominators (c : RingDiseqCnstr) : LinearM RingDiseqCnstr := do
+  let s ← getStruct
+  if s.noNatDivInst?.isNone then return c
+  cleanupDenominators' c (·.p) fun c p val x n => { c with p, h := .cancelDen c val x n }
+
+end Lean.Meta.Grind.Arith.Linear
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean
@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.Linear.Den
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
 import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
@ -48,6 +49,8 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue :
  if eqTrue then
    let p := (lhs.sub rhs).toPoly
    let c : RingIneqCnstr := { p, strict, h := .core e lhs rhs }
+    let c ← c.cleanupDenominators
+    let p := c.p
    let lhs ← p.toIntModuleExpr generation
    let some lhs ← reify? lhs (skipVar := false) generation | return ()
    let p := lhs.norm
@ -57,6 +60,8 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue :
    let p := (rhs.sub lhs).toPoly
    let strict := !strict
    let c : RingIneqCnstr := { p, strict, h := .notCore e lhs rhs }
+    let c ← c.cleanupDenominators
+    let p := c.p
    let lhs ← p.toIntModuleExpr generation
    let some lhs ← reify? lhs (skipVar := false) generation | return ()
    let p := lhs.norm
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean
@ -204,6 +204,14 @@ private def mkCommRingThmPrefix (declName : Name) : ProofM Expr := do
  let s ← getStruct
  return mkApp3 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getRingContext)

+/--
+Returns the prefix of a theorem with name `declName` where the first four arguments are
+`{α} [CommRing α] [NoNatZeroDivisors α] (rctx : Context α)`
+-/
+private def mkCommRingNoNatDivThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp4 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getNoNatDivInst) (← getRingContext)
+
 /--
 Returns the prefix of a theorem with name `declName` where the first four arguments are
 `{α} [CommRing α] [LE α] (rctx : Context α)`
@ -244,6 +252,14 @@ private def mkCommRingLinOrdThmPrefix (declName : Name) : ProofM Expr := do
  let s ← getStruct
  return mkApp8 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getLTInst) (← getLawfulOrderLTInst) (← getIsLinearOrderInst) (← getOrderedRingInst) (← getRingContext)

+/--
+Returns the prefix of a theorem with name `declName` where the first three arguments are
+`{α} [Field α] [IsCharP α 0]`
+-/
+private def mkFieldChar0ThmPrefix (declName : Name) : ProofM Expr := do
+  let s ← getStruct
+  return mkApp3 (mkConst declName [s.u]) s.type s.fieldInst?.get! s.charInst?.get!.1
+
 partial def RingIneqCnstr.toExprProof (c' : RingIneqCnstr) : ProofM Expr := do
  match c'.h with
  | .core e lhs rhs =>
@ -252,6 +268,20 @@ partial def RingIneqCnstr.toExprProof (c' : RingIneqCnstr) : ProofM Expr := do
  | .notCore e lhs rhs =>
    let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm)
    return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
+  | .cancelDen c val x n =>
+    let h ← if c.strict then
+      mkCommRingLawfulPreOrdThmPrefix ``Grind.CommRing.lt_mul
+    else
+      mkCommRingPreOrdThmPrefix ``Grind.CommRing.le_mul
+    let p₁ := c.p.mulConst (val^n)
+    let p₁ ← mkRingPolyDecl p₁
+    let h := mkApp5 h (← mkRingPolyDecl c.p) (toExpr (val^n)) p₁ eagerReflBoolTrue (← c.toExprProof)
+    let h_eq_one := mkApp2 (← mkFieldChar0ThmPrefix ``Grind.CommRing.inv_int_eq') (toExpr val) eagerReflBoolTrue
+    let h' ← if c.strict then
+      mkCommRingLTThmPrefix ``Grind.CommRing.lt_cancel_var
+    else
+      mkCommRingLEThmPrefix ``Grind.CommRing.le_cancel_var
+    return mkApp7 h' (toExpr val) (toExpr x) p₁ (← mkRingPolyDecl c'.p) eagerReflBoolTrue h_eq_one h

 partial def RingEqCnstr.toExprProof (c' : RingEqCnstr) : ProofM Expr := do
  match c'.h with
@ -262,12 +292,28 @@ partial def RingEqCnstr.toExprProof (c' : RingEqCnstr) : ProofM Expr := do
    let h ← c.toExprProof
    let h' ← mkCommRingThmPrefix ``Grind.CommRing.Stepwise.inv
    return mkApp4 h' (← mkRingPolyDecl c.p) (← mkRingPolyDecl c'.p) eagerReflBoolTrue h
+  | .cancelDen c val x n =>
+    let h ← mkCommRingThmPrefix ``Grind.CommRing.Stepwise.eq_mul
+    let p₁ := c.p.mulConst (val^n)
+    let p₁ ← mkRingPolyDecl p₁
+    let h := mkApp5 h (← mkRingPolyDecl c.p) (toExpr (val^n)) p₁ eagerReflBoolTrue (← c.toExprProof)
+    let h_eq_one := mkApp2 (← mkFieldChar0ThmPrefix ``Grind.CommRing.inv_int_eq') (toExpr val) eagerReflBoolTrue
+    let h' ← mkCommRingThmPrefix ``Grind.CommRing.eq_cancel_var
+    return mkApp7 h' (toExpr val) (toExpr x) p₁ (← mkRingPolyDecl c'.p) eagerReflBoolTrue h_eq_one h

 partial def RingDiseqCnstr.toExprProof (c' : RingDiseqCnstr) : ProofM Expr := do
  match c'.h with
  | .core a b lhs rhs =>
    let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_norm
    return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (← mkDiseqProof a b)
+  | .cancelDen c val x n =>
+    let h ← mkCommRingNoNatDivThmPrefix ``Grind.CommRing.Stepwise.diseq_mul
+    let p₁ := c.p.mulConst (val^n)
+    let p₁ ← mkRingPolyDecl p₁
+    let h := mkApp5 h (← mkRingPolyDecl c.p) (toExpr (val^n)) p₁ eagerReflBoolTrue (← c.toExprProof)
+    let h_eq_one := mkApp2 (← mkFieldChar0ThmPrefix ``Grind.CommRing.inv_int_eq') (toExpr val) eagerReflBoolTrue
+    let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_cancel_var
+    return mkApp7 h' (toExpr val) (toExpr x) p₁ (← mkRingPolyDecl c'.p) eagerReflBoolTrue h_eq_one h

 mutual
 partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean
@ -8,6 +8,7 @@ prelude
 public import Lean.Meta.Tactic.Grind.Arith.Linear.LinearM
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.Linear.Den
 import Lean.Meta.Tactic.Grind.Arith.Linear.Var
 import Lean.Meta.Tactic.Grind.Arith.Linear.StructId
 import Lean.Meta.Tactic.Grind.Arith.Linear.Reify
@ -56,6 +57,8 @@ private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do
  let generation := max (← getGeneration a) (← getGeneration b)
  let p := (lhs.sub rhs).toPoly
  let c : RingEqCnstr := { p, h := .core a b lhs rhs }
+  let c ← c.cleanupDenominators
+  let p := c.p
  let lhs ← p.toIntModuleExpr generation
  let some lhs ← reify? lhs (skipVar := false) generation | return ()
  let p := lhs.norm
@ -274,6 +277,8 @@ private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do
  let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return ()
  let p := (lhs.sub rhs).toPoly
  let c : RingDiseqCnstr := { p, h := .core a b lhs rhs }
+  let c ← c.cleanupDenominators
+  let p := c.p
  let generation := max (← getGeneration a) (← getGeneration b)
  let lhs ← p.toIntModuleExpr generation
  let some lhs ← reify? lhs (skipVar := false) generation | return ()
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean
@ -28,7 +28,7 @@ structure RingIneqCnstr where
 inductive RingIneqCnstrProof where
  | core (e : Expr) (lhs rhs : Grind.CommRing.Expr)
  | notCore (e : Expr) (lhs rhs : Grind.CommRing.Expr)
-  -- **TODO**: cleanup denominator proof step
+  | cancelDen (c : RingIneqCnstr) (val : Int) (x : Var) (n : Var)
 end

 mutual
@ -40,7 +40,7 @@ structure RingEqCnstr where
 inductive RingEqCnstrProof where
  | core (a b : Expr) (ra rb : Grind.CommRing.Expr)
  | symm (c : RingEqCnstr)
-  -- **TODO**: cleanup denominator proof step
+  | cancelDen (c : RingEqCnstr) (val : Int) (x : Var) (n : Var)
 end

 mutual
@ -51,7 +51,7 @@ structure RingDiseqCnstr where

 inductive RingDiseqCnstrProof where
  | core (a b : Expr) (ra rb : Grind.CommRing.Expr)
-  -- **TODO**: cleanup denominator proof step
+  | cancelDen (c : RingDiseqCnstr) (val : Int) (x : Var) (n : Var)
 end

 mutual
--- a/tests/lean/grind/algebra/linarith_field.lean
+++ b/tests/lean/grind/algebra/linarith_field.lean
@ -1,14 +0,0 @@
-open Std Lean.Grind
-
-variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α]
-
-example (a b : α) (h : a < b / 2) : 2 * a < b := by grind
-example (a b : α) (h : a < b / 2) : a + a < b := by grind
-example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind
-example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind
-example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind
-example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind
-
-example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
-
-example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind
--- a/tests/lean/run/grind_clean_den.lean
+++ b/tests/lean/run/grind_clean_den.lean
@ -0,0 +1,41 @@
+open Std Lean.Grind
+
+section
+variable {α : Type} [Field α] [LE α] [LT α] [LawfulOrderLT α] [IsLinearOrder α] [OrderedRing α]
+
+example (a b : α) (h : a < b * (3⁻¹)^2) : 9 * a < b := by grind
+example (a b : α) (h : a ≤ b * (3⁻¹)^2) : 9 * a ≤ b := by grind
+example (a b : α) (h : a < b / 2) : 2 * a < b := by grind
+example (a b : α) (h : a < b / 2) : a + a < b := by grind
+example (a b : α) (h : a < b / 2) : 2 * a ≤ b := by grind
+example (a b : α) (h : a < b / 2) : a + a ≤ b := by grind
+example (a b : α) (h : a ≤ b / 2) : 2 * a ≤ b := by grind
+example (a b : α) (h : a ≤ b / 2) : a + a ≤ b := by grind
+example (a b : α) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
+example (a b : α) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind
+
+example (a b : α) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind
+example (a b : α) (h : a = b / 2) : a + a ≤ b := by grind
+example (a b : α) (h : a ≠ b) : a < b ∨ a > b := by grind
+variable [NoNatZeroDivisors α]
+example (a b : α) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind
+example (a b : α) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind
+
+example (a b : α) (h : a < b / (2^2 - 3/2 + -1 + 1/2)) : 2 * a < b := by grind
+
+end
+
+example (a b : Rat) (h : a < b * (3⁻¹)^2) : 9 * a < b := by grind
+example (a b : Rat) (h : a ≤ b * (3⁻¹)^2) : 9 * a ≤ b := by grind
+example (a b : Rat) (h : a < b / 2) : 2 * a < b := by grind
+example (a b : Rat) (h : a < b / 2) : a + a < b := by grind
+example (a b : Rat) (h : a < b / 2) : 2 * a ≤ b := by grind
+example (a b : Rat) (h : a < b / 2) : a + a ≤ b := by grind
+example (a b : Rat) (h : a ≤ b / 2) : 2 * a ≤ b := by grind
+example (a b : Rat) (h : a ≤ b / 2) : a + a ≤ b := by grind
+example (a b : Rat) (_ : 0 ≤ a) (h : a ≤ b) : a / 7 ≤ b / 2 := by grind
+example (a b : Rat) (_ : b < 0) (h : a < b) : (3/2) * a < (5/4) * b := by grind
+example (a b : Rat) (h : a = b * (3⁻¹)^2) : 9 * a ≤ b := by grind
+example (a b : Rat) (h : a = b / 2) : a + a ≤ b := by grind
+example (a b : Rat) (h : a ≠ b * (3⁻¹)^2) : 9 * a < b ∨ 9 * a > b := by grind
+example (a b : Rat) (h : a / 2 ≠ b / 9) : 9 * a < 2 * b ∨ 9 * a > 2 * b := by grind