feat: Rabinowitsch transformation in grind (#8789)

This PR implements the Rabinowitsch transformation for `Field`
disequalities in `grind`. For example, this transformation is necessary
for solving:
```lean
example [Field α] (a : α) : a^2 = 0 → a = 0 := by
  grind
```

Author: leodemoura

src/Init/Grind/CommRing/Poly.lean

@@ -1249,7 +1249,7 @@ open Classical in
 theorem inv_split {α} [Field α] (a : α) : if a = 0 then a⁻¹ = 0 else a * a⁻¹ = 1 := by
   split
   next h => simp [h, Field.inv_zero]
-  next h => rw [CommRing.mul_comm, Field.inv_mul_cancel h]
+  next h => rw [Field.mul_inv_cancel h]
 
 def one_eq_zero_unsat_cert (p : Poly) :=
   p == .num 1 || p == .num (-1)
@@ -1259,6 +1259,16 @@ theorem one_eq_zero_unsat {α} [Field α] (ctx : Context α) (p : Poly) : one_eq
   next => rw [Eq.comm]; apply Field.zero_ne_one
   next => rw [← neg_eq_zero, neg_neg, Eq.comm]; apply Field.zero_ne_one
 
+theorem diseq_to_eq {α} [Field α] (a b : α) : a ≠ b → (a - b)*(a - b)⁻¹ = 1 := by
+  intro h
+  have : a - b ≠ 0 := by
+    intro h'; rw [Ring.sub_eq_zero_iff.mp h'] at h
+    contradiction
+  exact Field.mul_inv_cancel this
+
+theorem diseq0_to_eq {α} [Field α] (a : α) : a ≠ 0 → a*a⁻¹ = 1 := by
+  exact Field.mul_inv_cancel
+
 end CommRing
 
 end Lean.Grind

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

@@ -39,5 +39,6 @@ builtin_initialize registerTraceClass `grind.debug.ring.check
 builtin_initialize registerTraceClass `grind.debug.ring.impEq
 builtin_initialize registerTraceClass `grind.debug.ring.simpBasis
 builtin_initialize registerTraceClass `grind.debug.ring.basis
+builtin_initialize registerTraceClass `grind.debug.ring.rabinowitsch
 
 end Lean

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

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Var
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 
 namespace Lean.Meta.Grind.Arith.CommRing
 /-!
@@ -16,13 +17,7 @@ variable [Monad M] [MonadGetRing M]
 
 def denoteNum (k : Int) : M Expr := do
   let ring ← getRing
-  let n := mkRawNatLit k.natAbs
-  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [ring.u]) ring.type ring.semiringInst n
-  let n := mkApp3 (mkConst ``OfNat.ofNat [ring.u]) ring.type n ofNatInst
-  if k < 0 then
-    return mkApp ring.negFn n
-  else
-    return n
+  return denoteNumCore ring.u ring.type ring.semiringInst ring.negFn k
 
 def _root_.Lean.Grind.CommRing.Power.denoteExpr (pw : Power) : M Expr := do
   let x := (← getRing).vars[pw.x]!

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

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Lean.Meta.Tactic.Grind.ProveEq
 import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
@@ -282,6 +283,36 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
     let p ← (ra.sub rb).toPolyM
     addNewEq (← mkEqCnstr p (.core a b ra rb))
 
+private def pre (e : Expr) : GoalM Expr := do
+  -- We must canonicalize because the instances generated by this module may not match
+  -- the ones selected by the canonicalizer
+  shareCommon (← canon e)
+
+private def diseqToEq (a b : Expr) : RingM Unit := do
+  -- Rabinowitsch transformation
+  let gen := max (← getGeneration a) (← getGeneration b)
+  let ring ← getRing
+  let some fieldInst := ring.fieldInst? | unreachable!
+  let e ← pre <| mkApp2 ring.subFn a b
+  modifyRing fun s => { s with invSet := s.invSet.insert e }
+  let eInv ← pre <| mkApp (← getRing).invFn?.get! e
+  let lhs ← pre <| mkApp2 ring.mulFn e eInv
+  internalize lhs gen none
+  trace[grind.debug.ring.rabinowitsch] "{lhs}"
+  pushEq lhs ring.one <| mkApp5 (mkConst ``Grind.CommRing.diseq_to_eq [ring.u]) ring.type fieldInst a b (← mkDiseqProof a b)
+
+private def diseqZeroToEq (a b : Expr) : RingM Unit := do
+  -- Rabinowitsch transformation for `b = 0` case
+  let gen ← getGeneration a
+  let ring ← getRing
+  let some fieldInst := ring.fieldInst? | unreachable!
+  modifyRing fun s => { s with invSet := s.invSet.insert a }
+  let aInv ← pre <| mkApp (← getRing).invFn?.get! a
+  let lhs ← pre <| mkApp2 ring.mulFn a aInv
+  internalize lhs gen none
+  trace[grind.debug.ring.rabinowitsch] "{lhs}"
+  pushEq lhs ring.one <| mkApp4 (mkConst ``Grind.CommRing.diseq0_to_eq [ring.u]) ring.type fieldInst a (← mkDiseqProof a b)
+
 @[export lean_process_ring_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
   let some ringId ← inSameRing? a b | return ()
@@ -290,6 +321,13 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
     let some ra ← toRingExpr? a | return ()
     let some rb ← toRingExpr? b | return ()
     let p ← (ra.sub rb).toPolyM
+    if (← isField) then
+      unless p matches .num _ do
+        if rb matches .num 0 then
+          diseqZeroToEq a b
+        else
+          diseqToEq a b
+        return ()
     addNewDiseq {
       lhs := a, rhs := b
       rlhs := ra, rrhs := rb

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

@@ -35,12 +35,13 @@ private def isForbiddenParent (parent? : Option Expr) : Bool :=
       -- Remark: `HDiv` should appear in `getType?` as soon as we add support for `Field`,
       -- `LE.le` linear combinations
       match_expr parent with
+      | LT.lt _ _ _ _ => true
       | LE.le _ _ _ _ => true
       | HDiv.hDiv _ _ _ _ _ _ => true
       | HMod.hMod _ _ _ _ _ _ => true
       | _ => false
   else
-    true
+    false
 
 private partial def toInt? (e : Expr) : RingM (Option Int) := do
   match_expr e with

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

@@ -10,6 +10,15 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
 
 namespace Lean.Meta.Grind.Arith.CommRing
 
+def denoteNumCore (u : Level) (type : Expr) (semiringInst : Expr) (negFn : Expr) (k : Int) : Expr :=
+  let n := mkRawNatLit k.natAbs
+  let ofNatInst := mkApp3 (mkConst ``Grind.Semiring.ofNat [u]) type semiringInst n
+  let n := mkApp3 (mkConst ``OfNat.ofNat [u]) type n ofNatInst
+  if k < 0 then
+    mkApp negFn n
+  else
+    n
+
 private def internalizeFn (fn : Expr) : GoalM Expr := do
   shareCommon (← canon fn)
 
@@ -103,6 +112,10 @@ def getRingId? (type : Expr) : GoalM (Option Nat) := do
   else
     let id? ← go?
     modify' fun s => { s with typeIdOf := s.typeIdOf.insert { expr := type } id? }
+    if let some id := id? then
+      -- Internalize helper constants
+      let ring := (← get').rings[id]!
+      internalize ring.one 0
     return id?
 where
   go? : GoalM (Option Nat) := do
@@ -142,14 +155,15 @@ where
     let powFn ← getPowFn type u semiringInst
     let intCastFn ← getIntCastFn type u ringInst
     let natCastFn ← getNatCastFn type u semiringInst
-    let (invFn?, divFn?) ← if fieldInst?.isSome then
-      pure (some (← getInvFn type u), some (← getDivFn type u))
+    let invFn? ← if fieldInst?.isSome then
+      pure (some (← getInvFn type u))
     else
-      pure (none, none)
+      pure none
+    let one ← shareCommon <| (← canon <| denoteNumCore u type semiringInst negFn 1)
     let id := (← get').rings.size
     let ring : Ring := {
       id, type, u, semiringInst, ringInst, commSemiringInst, commRingInst, charInst?, noZeroDivInst?, fieldInst?,
-      addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn, invFn?, divFn? }
+      addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn, invFn?, one }
     modify' fun s => { s with rings := s.rings.push ring }
     return some id
 

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

@@ -153,8 +153,7 @@ structure Ring where
   natCastFn      : Expr
   /-- Inverse if `fieldInst?` is `some inst` -/
   invFn?         : Option Expr
-  /-- Division if `fieldInst?` is `some inst` -/
-  divFn?         : Option Expr
+  one            : Expr
   /--
   Mapping from variables to their denotations.
   Remark each variable can be in only one ring.

tests/lean/grind/algebra/field_normalization.lean

@@ -2,30 +2,6 @@ open Lean.Grind
 
 variable (R : Type u) [Field R]
 
-example (a : R) : (1 / 2) * a = a / 2 := by grind
-example (a : R) : 2⁻¹ * a = a / 2 := by grind
-example (a : R) : a⁻¹⁻¹ = a := by grind
-
 example (a : R) : (2 * a)⁻¹ = a⁻¹ / 2 := by grind
 
-example [IsCharP R 0] (a : R) : a / 2 + a / 3 = 5 * a / 6 := by grind
-
-example (_ : x ≠ 0) (_ : z ≠ 0) : w / x + y / z = (w * z + y * x) / (x * z) := by grind
-example (_ : x * z ≠ 0) : w / x + y / z = (w * z + y * x) / (x * z) := by grind
-
-example {x y z w : R} (h : x / y = z / w) (hy : y ≠ 0) (hw : w ≠ 0) : x * w = z * y := by
-  grind
-
-example (a : R) (_ : 2 * a ≠ 0) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
-example [IsCharP R 0] (a : R) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
-example [NoNatZeroDivisors R] (a : R) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
 example (a : R) (_ : (2 : R) ≠ 0) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by grind
-
-example (a b : R) (_ : a ≠ 0) (_ : b ≠ 0) : a / (a / b) = b := by grind
-example (a b : R) (_ : a ≠ 0) : a / (a / b) = b := by grind
-
--- TODO: create a mock implementation of `ℚ` for testing purposes.
-variable (ℚ : Type) [Field ℚ] [IsCharP ℚ 0]
-
-example (x : ℚ) (h₀ : x ≠ 0) :
-    (4 / x)⁻¹ * ((3 * x^3) / x)^2 * ((1 / (2 * x))⁻¹)^3 = 18 * x^8 := by grind

tests/lean/grind/ring_regressions.lean

@@ -6,20 +6,3 @@ example (n : Nat) :
 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
-
-open Lean.Grind
-
-example [Field R] (x : R) (cos : R → R) :
-    (cos x ^ 2 + (2 * cos x ^ 2 - 1) ^ 2 + (4 * cos x ^ 3 - 3 * cos x) ^ 2 - 1) / 4 =
-      cos x * (cos x ^ 2 - 1 / 2) * (4 * cos x ^ 3 - 3 * cos x) := by
-  grind
-
-example [Field R] {sqrtTwo a b c : R} :
-    sqrtTwo / 32 * ((a - b) ^ 2 + (b - c) ^ 2 + (c - a) ^ 2 + (-(a + b + c)) ^ 2) ^ 2 =
-      9 * sqrtTwo / 32 * (a ^ 2 + b ^ 2 + c ^ 2) ^ 2 := by
-  grind
-
-example [Field R] [LinearOrder R] [Ring.IsOrdered R] (x y z : R) (hx : x > 0) (hy : y > 0) (hz : z > 0) (h : x * y * z ≥ 1) :
-    (x ^ 2 - y * z) / (x ^ 2 + y ^ 2 + z ^ 2) + (y ^ 2 - z * x) / (y ^ 2 + z ^ 2 + x ^ 2) +
-      (z ^ 2 - x * y) / (z ^ 2 + x ^ 2 + y ^ 2) =
-    1 / 2 * ((x - y) ^ 2 + (y - z) ^ 2 + (z - x) ^ 2) / (x ^ 2 + y ^ 2 + z ^ 2) := by grind

tests/lean/run/grind_const_pattern.lean

@@ -18,7 +18,7 @@ h : ¬a = 10
   [eqc] False propositions
     [prop] a = 10
   [cutsat] Assignment satisfying linear constraints
-    [assign] a := 1
+    [assign] a := 2
 -/
 #guard_msgs (error) in
 example : a = 5 + 5 := by
@@ -49,8 +49,8 @@ h : ¬f a = 11
   [eqc] False propositions
     [prop] f a = 11
   [cutsat] Assignment satisfying linear constraints
-    [assign] a := 2
-    [assign] f a := 1
+    [assign] a := 3
+    [assign] f a := 2
 -/
 #guard_msgs (error) in
 example : f a = 10 + 1 := by
@@ -75,9 +75,9 @@ h : ¬f x = 11
   [ematch] E-matching patterns
     [thm] fa: [f `[a]]
   [cutsat] Assignment satisfying linear constraints
-    [assign] x := 3
-    [assign] a := 2
-    [assign] f x := 1
+    [assign] x := 4
+    [assign] a := 3
+    [assign] f x := 2
 -/
 #guard_msgs (error) in
 example : f x = 10 + 1 := by