diff --git a/src/Init/Grind/CommRing/Poly.lean b/src/Init/Grind/CommRing/Poly.lean index 6ed19a0922..5722523d9a 100644 --- a/src/Init/Grind/CommRing/Poly.lean +++ b/src/Init/Grind/CommRing/Poly.lean @@ -1224,29 +1224,41 @@ 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 +theorem inv_int_eq [Field α] [IsCharP α 0] (b : Int) : b != 0 → (denoteInt b : α) * (denoteInt b)⁻¹ = 1 := by + simp; 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] + rw [Field.mul_inv_cancel this] -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 +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 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] + rw [Field.mul_inv_cancel this] -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 +theorem inv_zero_eqC {α c} [Field α] [IsCharP α c] (b : Int) : b % c == 0 → (denoteInt b : α)⁻¹ = 0 := by + simp [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] + simp [this, Field.inv_zero] + +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] + +def one_eq_zero_unsat_cert (p : Poly) := + p == .num 1 || p == .num (-1) + +theorem one_eq_zero_unsat {α} [Field α] (ctx : Context α) (p : Poly) : one_eq_zero_unsat_cert p → p.denote ctx = 0 → False := by + simp [one_eq_zero_unsat_cert]; intro h; cases h <;> simp [*, Poly.denote, intCast_one, intCast_neg] + next => rw [Eq.comm]; apply Field.zero_ne_one + next => rw [← neg_eq_zero, neg_neg, Eq.comm]; apply Field.zero_ne_one + end CommRing end Lean.Grind diff --git a/src/Init/Grind/Norm.lean b/src/Init/Grind/Norm.lean index bde0d9a418..119de2ff55 100644 --- a/src/Init/Grind/Norm.lean +++ b/src/Init/Grind/Norm.lean @@ -12,6 +12,7 @@ import Init.Classical import Init.ByCases import Init.Data.Int.Linear import Init.Data.Int.Pow +import Init.Grind.CommRing.Field namespace Lean.Grind /-! @@ -197,5 +198,7 @@ init_grind_norm -- Function composition Function.const_apply Function.comp_apply Function.const_comp Function.comp_const Function.true_comp Function.false_comp + -- Field + Field.div_eq_mul_inv Field.inv_zero Field.inv_inv Field.inv_one Field.inv_neg end Lean.Grind diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean index 5a86a761f1..801c18ffd3 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/EqCnstr.lean @@ -123,9 +123,15 @@ def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}" else if (← hasChar) then c.setUnsat + else if k.natAbs == 1 then + if (← isField) then + c.setUnsat + else + -- Remark: we currently don't do anything if the ring characteristic is not known. + -- TODO: we could set all terms of this ring `0` if `1 = 0`. + trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}" else - -- Remark: we currently don't do anything if the characteristic is not known. - -- TODO: if `k.natAbs` is `1`, we could set all terms of this ring `0`. + -- TODO: we could save the equation for and use it to simplify polynomials trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}" return true diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean index d046b6581a..974b8af5a0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Internalize.lean @@ -59,62 +59,55 @@ private partial def toInt? (e : Expr) : RingM (Option Int) := do return some (Int.ofNat v) | _ => return none -private def isDivInst (inst : Expr) : RingM Bool := do - let some fn := (← getRing).divFn? | return false +private def isInvInst (inst : Expr) : RingM Bool := do + let some fn := (← getRing).invFn? | 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` +Given `e` of the form `@Inv.inv _ inst a`, +asserts `a * a⁻¹ = 1` if `a` is a numeral. +Otherwise, asserts `if a = 0 then a⁻¹ = 0 else a * a⁻¹ = 1` -/ -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 +private def processInv (e inst a : Expr) : RingM Unit := do + unless (← isInvInst inst) do return () + let ring ← getRing + let some fieldInst := ring.fieldInst? | return () + if (← getRing).invSet.contains a then return () + modifyRing fun s => { s with invSet := s.invSet.insert a } + if let some k ← toInt? a then + assert! k != 0 -- We have the normalization rule `Field.inv_zero` + if (← hasChar) then let (charInst, c) ← getCharInst if c == 0 then - let expected ← mkEq a (mkApp2 ring.mulFn b e) + let expected ← mkEq (mkApp2 ring.mulFn a e) (← denoteNum 1) pushNewFact <| mkExpectedPropHint - (mkApp6 (mkConst ``Grind.CommRing.div_int_eq [ring.u]) ring.type fieldInst charInst a (mkIntLit k) reflBoolTrue) + (mkApp5 (mkConst ``Grind.CommRing.inv_int_eq [ring.u]) ring.type fieldInst charInst (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) + (mkApp6 (mkConst ``Grind.CommRing.inv_zero_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst (mkIntLit k) reflBoolTrue) expected else - let expected ← mkEq a (mkApp2 ring.mulFn b e) + let expected ← mkEq (mkApp2 ring.mulFn a e) (← denoteNum 1) pushNewFact <| mkExpectedPropHint - (mkApp7 (mkConst ``Grind.CommRing.div_int_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst a (mkIntLit k) reflBoolTrue) + (mkApp6 (mkConst ``Grind.CommRing.inv_int_eqC [ring.u]) ring.type (mkNatLit c) fieldInst charInst (mkIntLit k) reflBoolTrue) expected - else - -- TODO - return () + return () + pushNewFact <| mkApp3 (mkConst ``Grind.CommRing.inv_split [ring.u]) ring.type fieldInst a -/-- -Returns `true` if `e` is a term `a/b` or `a⁻¹`. --/ -private def internalizeDivInv (e : Expr) : GoalM Bool := do +/-- Returns `true` if `e` is a term `a⁻¹`. -/ +private def internalizeInv (e : Expr) : GoalM Bool := do match_expr e with - | HDiv.hDiv α _ _ inst a b => + | Inv.inv α inst a => let some ringId ← getRingId? α | return true - RingM.run ringId do processDiv e inst a b - return true - | Inv.inv _α _inst _a => - -- TODO + RingM.run ringId do processInv e inst a 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 () + if (← internalizeInv 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/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean index 2e21a93959..72eda8b0e8 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean @@ -236,7 +236,7 @@ def setEqUnsat (c : EqCnstr) : RingM Unit := do trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}" let ring ← getRing let some (charInst, char) := ring.charInst? - | throwError "`grind` internal error, `IsCharP` insrtance is needed, but it is not available for{indentExpr (← getRing).type}" + | throwError "`grind` internal error, `IsCharP` instance is needed, but it is not available for{indentExpr (← getRing).type}\nconsider not using `+ringNull`" let h := if char == 0 then mkApp (mkConst ``Grind.CommRing.NullCert.eq_unsat [ring.u]) ring.type else @@ -432,12 +432,18 @@ where open Lean.Grind.CommRing in def setEqUnsat (c : EqCnstr) : RingM Unit := do let h ← withProofContext do - let mut h ← mkStepPrefix ``Stepwise.unsat_eq ``Stepwise.unsat_eqC - let (charInst, char) ← getCharInst - if char == 0 then - h := mkApp h charInst - let k ← getPolyConst c.p - return mkApp4 h (← mkPolyDecl c.p) (toExpr k) reflBoolTrue (← c.toExprProof) + let ring ← getRing + if let some (charInst, char) := ring.charInst? then + let mut h ← mkStepPrefix ``Stepwise.unsat_eq ``Stepwise.unsat_eqC + if char == 0 then + h := mkApp h charInst + let k ← getPolyConst c.p + return mkApp4 h (← mkPolyDecl c.p) (toExpr k) reflBoolTrue (← c.toExprProof) + else if let some fieldInst := ring.fieldInst? then + return mkApp6 (mkConst ``Grind.CommRing.one_eq_zero_unsat [ring.u]) ring.type fieldInst (← getContext) + (← mkPolyDecl c.p) reflBoolTrue (← c.toExprProof) + else + throwError "`grind ring` internal error, unexpected unsat eq proof {← c.denoteExpr}" closeGoal h def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean index 1b385f5ef0..0613b2caa0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Types.lean @@ -184,8 +184,6 @@ 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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean index 0a88e77c6e..7480912359 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Util.lean @@ -124,6 +124,9 @@ def getCharInst : RingM (Expr × Nat) := do | throwError "`grind` internal error, ring does not have a characteristic" return c +def isField : RingM Bool := + return (← getRing).fieldInst?.isSome + /-- Converts the given ring expression into a multivariate polynomial. If the ring has a nonzero characteristic, it is used during normalization. diff --git a/tests/lean/run/grind_field_div.lean b/tests/lean/run/grind_field_div.lean index 6ebcdb4d1d..5499eb984a 100644 --- a/tests/lean/run/grind_field_div.lean +++ b/tests/lean/run/grind_field_div.lean @@ -16,3 +16,43 @@ 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 + +example [Field α] (a : α) : (1 / 2) * a = a / 2 := by grind + +example [Field α] (a : α) : 2⁻¹ * a = a / 2 := by grind + +example [Field α] (a : α) : a⁻¹⁻¹ = a := by grind + +example [Field α] [IsCharP α 0] (a : α) : a / 2 + a / 3 = 5 * a / 6 := by + grind + +example [Field α] (a b : α) : a ≠ 0 → b ≠ 0 → a / (a / b) = b := by + grind + +example [Field α] (a b : α) : a ≠ 0 → a / (a / b) = b := by + grind + +example [Field α] [IsCharP α 0] (x : α) + : x ≠ 0 → (4 / x)⁻¹ * ((3 * x^3) / x)^2 * ((1 / (2 * x))⁻¹)^3 = 18 * x^8 := by + grind + +example [Field α] (a : α) : 2 * a ≠ 0 → 1 / a + 1 / (2 * a) = 3 / (2 * a) := by + grind + +example [Field α] [IsCharP α 0] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by + grind + +example [Field α] [IsCharP α 0] (a b : α) : 2*b - a = a + b → 1 / a + 1 / (2 * a) = 3 / b := by + grind + +example [Field α] [NoNatZeroDivisors α] (a : α) : 1 / a + 1 / (2 * a) = 3 / (2 * a) := by + grind + +example [Field α] {x y z w : α} : x / y = z / w → y ≠ 0 → w ≠ 0 → x * w = z * y := by + grind + +example [Field α] (a : α) : a = 0 → a ≠ 1 := by + grind + +example [Field α] (a : α) : a = 0 → a ≠ 1 - a := by + grind