refactor: grind linarith ring normalization (#11334)
This PR adds an explicit normalization layer for ring constraints in the `grind linarith` module. For example, it will be used to clean up denominators when the ring is a field.
This commit is contained in:
Leonardo de Moura
GitHub
parent
0b173923f4
commit
f2e191d0af
7 changed files with 164 additions and 79 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue