From aef4a29148c08a99fbcd50d7e2fdf1be77db0660 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 Jun 2025 18:42:49 -0400 Subject: [PATCH] feat: `Field` support in `grind ring` (#8777) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR implements basic `Field` support in the commutative ring module in `grind`. It is just division by numerals for now. Examples: ```lean open Lean Grind example [Field α] [IsCharP α 0] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c := by grind example [Field α] (a b : α) : b = 0 → (a + a) / 0 = b := by grind example [Field α] [IsCharP α 3] (a b : α) : a/3 = b → b = 0 := by grind example [Field α] [IsCharP α 7] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c + 7 := by grind example [Field R] [IsCharP R 0] (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 ``` --- src/Init/Grind/CommRing/Poly.lean | 29 ++++++- .../Grind/Arith/CommRing/DenoteExpr.lean | 2 +- .../Grind/Arith/CommRing/Internalize.lean | 72 +++++++++++++++++ .../Tactic/Grind/Arith/CommRing/RingId.lean | 80 ++++++++++--------- .../Tactic/Grind/Arith/CommRing/Types.lean | 14 +++- tests/lean/run/grind_field_div.lean | 18 +++++ 6 files changed, 172 insertions(+), 43 deletions(-) create mode 100644 tests/lean/run/grind_field_div.lean diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index e120ecff63..6ed19a0922 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -11,14 +11,13 @@ import Init.Data.Hashable import all Init.Data.Ord import Init.Data.RArray import Init.Grind.CommRing.Basic +import Init.Grind.CommRing.Field import Init.Grind.Ordered.Ring namespace Lean.Grind -namespace CommRing - -- These are no longer global instances, so we need to turn them on here. attribute [local instance] Semiring.natCast Ring.intCast - +namespace CommRing abbrev Var := Nat inductive Expr where @@ -1225,5 +1224,29 @@ theorem not_lt_norm' {α} [CommRing α] [Preorder α] [Ring.IsOrdered α] (ctx : rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h contradiction +theorem div_int_eq {α} [Field α] [IsCharP α 0] (a : α) (b : Int) : b != 0 → a = denoteInt b * (a / denoteInt b) := by + simp [Field.div_eq_mul_inv]; intro h + have : (denoteInt b : α) ≠ 0 := by + simp [denoteInt_eq]; intro h + have := IsCharP.intCast_eq_zero_iff (α := α) 0 b; simp [*] at this + rw [CommRing.mul_comm, Semiring.mul_assoc, CommRing.mul_comm _ (denoteInt b), Field.mul_inv_cancel this, Semiring.mul_one] + +theorem div_int_eqC {α c} [Field α] [IsCharP α c] (a : α) (b : Int) : b % c != 0 → a = (denoteInt b) * (a / denoteInt b) := by + simp [Field.div_eq_mul_inv]; intro h + have : (denoteInt b : α) ≠ 0 := by + simp [denoteInt_eq]; intro h + have := IsCharP.intCast_eq_zero_iff (α := α) c b; simp [*] at this + rw [CommRing.mul_comm, Semiring.mul_assoc, CommRing.mul_comm _ (denoteInt b), Field.mul_inv_cancel this, Semiring.mul_one] + +theorem div_zero_eq {α} [Field α] (a : α) : a / 0 = 0 := by + simp [Field.div_eq_mul_inv, Field.inv_zero, Semiring.mul_zero] + +theorem div_zero_eqC {α c} [Field α] [IsCharP α c] (a : α) (b : Int) : b % c == 0 → (a / denoteInt b) = 0 := by + simp [Field.div_eq_mul_inv, denoteInt_eq]; intro h + have : (b : α) = 0 := by + have := IsCharP.intCast_eq_zero_iff (α := α) c b + simp [*] + simp [this, Field.div_eq_mul_inv, Field.inv_zero, Semiring.mul_zero] end CommRing + end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean index 6f9565c1a1..809be77240 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/DenoteExpr.lean @@ -14,7 +14,7 @@ Helper functions for converting reified terms back into their denotations. variable [Monad M] [MonadGetRing M] -private def denoteNum (k : Int) : M Expr := do +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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean index a8798320c7..d046b6581a 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean @@ -7,6 +7,7 @@ prelude import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify +import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr namespace Lean.Meta.Grind.Arith.CommRing @@ -41,8 +42,79 @@ private def isForbiddenParent (parent? : Option Expr) : Bool := else true +private partial def toInt? (e : Expr) : RingM (Option Int) := do + match_expr e with + | Neg.neg _ i a => + if isNegInst (← getRing) i then return (- .) <$> (← toInt? a) else return none + | IntCast.intCast _ i a => + if isIntCastInst (← getRing) i then getIntValue? a else return none + | NatCast.natCast _ i a => + if isNatCastInst (← getRing) i then + let some v ← getNatValue? a | return none + return some (Int.ofNat v) + else + return none + | OfNat.ofNat _ n _ => + let some v ← getNatValue? n | return none + return some (Int.ofNat v) + | _ => return none + +private def isDivInst (inst : Expr) : RingM Bool := do + let some fn := (← getRing).divFn? | return false + return isSameExpr fn.appArg! inst + +/-- +Given `e` of the form `@HDiv.hDiv _ _ _ inst a b`, +asserts `a = b * e` if `b` is a numeral. +Otherwise, asserts `b = 0 ∨ a = b * e` +-/ +private def processDiv (e inst a b : Expr) : RingM Unit := do + unless (← isDivInst inst) do return () + if (← getRing).divSet.contains (a, b) then return () + modifyRing fun s => { s with divSet := s.divSet.insert (a, b) } + if let some k ← toInt? b then + let ring ← getRing + let some fieldInst := ring.fieldInst? | return () + if k == 0 then + pushNewFact <| mkApp3 (mkConst ``Grind.CommRing.div_zero_eq [ring.u]) ring.type fieldInst a + else if (← hasChar) then + let (charInst, c) ← getCharInst + if c == 0 then + let expected ← mkEq a (mkApp2 ring.mulFn b e) + pushNewFact <| mkExpectedPropHint + (mkApp6 (mkConst ``Grind.CommRing.div_int_eq [ring.u]) ring.type fieldInst charInst a (mkIntLit k) reflBoolTrue) + expected + else if k % c == 0 then + let expected ← mkEq e (← denoteNum 0) + pushNewFact <| mkExpectedPropHint + (mkApp7 (mkConst ``Grind.CommRing.div_zero_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst a (mkIntLit k) reflBoolTrue) + expected + else + let expected ← mkEq a (mkApp2 ring.mulFn b e) + pushNewFact <| mkExpectedPropHint + (mkApp7 (mkConst ``Grind.CommRing.div_int_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst a (mkIntLit k) reflBoolTrue) + expected + else + -- TODO + return () + +/-- +Returns `true` if `e` is a term `a/b` or `a⁻¹`. +-/ +private def internalizeDivInv (e : Expr) : GoalM Bool := do + match_expr e with + | HDiv.hDiv α _ _ inst a b => + let some ringId ← getRingId? α | return true + RingM.run ringId do processDiv e inst a b + return true + | Inv.inv _α _inst _a => + -- TODO + return true + | _ => return false + def internalize (e : Expr) (parent? : Option Expr) : GoalM Unit := do if !(← getConfig).ring && !(← getConfig).ringNull then return () + if (← internalizeDivInv e) then return () let some type := getType? e | return () if isForbiddenParent parent? then return () let some ringId ← getRingId? type | return () diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean index d510cd7c7d..8f130b6104 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/RingId.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude +import Init.Grind.CommRing.Field import Lean.Meta.Tactic.Grind.Simp import Lean.Meta.Tactic.Grind.Arith.CommRing.Util @@ -12,41 +13,38 @@ namespace Lean.Meta.Grind.Arith.CommRing private def internalizeFn (fn : Expr) : GoalM Expr := do shareCommon (← canon fn) -private def getAddFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do - let instType := mkApp3 (mkConst ``HAdd [u, u, u]) type type type - let .some inst ← trySynthInstance instType | - throwError "failed to find instance for ring addition{indentExpr instType}" - let inst' := mkApp2 (mkConst ``instHAdd [u]) type <| mkApp2 (mkConst ``Grind.Semiring.toAdd [u]) type semiringInst - unless (← withDefault <| isDefEq inst inst') do - throwError "instance for addition{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}" - internalizeFn <| mkApp4 (mkConst ``HAdd.hAdd [u, u, u]) type type type inst +private def getUnaryFn (type : Expr)(u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do + let instType := mkApp (mkConst instDeclName [u]) type + let .some inst ← trySynthInstance instType + | throwError "`grind ring` failed to find instance{indentExpr instType}" + internalizeFn <| mkApp2 (mkConst declName [u]) type inst -private def getMulFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do - let instType := mkApp3 (mkConst ``HMul [u, u, u]) type type type - let .some inst ← trySynthInstance instType | - throwError "failed to find instance for ring multiplication{indentExpr instType}" - let inst' := mkApp2 (mkConst ``instHMul [u]) type <| mkApp2 (mkConst ``Grind.Semiring.toMul [u]) type semiringInst - unless (← withDefault <| isDefEq inst inst') do - throwError "instance for multiplication{indentExpr inst}\nis not definitionally equal to the `Grind.Semiring` one{indentExpr inst'}" - internalizeFn <| mkApp4 (mkConst ``HMul.hMul [u, u, u]) type type type inst +private def getBinHomoFn (type : Expr)(u : Level) (instDeclName : Name) (declName : Name) : GoalM Expr := do + let instType := mkApp3 (mkConst instDeclName [u, u, u]) type type type + let .some inst ← trySynthInstance instType + | throwError "`grind ring` failed to find instance{indentExpr instType}" + internalizeFn <| mkApp4 (mkConst declName [u, u, u]) type type type inst -private def getSubFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Expr := do - let instType := mkApp3 (mkConst ``HSub [u, u, u]) type type type - let .some inst ← trySynthInstance instType | - throwError "failed to find instance for ring subtraction{indentExpr instType}" - let inst' := mkApp2 (mkConst ``instHSub [u]) type <| mkApp2 (mkConst ``Grind.Ring.toSub [u]) type ringInst - unless (← withDefault <| isDefEq inst inst') do - throwError "instance for subtraction{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}" - internalizeFn <| mkApp4 (mkConst ``HSub.hSub [u, u, u]) type type type inst +-- Remark: we removed consistency checks such as the one that ensures `HAdd` instance matches `Semiring.toAdd` +-- That is, we are assuming the type classes were properly setup. -private def getNegFn (type : Expr) (u : Level) (ringInst : Expr) : GoalM Expr := do - let instType := mkApp (mkConst ``Neg [u]) type - let .some inst ← trySynthInstance instType | - throwError "failed to find instance for ring negation{indentExpr instType}" - let inst' := mkApp2 (mkConst ``Grind.Ring.toNeg [u]) type ringInst - unless (← withDefault <| isDefEq inst inst') do - throwError "instance for negation{indentExpr inst}\nis not definitionally equal to the `Grind.Ring` one{indentExpr inst'}" - internalizeFn <| mkApp2 (mkConst ``Neg.neg [u]) type inst +private def getAddFn (type : Expr) (u : Level) : GoalM Expr := do + getBinHomoFn type u ``HAdd ``HAdd.hAdd + +private def getMulFn (type : Expr) (u : Level) : GoalM Expr := do + getBinHomoFn type u ``HMul ``HMul.hMul + +private def getSubFn (type : Expr) (u : Level) : GoalM Expr := do + getBinHomoFn type u ``HSub ``HSub.hSub + +private def getDivFn (type : Expr) (u : Level) : GoalM Expr := do + getBinHomoFn type u ``HDiv ``HDiv.hDiv + +private def getNegFn (type : Expr) (u : Level) : GoalM Expr := do + getUnaryFn type u ``Neg ``Neg.neg + +private def getInvFn (type : Expr) (u : Level) : GoalM Expr := do + getUnaryFn type u ``Inv ``Inv.inv private def getPowFn (type : Expr) (u : Level) (semiringInst : Expr) : GoalM Expr := do let instType := mkApp3 (mkConst ``HPow [u, 0, u]) type Nat.mkType type @@ -135,15 +133,23 @@ where let noZeroDivType := mkApp3 (mkConst ``Grind.NoNatZeroDivisors [u]) type zeroInst hmulInst LOption.toOption <$> trySynthInstance noZeroDivType trace_goal[grind.ring] "NoNatZeroDivisors available: {noZeroDivInst?.isSome}" - let addFn ← getAddFn type u semiringInst - let mulFn ← getMulFn type u semiringInst - let subFn ← getSubFn type u ringInst - let negFn ← getNegFn type u ringInst + let field := mkApp (mkConst ``Grind.Field [u]) type + let fieldInst? : Option Expr ← LOption.toOption <$> trySynthInstance field + let addFn ← getAddFn type u + let mulFn ← getMulFn type u + let subFn ← getSubFn type u + let negFn ← getNegFn type u 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)) + else + pure (none, none) let id := (← get').rings.size - let ring : Ring := { id, type, u, semiringInst, ringInst, commSemiringInst, commRingInst, charInst?, noZeroDivInst?, addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn } + let ring : Ring := { + id, type, u, semiringInst, ringInst, commSemiringInst, commRingInst, charInst?, noZeroDivInst?, fieldInst?, + addFn, mulFn, subFn, negFn, powFn, intCastFn, natCastFn, invFn?, divFn? } modify' fun s => { s with rings := s.rings.push ring } return some id diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index e63b78517f..1b385f5ef0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -139,9 +139,11 @@ structure Ring where /-- `CommRing` instance for `type` -/ commRingInst : Expr /-- `IsCharP` instance for `type` if available. -/ - charInst? : Option (Expr × Nat) := .none + charInst? : Option (Expr × Nat) /-- `NoNatZeroDivisors` instance for `type` if available. -/ - noZeroDivInst? : Option Expr := .none + noZeroDivInst? : Option Expr + /-- `Field` instance for `type` if available. -/ + fieldInst? : Option Expr addFn : Expr mulFn : Expr subFn : Expr @@ -149,6 +151,10 @@ structure Ring where powFn : Expr intCastFn : Expr natCastFn : Expr + /-- Inverse if `fieldInst?` is `some inst` -/ + invFn? : Option Expr + /-- Division if `fieldInst?` is `some inst` -/ + divFn? : Option Expr /-- Mapping from variables to their denotations. Remark each variable can be in only one ring. @@ -178,6 +184,10 @@ structure Ring where disequalities and implied equalities. -/ recheck : Bool := false + /-- Division theorems that have been already asserted. -/ + divSet : PHashSet (Expr × Expr) := {} + /-- Inverse theorems that have been already asserted. -/ + invSet : PHashSet Expr := {} deriving Inhabited /-- State for all `CommRing` types detected by `grind`. -/ diff --git a/tests/lean/run/grind_field_div.lean b/tests/lean/run/grind_field_div.lean new file mode 100644 index 0000000000..6ebcdb4d1d --- /dev/null +++ b/tests/lean/run/grind_field_div.lean @@ -0,0 +1,18 @@ +open Lean Grind + +example [Field α] [IsCharP α 0] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c := by + grind + +example [Field α] (a b : α) : b = 0 → (a + a) / 0 = b := by + grind + +example [Field α] [IsCharP α 3] (a b : α) : a/3 = b → b = 0 := by + grind + +example [Field α] [IsCharP α 7] (a b c : α) : a/3 = b → c = a/3 → a/2 + a/2 = b + 2*c + 7 := by + grind + +example [Field R] [IsCharP R 0] (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