feat: use comm ring module to normalize nonlinear polynomials in grind cutsat (#9074)
This PR uses the commutative ring module to normalize nonlinear polynomials in `grind cutsat`. Examples: ```lean example (a b : Nat) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := by grind example (a b c : Int) (h₁ : a + 1 + c = b * a) (h₂ : c + 2*b*a = 0) : 6 * a * b - 2 * a ≤ 2 := by grind ```
This commit is contained in:
Leonardo de Moura
GitHub
parent
f2e06ead54
commit
b95b0069e7
15 changed files with 333 additions and 65 deletions
|
|
@ -1524,7 +1524,7 @@ private theorem cooper_right_core
|
|||
have d_pos : (0 : Int) < 1 := by decide
|
||||
have h₃ : 1 ∣ 0*x + 0 := Int.one_dvd _
|
||||
have h := cooper_dvd_right_core a_neg b_pos d_pos h₁ h₂ h₃
|
||||
simp only [Int.mul_one, gcd_zero, Int.natAbs_of_nonneg (Int.le_of_lt b_pos),
|
||||
simp only [Int.mul_one, gcd_zero, Int.natAbs_of_nonneg (Int.le_of_lt b_pos),
|
||||
Int.ediv_self (Int.ne_of_gt b_pos), lcm_one,
|
||||
Int.zero_mul, Int.mul_zero, Int.add_zero, Int.dvd_zero,
|
||||
and_true, Int.neg_zero] at h
|
||||
|
|
@ -1915,6 +1915,11 @@ theorem eq_def (ctx : Context) (x : Var) (xPoly : Poly) (p : Poly)
|
|||
simp [eq_def_cert]; intro _ h; subst p; simp [h]
|
||||
rw [← Int.sub_eq_add_neg, Int.sub_self]
|
||||
|
||||
theorem eq_def_norm (ctx : Context) (x : Var) (xPoly xPoly' : Poly) (p : Poly)
|
||||
: eq_def_cert x xPoly' p → x.denote ctx = xPoly.denote' ctx → xPoly.denote' ctx = xPoly'.denote' ctx → p.denote' ctx = 0 := by
|
||||
simp [eq_def_cert]; intro _ h₁ h₂; subst p; simp [h₁, h₂]
|
||||
rw [← Int.sub_eq_add_neg, Int.sub_self]
|
||||
|
||||
@[expose]
|
||||
def eq_def'_cert (x : Var) (e : Expr) (p : Poly) : Bool :=
|
||||
p == .add (-1) x e.norm
|
||||
|
|
@ -1924,6 +1929,27 @@ theorem eq_def' (ctx : Context) (x : Var) (e : Expr) (p : Poly)
|
|||
simp [eq_def'_cert]; intro _ h; subst p; simp [h]
|
||||
rw [← Int.sub_eq_add_neg, Int.sub_self]
|
||||
|
||||
@[expose]
|
||||
def eq_def'_norm_cert (x : Var) (e : Expr) (ePoly ePoly' p : Poly) : Bool :=
|
||||
ePoly == e.norm && p == .add (-1) x ePoly'
|
||||
|
||||
theorem eq_def'_norm (ctx : Context) (x : Var) (e : Expr) (ePoly ePoly' : Poly) (p : Poly)
|
||||
: eq_def'_norm_cert x e ePoly ePoly' p → x.denote ctx = e.denote ctx → ePoly.denote' ctx = ePoly'.denote' ctx → p.denote' ctx = 0 := by
|
||||
simp [eq_def'_norm_cert]; intro _ _ h₁ h₂; subst ePoly p; simp [h₁, ← h₂]
|
||||
rw [← Int.sub_eq_add_neg, Int.sub_self]
|
||||
|
||||
theorem eq_norm_poly (ctx : Context) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → p.denote' ctx = 0 → p'.denote' ctx = 0 := by
|
||||
intro h; rw [h]; simp
|
||||
|
||||
theorem le_norm_poly (ctx : Context) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → p.denote' ctx ≤ 0 → p'.denote' ctx ≤ 0 := by
|
||||
intro h; rw [h]; simp
|
||||
|
||||
theorem diseq_norm_poly (ctx : Context) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
|
||||
intro h; rw [h]; simp
|
||||
|
||||
theorem dvd_norm_poly (ctx : Context) (d : Int) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → d ∣ p.denote' ctx → d ∣ p'.denote' ctx := by
|
||||
intro h; rw [h]; simp
|
||||
|
||||
end Int.Linear
|
||||
|
||||
theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ public import Init.Data.RArray
|
|||
public import Init.Grind.Ring.Basic
|
||||
public import Init.Grind.Ring.Field
|
||||
public import Init.Grind.Ordered.Ring
|
||||
|
||||
public import Init.GrindInstances.Ring.Int
|
||||
public section
|
||||
|
||||
namespace Lean.Grind
|
||||
|
|
@ -97,6 +97,17 @@ def Mon.denote {α} [Semiring α] (ctx : Context α) : Mon → α
|
|||
| unit => 1
|
||||
| .mult p m => p.denote ctx * denote ctx m
|
||||
|
||||
@[expose]
|
||||
def Mon.denote' {α} [Semiring α] (ctx : Context α) (m : Mon) : α :=
|
||||
match m with
|
||||
| .unit => 1
|
||||
| .mult pw m => go m (pw.denote ctx)
|
||||
where
|
||||
go (m : Mon) (acc : α) : α :=
|
||||
match m with
|
||||
| .unit => acc
|
||||
| .mult pw m => go m (acc * (pw.denote ctx))
|
||||
|
||||
@[expose]
|
||||
def Mon.ofVar (x : Var) : Mon :=
|
||||
.mult { x, k := 1 } .unit
|
||||
|
|
@ -236,6 +247,24 @@ def Poly.denote [Ring α] (ctx : Context α) (p : Poly) : α :=
|
|||
| .num k => Int.cast k
|
||||
| .add k m p => Int.cast k * m.denote ctx + denote ctx p
|
||||
|
||||
@[expose]
|
||||
def Poly.denote' [Ring α] (ctx : Context α) (p : Poly) : α :=
|
||||
match p with
|
||||
| .num k => Int.cast k
|
||||
| .add k m p => go p (denoteTerm k m)
|
||||
where
|
||||
denoteTerm (k : Int) (m : Mon) : α :=
|
||||
bif k == 1 then
|
||||
m.denote' ctx
|
||||
else
|
||||
Int.cast k * m.denote' ctx
|
||||
|
||||
go (p : Poly) (acc : α) : α :=
|
||||
match p with
|
||||
| .num 0 => acc
|
||||
| .num k => acc + Int.cast k
|
||||
| .add k m p => go p (acc + denoteTerm k m)
|
||||
|
||||
@[expose]
|
||||
def Poly.ofMon (m : Mon) : Poly :=
|
||||
.add 1 m (.num 0)
|
||||
|
|
@ -576,6 +605,14 @@ theorem Power.denote_eq {α} [Semiring α] (ctx : Context α) (p : Power)
|
|||
: p.denote ctx = p.x.denote ctx ^ p.k := by
|
||||
cases p <;> simp [Power.denote] <;> split <;> simp [pow_zero, pow_succ, one_mul]
|
||||
|
||||
theorem Mon.denote'_eq_denote {α} [Semiring α] (ctx : Context α) (m : Mon) : m.denote' ctx = m.denote ctx := by
|
||||
cases m <;> simp [denote', denote]
|
||||
next pw m =>
|
||||
generalize pw.denote ctx = acc
|
||||
fun_induction denote'.go
|
||||
next => simp [denote, Semiring.mul_one]
|
||||
next acc pw m ih => simp [ih, denote, Semiring.mul_assoc]
|
||||
|
||||
theorem Mon.denote_ofVar {α} [Semiring α] (ctx : Context α) (x : Var)
|
||||
: denote ctx (ofVar x) = x.denote ctx := by
|
||||
simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul, mul_one]
|
||||
|
|
@ -658,6 +695,16 @@ theorem Mon.eq_of_revlex {m₁ m₂ : Mon} : revlex m₁ m₂ = .eq → m₁ = m
|
|||
theorem Mon.eq_of_grevlex {m₁ m₂ : Mon} : grevlex m₁ m₂ = .eq → m₁ = m₂ := by
|
||||
simp [grevlex]; intro; apply eq_of_revlex
|
||||
|
||||
theorem Poly.denoteTerm_eq {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : denote'.denoteTerm ctx k m = k * m.denote ctx := by
|
||||
simp [denote'.denoteTerm, Mon.denote'_eq_denote, cond_eq_if]; intro; subst k; rw [Ring.intCast_one, Semiring.one_mul]
|
||||
|
||||
theorem Poly.denote'_eq_denote {α} [Ring α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
|
||||
cases p <;> simp [denote', denote, denoteTerm_eq]
|
||||
next k m p =>
|
||||
generalize k * m.denote ctx = acc
|
||||
fun_induction denote'.go <;> simp [denote, *, Ring.intCast_zero, Semiring.add_zero, denoteTerm_eq]
|
||||
next ih => simp [denoteTerm_eq] at ih; simp [ih, Semiring.add_assoc]
|
||||
|
||||
theorem Poly.denote_ofMon {α} [CommRing α] (ctx : Context α) (m : Mon)
|
||||
: denote ctx (ofMon m) = m.denote ctx := by
|
||||
simp [ofMon, denote, intCast_one, intCast_zero, one_mul, add_zero]
|
||||
|
|
@ -1379,6 +1426,7 @@ theorem Poly.normEq0_eq {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Na
|
|||
simp [denote, normEq0]; split <;> simp [denote, *]
|
||||
next h' => rw [of_mod_eq_0 h h', Semiring.zero_mul, Semiring.zero_add]
|
||||
|
||||
@[expose]
|
||||
def eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
|
||||
p₁ == .num c && p == p₂.normEq0 c
|
||||
|
||||
|
|
@ -1398,6 +1446,7 @@ theorem gcd_eq_0 [CommRing α] (g n m a b : Int) (h : g = a * n + b * m)
|
|||
rw [← Ring.intCast_add, h₂, Semiring.zero_add, ← h] at h₁
|
||||
rw [Ring.intCast_zero, h₁]
|
||||
|
||||
@[expose]
|
||||
def eq_gcd_cert (a b : Int) (p₁ p₂ p : Poly) : Bool :=
|
||||
match p₁ with
|
||||
| .add .. => false
|
||||
|
|
@ -1415,6 +1464,7 @@ theorem eq_gcd {α} [CommRing α] (ctx : Context α) (a b : Int) (p₁ p₂ p :
|
|||
next n m g =>
|
||||
apply gcd_eq_0 g n m a b
|
||||
|
||||
@[expose]
|
||||
def d_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
|
||||
p₂ == .num c && p == p₁.normEq0 c
|
||||
|
||||
|
|
@ -1423,5 +1473,11 @@ theorem d_normEq0 {α} [CommRing α] (ctx : Context α) (k : Int) (c : Nat) (ini
|
|||
simp [d_normEq0_cert]; intro _ h₁ h₂; subst p p₂; simp [Poly.denote]
|
||||
intro h; rw [p₁.normEq0_eq] <;> assumption
|
||||
|
||||
@[expose] def norm_int_cert (e : Expr) (p : Poly) : Bool :=
|
||||
e.toPoly == p
|
||||
|
||||
theorem norm_int (ctx : Context Int) (e : Expr) (p : Poly) : norm_int_cert e p → e.denote ctx = p.denote' ctx := by
|
||||
simp [norm_int_cert, Poly.denote'_eq_denote]; intro; subst p; simp [Expr.denote_toPoly]
|
||||
|
||||
end CommRing
|
||||
end Lean.Grind
|
||||
|
|
|
|||
|
|
@ -18,6 +18,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.SearchM
|
|||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.MBTC
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
|
||||
|
||||
namespace Lean
|
||||
|
||||
|
|
@ -27,6 +28,7 @@ builtin_initialize registerTraceClass `grind.cutsat.assert
|
|||
builtin_initialize registerTraceClass `grind.cutsat.assert.trivial
|
||||
builtin_initialize registerTraceClass `grind.cutsat.assert.unsat
|
||||
builtin_initialize registerTraceClass `grind.cutsat.assert.store
|
||||
builtin_initialize registerTraceClass `grind.cutsat.assert.nonlinear
|
||||
|
||||
builtin_initialize registerTraceClass `grind.debug.cutsat.subst
|
||||
builtin_initialize registerTraceClass `grind.debug.cutsat.search
|
||||
|
|
|
|||
58
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean
Normal file
58
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean
Normal file
|
|
@ -0,0 +1,58 @@
|
|||
/-
|
||||
Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Lean.Meta.Tactic.Grind.ProveEq
|
||||
import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
|
||||
import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
|
||||
import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
|
||||
|
||||
/-!
|
||||
CommRing interface for cutsat. We use it to normalize nonlinear polynomials.
|
||||
-/
|
||||
|
||||
namespace Lean.Meta.Grind.Arith.Cutsat
|
||||
|
||||
/-- Returns `true` if `p` contains a nonlinear monomial. -/
|
||||
def _root_.Int.Linear.Poly.isNonlinear (p : Poly) : GoalM Bool := do
|
||||
let .add _ x p := p | return false
|
||||
if (← getVar x).isAppOf ``HMul.hMul then return true
|
||||
p.isNonlinear
|
||||
|
||||
def _root_.Int.Linear.Poly.getGeneration (p : Poly) : GoalM Nat := do
|
||||
go p 0
|
||||
where
|
||||
go : Poly → Nat → GoalM Nat
|
||||
| .num _, gen => return gen
|
||||
| .add _ x p, gen => do go p (max (← Grind.getGeneration (← getVar x)) gen)
|
||||
|
||||
def getIntRingId? : GoalM (Option Nat) := do
|
||||
CommRing.getRingId? (← getIntExpr)
|
||||
|
||||
/-- Normalize the polynomial using `CommRing`-/
|
||||
def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.RingExpr × CommRing.Poly × Poly)) := do
|
||||
unless (← p.isNonlinear) do return none
|
||||
let some ringId ← getIntRingId? | return none
|
||||
CommRing.RingM.run ringId do
|
||||
let e ← p.denoteExpr'
|
||||
-- TODO: we can avoid the following statement if we construct the `Int` denotation using
|
||||
-- Internalized operators instead of `mkIntMul` and `mkIntAdd`
|
||||
let e ← shareCommon (← canon e)
|
||||
let gen ← p.getGeneration
|
||||
let some re ← CommRing.reify? e (gen := gen) | return none
|
||||
let p' := re.toPoly
|
||||
let e' ← p'.denoteExpr
|
||||
let e' ← preprocessLight e'
|
||||
-- Remark: we are reusing the `IntModule` virtual parent.
|
||||
-- TODO: Investigate whether we should have a custom virtual parent for cutsat
|
||||
internalize e' gen (some getIntModuleVirtualParent)
|
||||
let p'' ← toPoly e'
|
||||
if p == p'' then return none
|
||||
modify' fun s => { s with usedCommRing := true }
|
||||
trace[grind.cutsat.assert.nonlinear] "{← p.pp} ===> {← p''.pp}"
|
||||
return some (re, p', p'')
|
||||
|
||||
end Lean.Meta.Grind.Arith.Cutsat
|
||||
|
|
@ -85,6 +85,14 @@ partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
|
|||
c.p.updateOccs
|
||||
modify' fun s => { s with dvds := s.dvds.set x (some c) }
|
||||
|
||||
/-- Asserts a constraint coming from the core. -/
|
||||
private def DvdCnstr.assertCore (c : DvdCnstr) : GoalM Unit := do
|
||||
if let some (re, rp, p) ← c.p.normCommRing? then
|
||||
let c := { c with p, h := .commRingNorm c re rp : DvdCnstr}
|
||||
c.assert
|
||||
else
|
||||
c.assert
|
||||
|
||||
def propagateIntDvd (e : Expr) : GoalM Unit := do
|
||||
let_expr Dvd.dvd _ inst a b ← e | return ()
|
||||
unless (← isInstDvdInt inst) do return ()
|
||||
|
|
@ -94,7 +102,7 @@ def propagateIntDvd (e : Expr) : GoalM Unit := do
|
|||
if (← isEqTrue e) then
|
||||
let p ← toPoly b
|
||||
let c := { d, p, h := .core e : DvdCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
else if (← isEqFalse e) then
|
||||
pushNewFact <| mkApp4 (mkConst ``Int.Linear.of_not_dvd) a b reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
|
||||
|
||||
|
|
@ -106,7 +114,7 @@ def propagateNatDvd (e : Expr) : GoalM Unit := do
|
|||
let p := b'.norm
|
||||
if (← isEqTrue e) then
|
||||
let c := { d, p, h := .coreNat e d b b' : DvdCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
else if (← isEqFalse e) then
|
||||
let_expr Dvd.dvd _ _ a b ← e | return ()
|
||||
pushNewFact <| mkApp3 (mkConst ``Nat.emod_pos_of_not_dvd) a b (mkOfEqFalseCore e (← mkEqFalseProof e))
|
||||
|
|
|
|||
|
|
@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
|
|||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
|
||||
|
||||
namespace Lean.Meta.Grind.Arith.Cutsat
|
||||
|
||||
|
|
@ -223,9 +224,18 @@ private def exprAsPoly (a : Expr) : GoalM Poly := do
|
|||
private def processNewIntEq (a b : Expr) : GoalM Unit := do
|
||||
let p₁ ← exprAsPoly a
|
||||
let p₂ ← exprAsPoly b
|
||||
-- Remark: we don't need to use the comm ring normalizer here because `p` is always linear.
|
||||
let p := p₁.combine (p₂.mul (-1))
|
||||
{ p, h := .core a b p₁ p₂ : EqCnstr }.assert
|
||||
|
||||
/-- Asserts a constraint coming from the core. -/
|
||||
private def EqCnstr.assertCore (c : EqCnstr) : GoalM Unit := do
|
||||
if let some (re, rp, p) ← c.p.normCommRing? then
|
||||
let c := { p, h := .commRingNorm c re rp : EqCnstr}
|
||||
c.assert
|
||||
else
|
||||
c.assert
|
||||
|
||||
private def processNewNatEq (a b : Expr) : GoalM Unit := do
|
||||
let (lhs, rhs) ← Int.OfNat.toIntEq a b
|
||||
let gen ← getGeneration a
|
||||
|
|
@ -235,7 +245,7 @@ private def processNewNatEq (a b : Expr) : GoalM Unit := do
|
|||
let p := lhs'.sub rhs' |>.norm
|
||||
let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : EqCnstr }
|
||||
trace[grind.debug.cutsat.nat] "{← c.pp}"
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
private def processNewToIntEq (a b : Expr) : ToIntM Unit := do
|
||||
let gen := max (← getGeneration a) (← getGeneration b)
|
||||
|
|
@ -246,7 +256,7 @@ private def processNewToIntEq (a b : Expr) : ToIntM Unit := do
|
|||
let rhs ← toLinearExpr b' gen
|
||||
let p := lhs.sub rhs |>.norm
|
||||
let c := { p, h := .coreToInt a b thm lhs rhs : EqCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
@[export lean_process_cutsat_eq]
|
||||
def processNewEqImpl (a b : Expr) : GoalM Unit := do
|
||||
|
|
@ -262,6 +272,8 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
|
|||
ToIntM.run α do processNewToIntEq a b
|
||||
|
||||
private def processNewIntDiseq (a b : Expr) : GoalM Unit := do
|
||||
-- Remark: we don't need to use comm ring to normalize these polynomials because they are
|
||||
-- always linear.
|
||||
let p₁ ← exprAsPoly a
|
||||
let c ← if let some 0 ← getIntValue? b then
|
||||
pure { p := p₁, h := .core0 a b : DiseqCnstr }
|
||||
|
|
@ -271,6 +283,14 @@ private def processNewIntDiseq (a b : Expr) : GoalM Unit := do
|
|||
pure {p, h := .core a b p₁ p₂ : DiseqCnstr }
|
||||
c.assert
|
||||
|
||||
/-- Asserts a constraint coming from the core. -/
|
||||
private def DiseqCnstr.assertCore (c : DiseqCnstr) : GoalM Unit := do
|
||||
if let some (re, rp, p) ← c.p.normCommRing? then
|
||||
let c := { p, h := .commRingNorm c re rp : DiseqCnstr }
|
||||
c.assert
|
||||
else
|
||||
c.assert
|
||||
|
||||
private def processNewNatDiseq (a b : Expr) : GoalM Unit := do
|
||||
let (lhs, rhs) ← Int.OfNat.toIntEq a b
|
||||
let gen ← getGeneration a
|
||||
|
|
@ -279,7 +299,7 @@ private def processNewNatDiseq (a b : Expr) : GoalM Unit := do
|
|||
let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
|
||||
let p := lhs'.sub rhs' |>.norm
|
||||
let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : DiseqCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
private def processNewToIntDiseq (a b : Expr) : ToIntM Unit := do
|
||||
let gen := max (← getGeneration a) (← getGeneration b)
|
||||
|
|
@ -290,7 +310,7 @@ private def processNewToIntDiseq (a b : Expr) : ToIntM Unit := do
|
|||
let rhs ← toLinearExpr b' gen
|
||||
let p := lhs.sub rhs |>.norm
|
||||
let c := { p, h := .coreToInt a b thm lhs rhs : DiseqCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
@[export lean_process_cutsat_diseq]
|
||||
def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
|
||||
|
|
@ -352,8 +372,12 @@ private def internalizeInt (e : Expr) : GoalM Unit := do
|
|||
-- It is pointless to assert `x = x`
|
||||
-- This can happen if `e` is a nonlinear term (e.g., `e` is `a*b`)
|
||||
return
|
||||
let c := { p := .add (-1) x p, h := .defn e p : EqCnstr }
|
||||
c.assert
|
||||
if let some (re, rp, p') ← p.normCommRing? then
|
||||
let c := { p := .add (-1) x p', h := .defnCommRing e p re rp p' : EqCnstr }
|
||||
c.assert
|
||||
else
|
||||
let c := { p := .add (-1) x p, h := .defn e p : EqCnstr }
|
||||
c.assert
|
||||
|
||||
private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
|
||||
if b == 0 || b == 1 || b == -1 then
|
||||
|
|
@ -411,8 +435,12 @@ private def internalizeNat (e : Expr) : GoalM Unit := do
|
|||
trace[grind.debug.cutsat.internalize] "{aquote natCast_e}:= {← p.pp}"
|
||||
let x ← mkVar natCast_e
|
||||
modify' fun s => { s with natDef := s.natDef.insert { expr := e } x }
|
||||
let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }
|
||||
c.assert
|
||||
if let some (re, rp, p') ← p.normCommRing? then
|
||||
let c := { p := .add (-1) x p', h := .defnNatCommRing e' x e'' p re rp p' : EqCnstr }
|
||||
c.assert
|
||||
else
|
||||
let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }
|
||||
c.assert
|
||||
|
||||
private def isToIntForbiddenParent (parent? : Option Expr) : Bool :=
|
||||
if let some parent := parent? then
|
||||
|
|
|
|||
|
|
@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
|
|||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
|
||||
|
||||
namespace Lean.Meta.Grind.Arith.Cutsat
|
||||
|
||||
|
|
@ -135,6 +136,14 @@ private def toPolyLe? (e : Expr) : GoalM (Option Poly) := do
|
|||
reportNonNormalized e; return none
|
||||
return some (← toPoly a)
|
||||
|
||||
/-- Asserts a constraint coming from the core. -/
|
||||
private def LeCnstr.assertCore (c : LeCnstr) : GoalM Unit := do
|
||||
if let some (re, rp, p) ← c.p.normCommRing? then
|
||||
let c := { p, h := .commRingNorm c re rp : LeCnstr}
|
||||
c.assert
|
||||
else
|
||||
c.assert
|
||||
|
||||
/--
|
||||
Given an expression `e` that is in `True` (or `False` equivalence class), if `e` is an
|
||||
integer inequality, asserts it to the cutsat state.
|
||||
|
|
@ -145,7 +154,7 @@ def propagateIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
|
|||
pure { p, h := .core e : LeCnstr }
|
||||
else
|
||||
pure { p := p.mul (-1) |>.addConst 1, h := .coreNeg e p : LeCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
|
||||
let some (lhs, rhs) ← Int.OfNat.toIntLe? e | return ()
|
||||
|
|
@ -158,7 +167,7 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
|
|||
pure { p, h := .coreNat e lhs rhs lhs' rhs' : LeCnstr }
|
||||
else
|
||||
pure { p := p.mul (-1) |>.addConst 1, h := .coreNatNeg e lhs rhs lhs' rhs' : LeCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
def propagateToIntLe (e : Expr) (eqTrue : Bool) : ToIntM Unit := do
|
||||
let some thm ← if eqTrue then pure (← getInfo).ofLE? else pure (← getInfo).ofNotLE? | return ()
|
||||
|
|
@ -172,7 +181,7 @@ def propagateToIntLe (e : Expr) (eqTrue : Bool) : ToIntM Unit := do
|
|||
let rhs ← toLinearExpr b' gen
|
||||
let p := lhs.sub rhs |>.norm
|
||||
let c := { p, h := .coreToInt e eqTrue thm lhs rhs : LeCnstr }
|
||||
c.assert
|
||||
c.assertCore
|
||||
|
||||
def propagateLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
|
||||
unless (← getConfig).cutsat do return ()
|
||||
|
|
|
|||
|
|
@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import Init.Grind.Ring.Poly
|
||||
import Lean.Meta.Tactic.Grind.Diseq
|
||||
import Lean.Meta.Tactic.Grind.Arith.Util
|
||||
import Lean.Meta.Tactic.Grind.Arith.ProofUtil
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
|
||||
import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
|
||||
import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
|
||||
|
||||
namespace Lean.Meta.Grind.Arith.Cutsat
|
||||
|
||||
|
|
@ -20,12 +24,15 @@ structure ProofM.State where
|
|||
polyMap : Std.HashMap Poly Expr := {}
|
||||
exprMap : Std.HashMap Int.Linear.Expr Expr := {}
|
||||
natExprMap : Std.HashMap Int.OfNat.Expr Expr := {}
|
||||
ringPolyMap : Std.HashMap CommRing.Poly Expr := {}
|
||||
ringExprMap : Std.HashMap CommRing.RingExpr Expr := {}
|
||||
|
||||
structure ProofM.Context where
|
||||
ctx : Expr
|
||||
/-- Variables before reordering -/
|
||||
ctx' : Expr
|
||||
natCtx : Expr
|
||||
ringCtx : Expr
|
||||
/--
|
||||
`unordered` is `true` if we entered a `.reorder c` justification. The variables in `c` and
|
||||
its dependencies are unordered.
|
||||
|
|
@ -64,27 +71,41 @@ private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
|
|||
modify fun s => { s with cache := s.cache.insert addr h }
|
||||
return h
|
||||
|
||||
def mkPolyDecl (p : Poly) : ProofM Expr := do
|
||||
private def mkPolyDecl (p : Poly) : ProofM Expr := do
|
||||
if let some x := (← get).polyMap[p]? then
|
||||
return x
|
||||
let x := mkFVar (← mkFreshFVarId)
|
||||
modify fun s => { s with polyMap := s.polyMap.insert p x }
|
||||
return x
|
||||
|
||||
def mkExprDecl (e : Int.Linear.Expr) : ProofM Expr := do
|
||||
private def mkExprDecl (e : Int.Linear.Expr) : ProofM Expr := do
|
||||
if let some x := (← get).exprMap[e]? then
|
||||
return x
|
||||
let x := mkFVar (← mkFreshFVarId)
|
||||
modify fun s => { s with exprMap := s.exprMap.insert e x }
|
||||
return x
|
||||
|
||||
def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
|
||||
private def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
|
||||
if let some x := (← get).natExprMap[e]? then
|
||||
return x
|
||||
let x := mkFVar (← mkFreshFVarId)
|
||||
modify fun s => { s with natExprMap := s.natExprMap.insert e x }
|
||||
return x
|
||||
|
||||
private def mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr := do
|
||||
if let some x := (← get).ringPolyMap[p]? then
|
||||
return x
|
||||
let x := mkFVar (← mkFreshFVarId)
|
||||
modify fun s => { s with ringPolyMap := s.ringPolyMap.insert p x }
|
||||
return x
|
||||
|
||||
private def mkRingExprDecl (e : CommRing.RingExpr) : ProofM Expr := do
|
||||
if let some x := (← get).ringExprMap[e]? then
|
||||
return x
|
||||
let x := mkFVar (← mkFreshFVarId)
|
||||
modify fun s => { s with ringExprMap := s.ringExprMap.insert e x }
|
||||
return x
|
||||
|
||||
private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
|
||||
if h : 0 < vars.size then
|
||||
RArray.toExpr type id (RArray.ofFn (vars[·]) h)
|
||||
|
|
@ -100,18 +121,34 @@ private def toContextExpr' : GoalM Expr := do
|
|||
private def toNatContextExpr : GoalM Expr := do
|
||||
toContextExprCore (← getNatVars) Nat.mkType
|
||||
|
||||
private def toRingContextExpr : GoalM Expr := do
|
||||
if (← get').usedCommRing then
|
||||
if let some ringId ← getIntRingId? then
|
||||
return (← CommRing.RingM.run ringId do CommRing.toContextExpr)
|
||||
RArray.toExpr Int.mkType id (RArray.leaf (mkIntLit 0))
|
||||
|
||||
private abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
|
||||
withLetDecl `ctx (mkApp (mkConst ``RArray [levelZero]) Int.mkType) (← toContextExpr) fun ctx => do
|
||||
withLetDecl `ctx' (mkApp (mkConst ``RArray [levelZero]) Int.mkType) (← toContextExpr') fun ctx' => do
|
||||
withLetDecl `rctx (mkApp (mkConst ``RArray [levelZero]) Int.mkType) (← toRingContextExpr) fun ringCtx => do
|
||||
withLetDecl `nctx (mkApp (mkConst ``RArray [levelZero]) Nat.mkType) (← toNatContextExpr) fun natCtx => do
|
||||
go { ctx, ctx', natCtx } |>.run' {}
|
||||
go { ctx, ctx', ringCtx, natCtx } |>.run' {}
|
||||
where
|
||||
go : ProofM Expr := do
|
||||
let h ← x
|
||||
let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Int.Linear.Poly) toExpr
|
||||
let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Int.Linear.Expr) toExpr
|
||||
let h ← mkLetOfMap (← get).natExprMap h `a (mkConst ``Int.OfNat.Expr) toExpr
|
||||
mkLetFVars #[(← getContext), (← read).ctx', (← getNatContext)] h
|
||||
let h ← mkLetOfMap (← get).ringPolyMap h `rp (mkConst ``Grind.CommRing.Poly) toExpr
|
||||
let h ← mkLetOfMap (← get).ringExprMap h `re (mkConst ``Grind.CommRing.Expr) toExpr
|
||||
mkLetFVars #[(← getContext), (← read).ctx', (← read).ringCtx, (← getNatContext)] h
|
||||
|
||||
/--
|
||||
Returns a Lean expression representing the auxiliary `CommRing` variable context needed for normalizing
|
||||
nonlinear polynomials.
|
||||
-/
|
||||
private abbrev getRingContext : ProofM Expr := do
|
||||
return (← read).ringCtx
|
||||
|
||||
private def DvdCnstr.get_d_a (c : DvdCnstr) : GoalM (Int × Int) := do
|
||||
let d := c.d
|
||||
|
|
@ -154,6 +191,20 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
|
|||
(← getContext) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p)
|
||||
reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .reorder c => withUnordered <| c.toExprProof
|
||||
| .commRingNorm c e p =>
|
||||
let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
|
||||
return mkApp5 (mkConst ``Int.Linear.eq_norm_poly) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
|
||||
| .defnCommRing e p re rp p' =>
|
||||
let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) reflBoolTrue
|
||||
let some x := (← getVarMap).find? { expr := e } | throwError "`grind` internal error, missing cutsat variable{indentExpr e}"
|
||||
return mkApp8 (mkConst ``Int.Linear.eq_def_norm) (← getContext)
|
||||
(toExpr x) (← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p)
|
||||
reflBoolTrue (← mkEqRefl e) h
|
||||
| .defnNatCommRing e x e' p re rp p' =>
|
||||
let h₁ := mkApp2 (mkConst ``Int.OfNat.Expr.eq_denoteAsInt) (← getNatContext) (← mkNatExprDecl e)
|
||||
let h₂ := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) reflBoolTrue
|
||||
return mkApp9 (mkConst ``Int.Linear.eq_def'_norm) (← getContext) (toExpr x) (← mkExprDecl e')
|
||||
(← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p) reflBoolTrue h₁ h₂
|
||||
|
||||
partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
|
||||
trace[grind.debug.cutsat.proof] "{← c'.pp}"
|
||||
|
|
@ -216,6 +267,9 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
|
|||
(← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (← mkPolyDecl c'.p)
|
||||
(← s.toExprProof) reflBoolTrue
|
||||
| .reorder c => withUnordered <| c.toExprProof
|
||||
| .commRingNorm c e p =>
|
||||
let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
|
||||
return mkApp6 (mkConst ``Int.Linear.dvd_norm_poly) (← getContext) (toExpr c.d) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
|
||||
|
||||
partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
|
||||
trace[grind.debug.cutsat.proof] "{← c'.pp}"
|
||||
|
|
@ -302,6 +356,9 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
|
|||
return mkApp10 (mkConst thmName)
|
||||
(← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr coeff) (← mkPolyDecl c'.p) (← s.toExprProof) reflBoolTrue
|
||||
| .reorder c => withUnordered <| c.toExprProof
|
||||
| .commRingNorm c e p =>
|
||||
let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
|
||||
return mkApp5 (mkConst ``Int.Linear.le_norm_poly) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
|
||||
|
||||
partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do
|
||||
match c'.h with
|
||||
|
|
@ -329,6 +386,9 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
|
|||
(← getContext) (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
|
||||
reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
|
||||
| .reorder c => withUnordered <| c.toExprProof
|
||||
| .commRingNorm c e p =>
|
||||
let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
|
||||
return mkApp5 (mkConst ``Int.Linear.diseq_norm_poly) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
|
||||
|
||||
partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s do
|
||||
match s.h with
|
||||
|
|
@ -412,8 +472,9 @@ open CollectDecVars
|
|||
mutual
|
||||
partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
|
||||
match c'.h with
|
||||
| .core0 .. | .core .. | .coreNat .. | .defn .. | .defnNat .. | .coreToInt .. => return () -- Equalities coming from the core never contain cutsat decision variables
|
||||
| .reorder c | .norm c | .divCoeffs c => c.collectDecVars
|
||||
| .core0 .. | .core .. | .coreNat .. | .defn .. | .defnNat ..
|
||||
| .defnCommRing .. | .defnNatCommRing .. | .coreToInt .. => return () -- Equalities coming from the core never contain cutsat decision variables
|
||||
| .commRingNorm c .. | .reorder c | .norm c | .divCoeffs c => c.collectDecVars
|
||||
| .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
|
||||
|
||||
partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited s) do
|
||||
|
|
@ -429,14 +490,15 @@ partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do
|
|||
match c'.h with
|
||||
| .core _ | .coreNat .. => return ()
|
||||
| .cooper₁ c | .cooper₂ c
|
||||
| .reorder c | .norm c | .elim c | .divCoeffs c | .ofEq _ c => c.collectDecVars
|
||||
| .commRingNorm c .. | .reorder c | .norm c | .elim c | .divCoeffs c | .ofEq _ c => c.collectDecVars
|
||||
| .solveCombine c₁ c₂ | .solveElim c₁ c₂ | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
|
||||
|
||||
partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
|
||||
match c'.h with
|
||||
| .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .coreToInt .. | .denoteAsIntNonneg .. | .bound .. => return ()
|
||||
| .dec h => markAsFound h
|
||||
| .reorder c | .cooper c | .norm c | .divCoeffs c => c.collectDecVars
|
||||
| .commRingNorm c .. | .reorder c | .cooper c
|
||||
| .norm c | .divCoeffs c => c.collectDecVars
|
||||
| .dvdTight c₁ c₂ | .negDvdTight c₁ c₂
|
||||
| .combine c₁ c₂ | .combineDivCoeffs c₁ c₂ _
|
||||
| .subst _ c₁ c₂ | .ofLeDiseq c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
|
||||
|
|
@ -445,7 +507,7 @@ partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do u
|
|||
partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
|
||||
match c'.h with
|
||||
| .core0 .. | .core .. | .coreNat .. | .coreToInt .. => return () -- Disequalities coming from the core never contain cutsat decision variables
|
||||
| .reorder c | .norm c | .divCoeffs c | .neg c => c.collectDecVars
|
||||
| .commRingNorm c .. | .reorder c | .norm c | .divCoeffs c | .neg c => c.collectDecVars
|
||||
| .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -10,6 +10,7 @@ import Lean.Data.PersistentArray
|
|||
import Lean.Meta.Tactic.Grind.ExprPtr
|
||||
import Lean.Meta.Tactic.Grind.Arith.Util
|
||||
import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
|
||||
import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
|
||||
|
||||
namespace Lean.Meta.Grind.Arith.Cutsat
|
||||
|
||||
|
|
@ -95,6 +96,9 @@ inductive EqCnstrProof where
|
|||
| subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
|
||||
| ofLeGe (c₁ : LeCnstr) (c₂ : LeCnstr)
|
||||
| reorder (c : EqCnstr)
|
||||
| commRingNorm (c : EqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
|
||||
| defnCommRing (e : Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly)
|
||||
| defnNatCommRing (e : Int.OfNat.Expr) (x : Var) (e' : Int.Linear.Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly)
|
||||
|
||||
/-- A divisibility constraint and its justification/proof. -/
|
||||
structure DvdCnstr where
|
||||
|
|
@ -156,6 +160,7 @@ inductive DvdCnstrProof where
|
|||
/-- `c.c₃?` must be `some` -/
|
||||
| cooper₂ (c : CooperSplit)
|
||||
| reorder (c : DvdCnstr)
|
||||
| commRingNorm (c : DvdCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
|
||||
|
||||
/-- An inequality constraint and its justification/proof. -/
|
||||
structure LeCnstr where
|
||||
|
|
@ -182,6 +187,7 @@ inductive LeCnstrProof where
|
|||
| dvdTight (c₁ : DvdCnstr) (c₂ : LeCnstr)
|
||||
| negDvdTight (c₁ : DvdCnstr) (c₂ : LeCnstr)
|
||||
| reorder (c : LeCnstr)
|
||||
| commRingNorm (c : LeCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
|
||||
|
||||
/-- A disequality constraint and its justification/proof. -/
|
||||
structure DiseqCnstr where
|
||||
|
|
@ -203,6 +209,7 @@ inductive DiseqCnstrProof where
|
|||
| neg (c : DiseqCnstr)
|
||||
| subst (x : Var) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
|
||||
| reorder (c : DiseqCnstr)
|
||||
| commRingNorm (c : DiseqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
|
||||
|
||||
/--
|
||||
A proof of `False`.
|
||||
|
|
@ -330,6 +337,10 @@ structure State where
|
|||
from a α-term `e` to the pair `(toInt e, α)`.
|
||||
-/
|
||||
toIntTermMap : PHashMap ExprPtr ToIntTermInfo := {}
|
||||
/--
|
||||
`usedCommRing` is `true` if the `CommRing` has been used to normalize expressions.
|
||||
-/
|
||||
usedCommRing : Bool := false
|
||||
deriving Inhabited
|
||||
|
||||
end Lean.Meta.Grind.Arith.Cutsat
|
||||
|
|
|
|||
|
|
@ -75,11 +75,12 @@ def GrindM.run (x : GrindM α) (params : Params) (fallback : Fallback) : MetaM
|
|||
let (btrueExpr, scState) := shareCommonAlpha (mkConst ``Bool.true) scState
|
||||
let (natZExpr, scState) := shareCommonAlpha (mkNatLit 0) scState
|
||||
let (ordEqExpr, scState) := shareCommonAlpha (mkConst ``Ordering.eq) scState
|
||||
let (intExpr, scState) := shareCommonAlpha Int.mkType scState
|
||||
let simprocs := params.normProcs
|
||||
let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true)
|
||||
let simp := params.norm
|
||||
let config := params.config
|
||||
x (← mkMethods fallback).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr }
|
||||
x (← mkMethods fallback).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr }
|
||||
|>.run' { scState }
|
||||
|
||||
private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do
|
||||
|
|
|
|||
|
|
@ -112,6 +112,7 @@ structure Context where
|
|||
btrueExpr : Expr
|
||||
bfalseExpr : Expr
|
||||
ordEqExpr : Expr -- `Ordering.eq`
|
||||
intExpr : Expr -- `Int`
|
||||
|
||||
/-- Key for the congruence theorem cache. -/
|
||||
structure CongrTheoremCacheKey where
|
||||
|
|
@ -246,6 +247,10 @@ def getNatZeroExpr : GrindM Expr := do
|
|||
def getOrderingEqExpr : GrindM Expr := do
|
||||
return (← readThe Context).ordEqExpr
|
||||
|
||||
/-- Returns the internalized `Int`. -/
|
||||
def getIntExpr : GrindM Expr := do
|
||||
return (← readThe Context).intExpr
|
||||
|
||||
def cheapCasesOnly : GrindM Bool :=
|
||||
return (← readThe Context).cheapCases
|
||||
|
||||
|
|
|
|||
|
|
@ -1,16 +0,0 @@
|
|||
|
||||
open Lean.Grind
|
||||
|
||||
variable [CommRing R] [LinearOrder R] [OrderedRing R]
|
||||
example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
|
||||
example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
|
||||
|
||||
-- These don't work because `cutsat` disables `linarith`.
|
||||
-- We could use the CommRing normalizer in cutsat to solve these.
|
||||
example (a b : Int) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
|
||||
example (a b : Int) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
|
||||
|
||||
-- These should work by embedding `Nat` into its Grothendieck completion,
|
||||
-- and using that the embedding is monotone.
|
||||
example (a b : Nat) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
|
||||
example (a b : Nat) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
|
||||
|
|
@ -57,25 +57,3 @@ set_option trace.Meta.debug true
|
|||
example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by
|
||||
rw [left_comm] -- Introduces a new (non-canonical) instance for `Mul Nat`
|
||||
grind on_failure fallback -- State should have only 3 `*`-applications
|
||||
|
||||
|
||||
set_option pp.notation false in
|
||||
set_option pp.explicit true in
|
||||
/--
|
||||
trace: [Meta.debug] [@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
|
||||
(@NatCast.natCast Int instNatCastInt a),
|
||||
@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
|
||||
(@NatCast.natCast Int instNatCastInt d),
|
||||
@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a,
|
||||
@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b d]
|
||||
-/
|
||||
#guard_msgs (trace) in
|
||||
example (a b c d : Nat) : b * a = d * b → False := by
|
||||
rw [CommMonoid.mul_comm d b] -- Introduces a new (non-canonical) instance for `Mul Nat`
|
||||
-- See target here
|
||||
guard_target =ₛ
|
||||
@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a
|
||||
=
|
||||
@HMul.hMul Nat Nat Nat (@instHMul Nat (@Semigroup.toMul Nat (@Monoid.toSemigroup Nat (@CommMonoid.toMonoid Nat instCommMonoidNat)))) b d
|
||||
→ False
|
||||
grind on_failure fallback -- State should have only 2 `*`-applications, and they use the same instance
|
||||
|
|
|
|||
39
tests/lean/run/grind_cutsat_commring.lean
Normal file
39
tests/lean/run/grind_cutsat_commring.lean
Normal file
|
|
@ -0,0 +1,39 @@
|
|||
open Lean.Grind
|
||||
|
||||
variable [CommRing R] [LinearOrder R] [OrderedRing R]
|
||||
example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
|
||||
example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
|
||||
|
||||
example (a b : Int) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
|
||||
example (a b : Int) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
|
||||
|
||||
example (a b : Nat) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
|
||||
example (a b : Nat) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
|
||||
example (a b : Nat) (h : 7 ≤ a * b + b) : 7 ≤ b + b * a := by grind
|
||||
|
||||
example (a b : Int) (h₁ : 2 ∣ a*b) (h₂ : 2 ∣ 2*b*a + 1 - a*b) : False := by grind
|
||||
example (a b : Int) (h₁ : 2 ∣ a*b) : 2 ∣ b*a := by grind
|
||||
example (a b : Int) (h₁ : 3 ∣ a*b + b + c) (h₂ : 3 ∣ b*a + b + c + 1) : False := by grind
|
||||
|
||||
example (a b : Nat) (h₁ : 2 ∣ a*b) (h₂ : 2 ∣ b*a + 1) : False := by grind
|
||||
example (a b : Nat) (h₁ : 2 ∣ 2*a*b + b) (h₂ : 2 ∣ b + 2*b*a + 1) : False := by grind
|
||||
|
||||
example (a b : Int) (h : a + 1 = a * b) : 2 * b * a - 2 * a ≤ 2 := by grind
|
||||
example (a b : Int) (h : a + 1 = b * a) : 2 * a * b - 2 * a ≤ 2 := by grind
|
||||
example (a b : Int) (h : a + 1 = 3 * b * a) : 6 * a * b - 2 * a ≤ 2 := by grind
|
||||
example (a b c : Int) (h₁ : a + 1 + c = b * a) (h₂ : c + 2*b*a = 0) : 6 * a * b - 2 * a ≤ 2 := by grind
|
||||
|
||||
example (a b : Nat) (h : a + a * b = 1) : 2 * b * a + 2 * a ≤ 2 := by grind
|
||||
example (a b : Nat) (h : a + b * a = 1) : 2 * a * b + 2 * a ≤ 2 := by grind
|
||||
example (a b : Nat) (h : a + 2 * b * a = 10) : 2 * a * b + a ≤ 10 := by grind
|
||||
example (a b : Nat) (h : a + 2 * b * a = a^2 + b) : 2 * a * b ≤ b + a*a:= by grind
|
||||
|
||||
example (a b : Int) (h : a + 1 = b * a) : 2 * a * b - 2 * a ≤ 2 := by grind
|
||||
|
||||
example (a b : Int) (h₁ : a + 1 ≠ a * b) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
|
||||
example (a b : Int) (h₁ : a + 1 ≠ b * a) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
|
||||
example (a b : Int) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := by grind
|
||||
|
||||
example (a b : Nat) (h₁ : a + 1 ≠ a * b) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
|
||||
example (a b : Nat) (h₁ : a + 1 ≠ b * a) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
|
||||
example (a b : Nat) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := by grind
|
||||
|
|
@ -32,7 +32,8 @@ trace: [grind.cutsat.assert] -1*↑a ≤ 0
|
|||
[grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
|
||||
[grind.cutsat.assert] -1*「1」 + 1 = 0
|
||||
[grind.cutsat.assert] -1*↑c ≤ 0
|
||||
[grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
|
||||
[grind.cutsat.assert] -1*「↑a * ↑b + -1 * ↑c + 1」 + 「↑a * ↑b」 + -1*↑c + 1 = 0
|
||||
[grind.cutsat.assert] 「↑a * ↑b」 + -1*↑c + 1 ≤ 0
|
||||
[grind.cutsat.assert] -1*↑0 = 0
|
||||
[grind.cutsat.assert] ↑c = 0
|
||||
[grind.cutsat.assert] 0 ≤ 0
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue