diff --git a/src/Init/Grind/Ordered/Linarith.lean b/src/Init/Grind/Ordered/Linarith.lean index 44a5502e13..6598967ced 100644 --- a/src/Init/Grind/Ordered/Linarith.lean +++ b/src/Init/Grind/Ordered/Linarith.lean @@ -6,6 +6,7 @@ Authors: Leonardo de Moura module prelude import Init.Grind.Ordered.Module +import Init.Grind.Ordered.Ring import all Init.Data.Ord import all Init.Data.AC import Init.Data.RArray @@ -450,6 +451,14 @@ theorem lt_unsat {α} [IntModule α] [Preorder α] (ctx : Context α) : (Poly.ni have := Preorder.lt_iff_le_not_le.mp h simp at this +def zero_lt_one_cert (p : Poly) : Bool := + p == .add (-1) 0 .nil + +theorem zero_lt_one {α} [Ring α] [Preorder α] [Ring.IsOrdered α] (ctx : Context α) (p : Poly) + : zero_lt_one_cert p → (0 : Var).denote ctx = One.one → p.denote' ctx < 0 := by + simp [zero_lt_one_cert]; intro _ h; subst p; simp [Poly.denote, h, One.one, neg_hmul] + rw [neg_lt_iff, neg_zero]; apply Ring.IsOrdered.zero_lt_one + /-! Coefficient normalization -/ diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean index 7cb3c781d8..d9211fae39 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean @@ -102,7 +102,7 @@ def propagateIneq (e : Expr) (eqTrue : Bool) : GoalM Unit := do return () let lhs := e.getArg! 2 numArgs let rhs := e.getArg! 3 numArgs - if (← isCommRing) then + if (← isOrderedCommRing) then propagateCommRingIneq e lhs rhs strict eqTrue -- TODO: non-commutative ring normalizer else diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 4e4331c998..d12415b4f5 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean @@ -196,6 +196,10 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d | false, false => (``Grind.Linarith.le_le_combine, c₁, c₂) return mkApp6 (← mkIntModPreOrdThmPrefix declName) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p) reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof) + | .oneGtZero => + let s ← getStruct + let h := mkApp5 (mkConst ``Grind.Linarith.zero_lt_one [s.u]) s.type (← getRingInst) s.preorderInst (← getRingIsOrdInst) (← getContext) + return mkApp3 h (← mkPolyDecl c'.p) reflBoolTrue (← mkEqRefl (← getOne)) | _ => throwError "NIY" partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean index c77b631bca..f974aabff1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Reify.lean @@ -96,6 +96,6 @@ partial def reify? (e : Expr) (skipVar : Bool) : LinearM (Option LinExpr) := do if skipVar then return none else - return some (← asVar e) + return some (← toVar e) end Lean.Meta.Grind.Arith.Linear diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean index ec30479abf..36871e585d 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/StructId.lean @@ -139,7 +139,10 @@ where let getRingIsOrdInst? : GoalM (Option Expr) := do let some ringInst := ringInst? | return none let isOrdType := mkApp3 (mkConst ``Grind.Ring.IsOrdered [u]) type ringInst preorderInst - return LOption.toOption (← trySynthInstance isOrdType) + let .some inst ← trySynthInstance isOrdType + | reportIssue! "type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize{indentExpr isOrdType}" + return none + return some inst let ringIsOrdInst? ← getRingIsOrdInst? let getNoNatZeroDivInst? : GoalM (Option Expr) := do let hmulNat := mkApp3 (mkConst ``HMul [0, u, u]) Nat.mkType type type diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean index 3b70a13206..d35f0b72d5 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Util.lean @@ -86,6 +86,9 @@ def withRingM (x : RingM α) : LinearM α := do def isCommRing : LinearM Bool := return (← getStruct).ringId?.isSome +def isOrderedCommRing : LinearM Bool := do + return (← isCommRing) && (← getStruct).ringIsOrdInst?.isSome + def isLinearOrder : LinearM Bool := return (← getStruct).linearInst?.isSome @@ -109,6 +112,11 @@ def getLinearOrderInst : LinearM Expr := do | throwError "`grind linarith` internal error, structure is not a linear order" return inst +def getRingInst : LinearM Expr := do + let some inst := (← getStruct).ringInst? + | throwError "`grind linarith` internal error, structure is not a ring" + return inst + def getCommRingInst : LinearM Expr := do let some inst := (← getStruct).commRingInst? | throwError "`grind linarith` internal error, structure is not a commutative ring" diff --git a/tests/lean/run/grind_linarith_1.lean b/tests/lean/run/grind_linarith_1.lean index 3564eb08bd..8eea1b9d68 100644 --- a/tests/lean/run/grind_linarith_1.lean +++ b/tests/lean/run/grind_linarith_1.lean @@ -61,5 +61,29 @@ example [CommRing α] [LinearOrder α] [Ring.IsOrdered α] (a b c d : α) grind example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b c : α) - : a < b → b < c → c < a → False := by + : a < b → 2*b < c → c < 2*a → False := by grind + +-- Test misconfigured instances +/-- +trace: [grind.issues] type is an ordered `IntModule` and a `Ring`, but is not an ordered ring, failed to synthesize + Ring.IsOrdered α +-/ +#guard_msgs (drop error, trace) in +set_option trace.grind.issues true in +example [CommRing α] [Preorder α] [IntModule.IsOrdered α] (a b c : α) + : a < b → b + b < c → c < a → False := by + grind + +example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α) + : a < 2 → b < a → b > 5 → False := by + grind + +example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α) + : a < One.one + 4 → b < a → b ≥ 5 → False := by + grind + +example [CommRing α] [Preorder α] [Ring.IsOrdered α] (a b : α) + : a < One.one + 5 → b < a → b ≥ 5 → False := by + fail_if_success grind + sorry