diff --git a/src/Init/Grind/Ring/CommSolver.lean b/src/Init/Grind/Ring/CommSolver.lean index b3eee2e73e..48ca432248 100644 --- a/src/Init/Grind/Ring/CommSolver.lean +++ b/src/Init/Grind/Ring/CommSolver.lean @@ -1393,15 +1393,19 @@ theorem simp {α} [CommRing α] (ctx : Context α) (k₁ : Int) (p₁ : Poly) (k noncomputable def mul_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool := p₁.mulConst_k k |>.beq' p -def mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) +theorem mul {α} [CommRing α] (ctx : Context α) (p₁ : Poly) (k : Int) (p : Poly) : mul_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by simp [mul_cert]; intro _ h; subst p simp [Poly.denote_mulConst, *, mul_zero] +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 + noncomputable def div_cert (p₁ : Poly) (k : Int) (p : Poly) : Bool := !Int.beq' k 0 |>.and' (p.mulConst_k k |>.beq' p₁) -def div {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly) +theorem div {α} [CommRing α] (ctx : Context α) [NoNatZeroDivisors α] (p₁ : Poly) (k : Int) (p : Poly) : div_cert p₁ k p → p₁.denote ctx = 0 → p.denote ctx = 0 := by simp [div_cert]; intro hnz _ h; subst p₁ simp [Poly.denote_mulConst, ← zsmul_eq_intCast_mul] at h @@ -1575,60 +1579,62 @@ theorem Poly.denoteAsIntModule_eq_denote {α} [CommRing α] (ctx : Context α) ( open Stepwise theorem eq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denoteAsIntModule ctx = 0 := by - rw [Poly.denoteAsIntModule_eq_denote]; apply core + : core_cert lhs rhs p → lhs.denote ctx = rhs.denote ctx → p.denote ctx = 0 := by + apply core + +theorem eq_int_module {α} [CommRing α] (ctx : Context α) (p : Poly) + : p.denote ctx = 0 → p.denoteAsIntModule ctx = 0 := by + simp [Poly.denoteAsIntModule_eq_denote] theorem diseq_norm {α} [CommRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert lhs rhs p → lhs.denote ctx ≠ rhs.denote ctx → p.denoteAsIntModule ctx ≠ 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote] + : 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] intro h; rw [sub_eq_zero_iff] at h; contradiction +theorem diseq_int_module {α} [CommRing α] (ctx : Context α) (p : Poly) + : p.denote ctx ≠ 0 → p.denoteAsIntModule ctx ≠ 0 := by + simp [Poly.denoteAsIntModule_eq_denote] + open OrderedAdd theorem le_norm {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert lhs rhs p → lhs.denote ctx ≤ rhs.denote ctx → p.denoteAsIntModule ctx ≤ 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote] + : 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] replace h := add_le_left h ((-1) * rhs.denote ctx) rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h assumption +theorem le_int_module {α} [CommRing α] [LE α] (ctx : Context α) (p : Poly) + : p.denote ctx ≤ 0 → p.denoteAsIntModule ctx ≤ 0 := by + simp [Poly.denoteAsIntModule_eq_denote] + 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.denoteAsIntModule ctx < 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h; subst p; simp [Expr.denote_toPoly, Expr.denote] + : 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] replace h := add_lt_left h ((-1) * rhs.denote ctx) rw [neg_mul, ← sub_eq_add_neg, one_mul, ← sub_eq_add_neg, sub_self] at h assumption +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 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.denoteAsIntModule ctx < 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] + : 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] replace h₁ := LinearOrder.lt_of_not_le h₁ replace h₁ := add_lt_left h₁ (-lhs.denote ctx) simp [← sub_eq_add_neg, sub_self] at h₁ assumption theorem not_lt_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.denoteAsIntModule ctx ≤ 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote] + : 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] replace h₁ := LinearOrder.le_of_not_lt h₁ replace h₁ := add_le_left h₁ (-lhs.denote ctx) simp [← sub_eq_add_neg, sub_self] at h₁ assumption -theorem not_le_norm' {α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (ctx : Context α) (lhs rhs : Expr) (p : Poly) - : core_cert lhs rhs p → ¬ lhs.denote ctx ≤ rhs.denote ctx → ¬ p.denoteAsIntModule ctx ≤ 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h - replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) ≤ _ := add_le_right (rhs.denote ctx) h - rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h - contradiction - -theorem not_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.denoteAsIntModule ctx < 0 := by - simp [core_cert, Poly.denoteAsIntModule_eq_denote]; intro _ h₁; subst p; simp [Expr.denote_toPoly, Expr.denote]; intro h - replace h : rhs.denote ctx + (lhs.denote ctx - rhs.denote ctx) < _ := add_lt_right (rhs.denote ctx) h - rw [sub_eq_add_neg, add_left_comm, ← sub_eq_add_neg, sub_self] at h; simp [add_zero] at h - contradiction - 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 diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean index 29966f1ace..73a819e0c0 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/IneqCnstr.lean @@ -46,19 +46,21 @@ def propagateCommRingIneq (e : Expr) (lhs rhs : Expr) (strict : Bool) (eqTrue : let some rhs ← withRingM <| CommRing.reify? rhs (skipVar := false) | return () let generation ← getGeneration e if eqTrue then - let p' := (lhs.sub rhs).toPoly - let lhs' ← p'.toIntModuleExpr generation - let some lhs' ← reify? lhs' (skipVar := false) generation | return () - let p := lhs'.norm - let c : IneqCnstr := { p, strict, h := .coreCommRing e lhs rhs p' lhs' } + let p := (lhs.sub rhs).toPoly + let c : RingIneqCnstr := { p, strict, h := .core e lhs rhs } + let lhs ← p.toIntModuleExpr generation + let some lhs ← reify? lhs (skipVar := false) generation | return () + let p := lhs.norm + let c : IneqCnstr := { p, strict, h := .ring c lhs } c.assert else if (← isLinearOrder) then - let p' := (rhs.sub lhs).toPoly + let p := (rhs.sub lhs).toPoly let strict := !strict - let lhs' ← p'.toIntModuleExpr generation - let some lhs' ← reify? lhs' (skipVar := false) generation | return () - let p := lhs'.norm - let c : IneqCnstr := { p, strict, h := .notCoreCommRing e lhs rhs p' lhs' } + let c : RingIneqCnstr := { p, strict, h := .notCore e lhs rhs } + let lhs ← p.toIntModuleExpr generation + let some lhs ← reify? lhs (skipVar := false) generation | return () + let p := lhs.norm + let c : IneqCnstr := { p, strict, h := .ring c lhs } c.assert else -- Negation for preorders is not supported diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean index 4219e76036..9fea50d7d1 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean @@ -204,6 +204,22 @@ 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 α] [LE α] (rctx : Context α)` +-/ +private def mkCommRingLEThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp4 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLEInst) (← getRingContext) + +/-- +Returns the prefix of a theorem with name `declName` where the first four arguments are +`{α} [CommRing α] [LT α] (rctx : Context α)` +-/ +private def mkCommRingLTThmPrefix (declName : Name) : ProofM Expr := do + let s ← getStruct + return mkApp4 (mkConst declName [s.u]) s.type (← getCommRingInst) (← getLTInst) (← getRingContext) + /-- Returns the prefix of a theorem with name `declName` where the first five arguments are `{α} [CommRing α] [LE α] [LT α] [IsPreorder α] [OrderedRing α] (rctx : Context α)` @@ -228,6 +244,31 @@ 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) +partial def RingIneqCnstr.toExprProof (c' : RingIneqCnstr) : ProofM Expr := do + match c'.h with + | .core e lhs rhs => + let h' ← if c'.strict then mkCommRingLawfulPreOrdThmPrefix ``Grind.CommRing.lt_norm else mkCommRingPreOrdThmPrefix ``Grind.CommRing.le_norm + return mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e)) + | .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)) + +partial def RingEqCnstr.toExprProof (c' : RingEqCnstr) : ProofM Expr := do + match c'.h with + | .core a b la lb => + let h' ← mkCommRingThmPrefix ``Grind.CommRing.eq_norm + return mkApp5 h' (← mkRingExprDecl la) (← mkRingExprDecl lb) (← mkRingPolyDecl c'.p) eagerReflBoolTrue (← mkEqProof a b) + | .symm c => + let h ← c.toExprProof + let h' ← mkCommRingThmPrefix ``Grind.CommRing.Stepwise.inv + return mkApp4 h' (← mkRingPolyDecl c.p) (← mkRingPolyDecl c'.p) eagerReflBoolTrue 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) + mutual partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' do match c'.h with @@ -237,14 +278,10 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d | .notCore e lhs rhs => let h ← mkIntModLinOrdThmPrefix (if c'.strict then ``Grind.Linarith.not_le_norm else ``Grind.Linarith.not_lt_norm) return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e)) - | .coreCommRing e lhs rhs p' lhs' => - let h' ← if c'.strict then mkCommRingLawfulPreOrdThmPrefix ``Grind.CommRing.lt_norm else mkCommRingPreOrdThmPrefix ``Grind.CommRing.le_norm - let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') eagerReflBoolTrue (mkOfEqTrueCore e (← mkEqTrueProof e)) - let h ← if c'.strict then mkIntModLawfulPreOrdThmPrefix ``Grind.Linarith.lt_norm else mkIntModPreOrdThmPrefix ``Grind.Linarith.le_norm - return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h' - | .notCoreCommRing e lhs rhs p' lhs' => - let h' ← mkCommRingLinOrdThmPrefix (if c'.strict then ``Grind.CommRing.not_le_norm else ``Grind.CommRing.not_lt_norm) - let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') eagerReflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e)) + | .ring c lhs' => + let h ← c.toExprProof + let h' ← if c'.strict then mkCommRingLTThmPrefix ``Grind.CommRing.lt_int_module else mkCommRingLEThmPrefix ``Grind.CommRing.le_int_module + let h' := mkApp2 h' (← mkRingPolyDecl c.p) h let h ← if c'.strict then mkIntModLawfulPreOrdThmPrefix ``Grind.Linarith.lt_norm else mkIntModPreOrdThmPrefix ``Grind.Linarith.le_norm return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h' | .coreOfNat e natStructId lhs rhs => @@ -304,11 +341,11 @@ partial def IneqCnstr.toExprProof (c' : IneqCnstr) : ProofM Expr := caching c' d a b a' b' ha hb (← mkEqProof a b) let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq return mkApp5 h (← mkExprDecl la) (← mkExprDecl lb) (← mkPolyDecl c'.p) eagerReflBoolTrue h' - | .ofCommRingEq a b la lb p' lhs' => - let h' ← mkCommRingThmPrefix ``Grind.CommRing.eq_norm - let h' := mkApp5 h' (← mkRingExprDecl la) (← mkRingExprDecl lb) (← mkRingPolyDecl p') eagerReflBoolTrue (← mkEqProof a b) + | .ringEq c lhs => + let h' ← c.toExprProof + let h' := mkApp2 (← mkCommRingThmPrefix ``Grind.CommRing.eq_int_module) (← mkRingPolyDecl c.p) h' let h ← mkIntModPreOrdThmPrefix ``Grind.Linarith.le_of_eq - return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h' + return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h' | .dec h => return mkFVar h | .ofDiseqSplit c₁ fvarId h _ => let hFalse ← h.toExprProofCore @@ -323,11 +360,11 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' | .core a b lhs rhs => let h ← mkIntModThmPrefix ``Grind.Linarith.diseq_norm return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkDiseqProof a b) - | .coreCommRing a b lhs rhs p' lhs' => - let h' ← mkCommRingThmPrefix ``Grind.CommRing.diseq_norm - let h' := mkApp5 h' (← mkRingExprDecl lhs) (← mkRingExprDecl rhs) (← mkRingPolyDecl p') eagerReflBoolTrue (← mkDiseqProof a b) + | .ring c lhs => + let h' ← c.toExprProof + let h' := mkApp2 (← mkCommRingThmPrefix ``Grind.CommRing.diseq_int_module) (← mkRingPolyDecl c.p) h' let h ← mkIntModThmPrefix ``Grind.Linarith.diseq_norm - return mkApp5 h (← mkExprDecl lhs') (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h' + return mkApp5 h (← mkExprDecl lhs) (← mkExprDecl .zero) (← mkPolyDecl c'.p) eagerReflBoolTrue h' | .coreOfNat a b natStructId lhs rhs => let h ← OfNatModuleM.run natStructId do let ns ← getNatStruct @@ -403,8 +440,8 @@ mutual partial def IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .core .. | .notCore .. | .coreCommRing .. | .notCoreCommRing .. | .coreOfNat .. | .notCoreOfNat .. - | .oneGtZero | .ofEq .. | .ofEqOfNat .. | .ofCommRingEq .. => return () + | .core .. | .notCore .. | .coreOfNat .. | .notCoreOfNat .. | .ring .. | .ringEq .. + | .oneGtZero | .ofEq .. | .ofEqOfNat .. => return () | .combine c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars | .norm c₁ _ => c₁.collectDecVars | .dec h => markAsFound h @@ -415,7 +452,7 @@ partial def IneqCnstr.collectDecVars (c' : IneqCnstr) : CollectDecVarsM Unit := -- Actually, it cannot even contain decision variables in the current implementation. partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do match c'.h with - | .core .. | .coreCommRing .. | .coreOfNat .. | .oneNeZero => return () + | .core .. | .coreOfNat .. | .oneNeZero | .ring .. => return () | .neg c => c.collectDecVars | .subst _ _ c₁ c₂ | .subst1 _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean index 254801e598..0a2aab9d35 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/PropagateEq.lean @@ -54,18 +54,19 @@ private def processNewCommRingEq' (a b : Expr) : LinearM Unit := do let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return () let some rhs ← withRingM <| CommRing.reify? b (skipVar := false) | return () let generation := max (← getGeneration a) (← getGeneration b) - let p' := (lhs.sub rhs).toPoly - let lhs' ← p'.toIntModuleExpr generation - let some lhs' ← reify? lhs' (skipVar := false) generation | return () - let p := lhs'.norm + let p := (lhs.sub rhs).toPoly + let c : RingEqCnstr := { p, h := .core a b lhs rhs } + let lhs ← p.toIntModuleExpr generation + let some lhs ← reify? lhs (skipVar := false) generation | return () + let p := lhs.norm if p == .nil then return () - let c₁ : IneqCnstr := { p, strict := false, h := .ofCommRingEq a b lhs rhs p' lhs' } + let c₁ : IneqCnstr := { p, strict := false, h := .ringEq c lhs } c₁.assert + let c := { c with p := c.p.mulConst (-1), h := .symm c } let p := p.mul (-1) - let p' := p'.mulConst (-1) - let lhs' ← p'.toIntModuleExpr generation - let some lhs' ← reify? lhs' (skipVar := false) generation | return () - let c₂ : IneqCnstr := { p, strict := false, h := .ofCommRingEq b a rhs lhs p' lhs' } + let lhs ← c.p.toIntModuleExpr generation + let some lhs ← reify? lhs (skipVar := false) generation | return () + let c₂ : IneqCnstr := { p, strict := false, h := .ringEq c lhs } c₂.assert private def processNewIntModuleEq' (a b : Expr) : LinearM Unit := do @@ -271,12 +272,13 @@ def processNewEq (a b : Expr) : GoalM Unit := do private def processNewCommRingDiseq (a b : Expr) : LinearM Unit := do let some lhs ← withRingM <| CommRing.reify? a (skipVar := false) | return () 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 generation := max (← getGeneration a) (← getGeneration b) - let p' := (lhs.sub rhs).toPoly - let lhs' ← p'.toIntModuleExpr generation - let some lhs' ← reify? lhs' (skipVar := false) generation | return () - let p := lhs'.norm - let c : DiseqCnstr := { p, h := .coreCommRing a b lhs rhs p' lhs' } + let lhs ← p.toIntModuleExpr generation + let some lhs ← reify? lhs (skipVar := false) generation | return () + let p := lhs.norm + let c : DiseqCnstr := { p, h := .ring c lhs } c.assert private def processNewIntModuleDiseq (a b : Expr) : LinearM Unit := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean index 1240e82e62..9aac961fc8 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Types.lean @@ -18,6 +18,42 @@ abbrev LinExpr := Lean.Grind.Linarith.Expr deriving instance Hashable for Poly deriving instance Hashable for Grind.Linarith.Expr +mutual +/-- Auxiliary type for normalizing `Ring` and `Field` inequalities. -/ +structure RingIneqCnstr where + p : Grind.CommRing.Poly + strict : Bool + h : RingIneqCnstrProof + +inductive RingIneqCnstrProof where + | core (e : Expr) (lhs rhs : Grind.CommRing.Expr) + | notCore (e : Expr) (lhs rhs : Grind.CommRing.Expr) + -- **TODO**: cleanup denominator proof step +end + +mutual +/-- Auxiliary type for normalizing `Ring` and `Field` equalities. -/ +structure RingEqCnstr where + p : Grind.CommRing.Poly + h : RingEqCnstrProof + +inductive RingEqCnstrProof where + | core (a b : Expr) (ra rb : Grind.CommRing.Expr) + | symm (c : RingEqCnstr) + -- **TODO**: cleanup denominator proof step +end + +mutual +/-- Auxiliary type for normalizing `Ring` and `Field` disequalities. -/ +structure RingDiseqCnstr where + p : Grind.CommRing.Poly + h : RingDiseqCnstrProof + +inductive RingDiseqCnstrProof where + | core (a b : Expr) (ra rb : Grind.CommRing.Expr) + -- **TODO**: cleanup denominator proof step +end + mutual /-- An equality constraint and its justification/proof. -/ structure EqCnstr where @@ -41,8 +77,7 @@ structure IneqCnstr where inductive IneqCnstrProof where | core (e : Expr) (lhs rhs : LinExpr) | notCore (e : Expr) (lhs rhs : LinExpr) - | coreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr) - | notCoreCommRing (e : Expr) (lhs rhs : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr) + | ring (c : RingIneqCnstr) (lhs : LinExpr) | coreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr) | notCoreOfNat (e : Expr) (natStructId : Nat) (lhs rhs : LinExpr) | combine (c₁ : IneqCnstr) (c₂ : IneqCnstr) @@ -54,8 +89,8 @@ inductive IneqCnstrProof where ofEq (a b : Expr) (la lb : LinExpr) | /-- `a ≤ b` from an equality `a = b` coming from the core. -/ ofEqOfNat (a b : Expr) (natStructId : Nat) (la lb : LinExpr) - | /-- `a ≤ b` from an equality `a = b` coming from the core. -/ - ofCommRingEq (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr) + | /-- `p ≤ 0` from a ring equality `p = 0`. -/ + ringEq (c : RingEqCnstr) (lhs : LinExpr) | subst (x : Var) (c₁ : EqCnstr) (c₂ : IneqCnstr) structure DiseqCnstr where @@ -64,7 +99,7 @@ structure DiseqCnstr where inductive DiseqCnstrProof where | core (a b : Expr) (lhs rhs : LinExpr) - | coreCommRing (a b : Expr) (ra rb : Grind.CommRing.Expr) (p : Grind.CommRing.Poly) (lhs' : LinExpr) + | ring (c : RingDiseqCnstr) (lhs : LinExpr) | coreOfNat (a b : Expr) (natStructId : Nat) (lhs rhs : LinExpr) | neg (c : DiseqCnstr) | subst (k₁ k₂ : Int) (c₁ : EqCnstr) (c₂ : DiseqCnstr) diff --git a/tests/lean/run/grind_linarith_2.lean b/tests/lean/run/grind_linarith_2.lean index fc716a6d3f..f3e4be4657 100644 --- a/tests/lean/run/grind_linarith_2.lean +++ b/tests/lean/run/grind_linarith_2.lean @@ -19,7 +19,8 @@ trace: [grind.debug.proof] Classical.byContradiction fun h => let re_2 := (CommRing.Expr.var 1).add (CommRing.Expr.var 0); diseq_unsat ctx (diseq_norm ctx e_2 e_1 p_1 (eagerReduce (Eq.refl true)) - (CommRing.diseq_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h))) + (CommRing.diseq_int_module rctx rp_1 + (CommRing.diseq_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h)))) -/ #guard_msgs in open Linarith in diff --git a/tests/lean/run/grind_linarith_trim_context.lean b/tests/lean/run/grind_linarith_trim_context.lean index 719a5211b0..fdbeaf04a5 100644 --- a/tests/lean/run/grind_linarith_trim_context.lean +++ b/tests/lean/run/grind_linarith_trim_context.lean @@ -22,9 +22,11 @@ trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 => (le_lt_combine ctx p_3 p_5 p_1 (eagerReduce (Eq.refl true)) (le_le_combine ctx p_4 p_2 p_3 (eagerReduce (Eq.refl true)) (le_norm ctx e_3 e_2 p_4 (eagerReduce (Eq.refl true)) - (CommRing.le_norm rctx re_3 re_2 rp_2 (eagerReduce (Eq.refl true)) h_8)) + (CommRing.le_int_module rctx rp_2 + (CommRing.le_norm rctx re_3 re_2 rp_2 (eagerReduce (Eq.refl true)) h_8))) (le_norm ctx e_1 e_2 p_2 (eagerReduce (Eq.refl true)) - (CommRing.le_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h_1))) + (CommRing.le_int_module rctx rp_1 + (CommRing.le_norm rctx re_1 re_2 rp_1 (eagerReduce (Eq.refl true)) h_1)))) (zero_lt_one ctx p_5 (eagerReduce (Eq.refl true)) (Eq.refl One.one)))) -/ #guard_msgs in