feat: generate Nullstellensatz proof terms in grind (#8122)
This PR implements the generation of compact proof terms for Nullstellensatz certificates in the new commutative ring procedure in `grind`. Some examples: ```lean example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by grind +ring example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by grind +ring example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by grind +ring example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by grind +ring ```
This commit is contained in:
Leonardo de Moura
GitHub
parent
685aa9b359
commit
d64ae32965
11 changed files with 281 additions and 113 deletions
|
|
@ -325,7 +325,7 @@ class NoZeroNatDivisors (α : Type u) [CommRing α] where
|
|||
|
||||
export NoZeroNatDivisors (no_zero_nat_divisors)
|
||||
|
||||
theorem no_zero_int_divisors (α : Type u) [CommRing α] [NoZeroNatDivisors α] {k : Int} (a : α)
|
||||
theorem no_zero_int_divisors {α : Type u} [CommRing α] [NoZeroNatDivisors α] {k : Int} {a : α}
|
||||
: k ≠ 0 → k * a = 0 → a = 0 := by
|
||||
match k with
|
||||
| (k : Nat) =>
|
||||
|
|
|
|||
|
|
@ -700,33 +700,6 @@ theorem Expr.eq_of_toPoly_eq {α} [CommRing α] (ctx : Context α) (a b : Expr)
|
|||
simp [denote_toPoly] at h
|
||||
assumption
|
||||
|
||||
def ne_unsat_cert (a b : Expr) : Bool :=
|
||||
(a.sub b).toPoly == .num 0
|
||||
|
||||
theorem ne_unsat {α} [CommRing α] (ctx : Context α) (a b : Expr)
|
||||
: ne_unsat_cert a b → a.denote ctx ≠ b.denote ctx → False := by
|
||||
simp [ne_unsat_cert]
|
||||
intro h
|
||||
replace h := congrArg (Poly.denote ctx .) h
|
||||
simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_zero_iff] at h
|
||||
assumption
|
||||
|
||||
def eq_unsat_cert (a b : Expr) (k : Int) : Bool :=
|
||||
k != 0 && (a.sub b).toPoly == .num k
|
||||
|
||||
-- Remark: `[IsCharP α 0]` after `(ctx : Context α)` is not a mistake.
|
||||
-- The `grind` procedure assumes that support theorems start with `{α} [CommRing α] (ctx : Context α)`
|
||||
theorem eq_unsat {α} [CommRing α] (ctx : Context α) [IsCharP α 0] (a b : Expr) (k : Int)
|
||||
: eq_unsat_cert a b k → a.denote ctx = b.denote ctx → False := by
|
||||
simp [eq_unsat_cert]
|
||||
intro h₁ h₂
|
||||
replace h₂ := congrArg (Poly.denote ctx .) h₂
|
||||
simp [Poly.denote, Expr.denote, Expr.denote_toPoly, intCast_zero, sub_eq_iff] at h₂
|
||||
have := IsCharP.intCast_eq_zero_iff (α := α) 0 k
|
||||
simp [h₁] at this
|
||||
rw [h₂, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
|
||||
assumption
|
||||
|
||||
/-- Helper theorem for proving `NullCert` theorems. -/
|
||||
theorem NullCert.eqsImplies_helper {α} [CommRing α] (ctx : Context α) (nc : NullCert) (p : Prop) : (nc.denote ctx = 0 → p) → nc.eqsImplies ctx p := by
|
||||
induction nc <;> simp [denote, eqsImplies]
|
||||
|
|
@ -742,7 +715,7 @@ theorem NullCert.denote_toPoly {α} [CommRing α] (ctx : Context α) (nc : NullC
|
|||
def NullCert.eq_cert (nc : NullCert) (lhs rhs : Expr) :=
|
||||
(lhs.sub rhs).toPoly == nc.toPoly
|
||||
|
||||
theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
|
||||
theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) {lhs rhs : Expr}
|
||||
: nc.eq_cert lhs rhs → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
|
||||
simp [eq_cert]; intro h₁
|
||||
apply eqsImplies_helper
|
||||
|
|
@ -751,6 +724,46 @@ theorem NullCert.eq {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs r
|
|||
simp [Expr.denote_toPoly, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁
|
||||
assumption
|
||||
|
||||
theorem NullCert.eqsImplies_helper' {α} [CommRing α] {ctx : Context α} {nc : NullCert} {p q : Prop} : nc.eqsImplies ctx p → (p → q) → nc.eqsImplies ctx q := by
|
||||
induction nc <;> simp [denote, eqsImplies]
|
||||
next => intro h₁ h₂; exact h₂ h₁
|
||||
next ih => intro h₁ h₂ h₃; exact ih (h₁ h₃) h₂
|
||||
|
||||
theorem NullCert.ne_unsat {α} [CommRing α] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
|
||||
: nc.eq_cert lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
|
||||
intro h₁ h₂
|
||||
exact eqsImplies_helper' (eq ctx nc h₁) h₂
|
||||
|
||||
def NullCert.ne_nzdiv_unsat_cert (nc : NullCert) (k : Int) (lhs rhs : Expr) : Bool :=
|
||||
k ≠ 0 && (lhs.sub rhs).toPoly.mulConst k == nc.toPoly
|
||||
|
||||
theorem NullCert.ne_nzdiv_unsat {α} [CommRing α] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr)
|
||||
: nc.ne_nzdiv_unsat_cert k lhs rhs → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
|
||||
simp [ne_nzdiv_unsat_cert]
|
||||
intro h₁ h₂ h₃
|
||||
apply eqsImplies_helper
|
||||
intro h₄
|
||||
replace h₂ := congrArg (Poly.denote ctx) h₂
|
||||
simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, h₄, Expr.denote] at h₂
|
||||
replace h₂ := no_zero_int_divisors h₁ h₂
|
||||
rw [sub_eq_zero_iff] at h₂
|
||||
exact h₃ h₂
|
||||
|
||||
def NullCert.eq_unsat_cert (nc : NullCert) (k : Int) : Bool :=
|
||||
k ≠ 0 && nc.toPoly == .num k
|
||||
|
||||
theorem NullCert.eq_unsat {α} [CommRing α] [IsCharP α 0] (ctx : Context α) (nc : NullCert) (k : Int)
|
||||
: nc.eq_unsat_cert k → nc.eqsImplies ctx False := by
|
||||
simp [eq_unsat_cert]
|
||||
intro h₁ h₂
|
||||
apply eqsImplies_helper
|
||||
intro h₃
|
||||
replace h₂ := congrArg (Poly.denote ctx) h₂
|
||||
simp [Expr.denote_toPoly, Poly.denote_mulConst, denote_toPoly, Expr.denote, h₃, Poly.denote] at h₂
|
||||
have := IsCharP.intCast_eq_zero_iff (α := α) 0 k
|
||||
simp [← h₂] at this
|
||||
contradiction
|
||||
|
||||
/-!
|
||||
Theorems for justifying the procedure for commutative rings with a characteristic in `grind`.
|
||||
-/
|
||||
|
|
@ -877,45 +890,55 @@ theorem Expr.eq_of_toPolyC_eq {α c} [CommRing α] [IsCharP α c] (ctx : Context
|
|||
simp [denote_toPolyC] at h
|
||||
assumption
|
||||
|
||||
def ne_unsatC_cert (a b : Expr) (c : Nat) : Bool :=
|
||||
(a.sub b).toPolyC c == .num 0
|
||||
|
||||
theorem ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr)
|
||||
: ne_unsatC_cert a b c → a.denote ctx ≠ b.denote ctx → False := by
|
||||
simp [ne_unsatC_cert]
|
||||
intro h
|
||||
replace h := congrArg (Poly.denote ctx .) h
|
||||
simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_zero_iff] at h
|
||||
assumption
|
||||
|
||||
def eq_unsatC_cert (a b : Expr) (c : Nat) (k : Int) : Bool :=
|
||||
k != 0 && k % c != 0 && (a.sub b).toPolyC c == .num k
|
||||
|
||||
theorem eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (a b : Expr) (k : Int)
|
||||
: eq_unsatC_cert a b c k → a.denote ctx = b.denote ctx → False := by
|
||||
simp [eq_unsatC_cert]
|
||||
intro h₁ h₂ h₃
|
||||
replace h₃ := congrArg (Poly.denote ctx .) h₃
|
||||
simp [Poly.denote, Expr.denote, Expr.denote_toPolyC, intCast_zero, sub_eq_iff] at h₃
|
||||
have := IsCharP.intCast_eq_zero_iff (α := α) c k
|
||||
simp [h₁, h₂] at this
|
||||
rw [h₃, Eq.comm, ← sub_eq_iff, sub_self, Eq.comm]
|
||||
assumption
|
||||
|
||||
theorem NullCert.denote_toPolyC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) : (nc.toPolyC c).denote ctx = nc.denote ctx := by
|
||||
induction nc <;> simp [toPolyC, denote, Poly.denote, intCast_zero, Poly.denote_combineC, Poly.denote_mulC, Expr.denote_toPolyC, Expr.denote, *]
|
||||
|
||||
def NullCert.eq_certC (nc : NullCert) (lhs rhs : Expr) (c : Nat) :=
|
||||
(lhs.sub rhs).toPolyC c == nc.toPoly
|
||||
(lhs.sub rhs).toPolyC c == nc.toPolyC c
|
||||
|
||||
theorem NullCert.eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
|
||||
theorem NullCert.eqC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) {lhs rhs : Expr}
|
||||
: nc.eq_certC lhs rhs c → nc.eqsImplies ctx (lhs.denote ctx = rhs.denote ctx) := by
|
||||
simp [eq_certC]; intro h₁
|
||||
apply eqsImplies_helper
|
||||
intro h₂
|
||||
replace h₁ := congrArg (Poly.denote ctx) h₁
|
||||
simp [Expr.denote_toPolyC, denote_toPoly, h₂, Expr.denote, sub_eq_zero_iff] at h₁
|
||||
simp [Expr.denote_toPolyC, denote_toPolyC, h₂, Expr.denote, sub_eq_zero_iff] at h₁
|
||||
assumption
|
||||
|
||||
theorem NullCert.ne_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (lhs rhs : Expr)
|
||||
: nc.eq_certC lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
|
||||
intro h₁ h₂
|
||||
exact eqsImplies_helper' (eqC ctx nc h₁) h₂
|
||||
|
||||
def NullCert.ne_nzdiv_unsat_certC (nc : NullCert) (k : Int) (lhs rhs : Expr) (c : Nat) : Bool :=
|
||||
k ≠ 0 && ((lhs.sub rhs).toPolyC c).mulConstC k c == nc.toPolyC c
|
||||
|
||||
theorem NullCert.ne_nzdiv_unsatC {α c} [CommRing α] [IsCharP α c] [NoZeroNatDivisors α] (ctx : Context α) (nc : NullCert) (k : Int) (lhs rhs : Expr)
|
||||
: nc.ne_nzdiv_unsat_certC k lhs rhs c → lhs.denote ctx ≠ rhs.denote ctx → nc.eqsImplies ctx False := by
|
||||
simp [ne_nzdiv_unsat_certC]
|
||||
intro h₁ h₂ h₃
|
||||
apply eqsImplies_helper
|
||||
intro h₄
|
||||
replace h₂ := congrArg (Poly.denote ctx) h₂
|
||||
simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₄, Expr.denote] at h₂
|
||||
replace h₂ := no_zero_int_divisors h₁ h₂
|
||||
rw [sub_eq_zero_iff] at h₂
|
||||
exact h₃ h₂
|
||||
|
||||
def NullCert.eq_unsat_certC (nc : NullCert) (k : Int) (c : Nat) : Bool :=
|
||||
k % c != 0 && nc.toPolyC c == .num k
|
||||
|
||||
theorem NullCert.eq_unsatC {α c} [CommRing α] [IsCharP α c] (ctx : Context α) (nc : NullCert) (k : Int)
|
||||
: nc.eq_unsat_certC k c → nc.eqsImplies ctx False := by
|
||||
simp [eq_unsat_certC]
|
||||
intro h₁ h₂
|
||||
apply eqsImplies_helper
|
||||
intro h₃
|
||||
replace h₂ := congrArg (Poly.denote ctx) h₂
|
||||
simp [Expr.denote_toPolyC, Poly.denote_mulConstC, denote_toPolyC, h₃, Poly.denote] at h₂
|
||||
have := IsCharP.intCast_eq_zero_iff (α := α) c k
|
||||
simp [h₂] at this
|
||||
contradiction
|
||||
|
||||
end CommRing
|
||||
end Lean.Grind
|
||||
|
|
|
|||
|
|
@ -30,5 +30,6 @@ builtin_initialize registerTraceClass `grind.ring.simp
|
|||
builtin_initialize registerTraceClass `grind.ring.superpose
|
||||
|
||||
builtin_initialize registerTraceClass `grind.debug.ring.simp
|
||||
builtin_initialize registerTraceClass `grind.debug.ring.proof
|
||||
|
||||
end Lean
|
||||
|
|
|
|||
|
|
@ -74,4 +74,7 @@ def EqCnstr.denoteExpr (c : EqCnstr) : RingM Expr := do
|
|||
def PolyDerivation.denoteExpr (d : PolyDerivation) : RingM Expr := do
|
||||
d.p.denoteExpr
|
||||
|
||||
def DiseqCnstr.denoteExpr (c : DiseqCnstr) : RingM Expr := do
|
||||
return mkNot (← mkEq (← c.d.denoteExpr) (← denoteNum 0))
|
||||
|
||||
end Lean.Meta.Grind.Arith.CommRing
|
||||
|
|
|
|||
|
|
@ -130,7 +130,7 @@ def EqCnstr.checkConstant (c : EqCnstr) : RingM Bool := do
|
|||
if k == 0 then
|
||||
trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}"
|
||||
else if (← hasChar) then
|
||||
setUnsatEq c
|
||||
c.setUnsat
|
||||
else
|
||||
-- Remark: we currently don't do anything if the characteristic is not known.
|
||||
trace_goal[grind.ring.assert.discard] "{← c.denoteExpr}"
|
||||
|
|
@ -219,6 +219,28 @@ def addNewEq (c : EqCnstr) : RingM Unit := do
|
|||
else
|
||||
c.addToQueue
|
||||
|
||||
/-- Returns `true` if `c.d.p` is the constant polynomial. -/
|
||||
def DiseqCnstr.checkConstant (c : DiseqCnstr) : RingM Bool := do
|
||||
let .num k := c.d.p | return false
|
||||
if k == 0 then
|
||||
c.setUnsat
|
||||
else
|
||||
trace_goal[grind.ring.assert.trivial] "{← c.denoteExpr}"
|
||||
return true
|
||||
|
||||
def DiseqCnstr.simplify (c : DiseqCnstr) : RingM DiseqCnstr := do
|
||||
return { c with d := (← c.d.simplify) }
|
||||
|
||||
def saveDiseq (c : DiseqCnstr) : RingM Unit := do
|
||||
trace_goal[grind.ring.assert.store] "{← c.denoteExpr}"
|
||||
modifyRing fun s => { s with diseqs := s.diseqs.push c }
|
||||
|
||||
def addNewDiseq (c : DiseqCnstr) : RingM Unit := do
|
||||
let c ← c.simplify
|
||||
if (← c.checkConstant) then
|
||||
return ()
|
||||
saveDiseq c
|
||||
|
||||
@[export lean_process_ring_eq]
|
||||
def processNewEqImpl (a b : Expr) : GoalM Unit := do
|
||||
if isSameExpr a b then return () -- TODO: check why this is needed
|
||||
|
|
@ -228,17 +250,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
|
|||
let some ra ← toRingExpr? a | return ()
|
||||
let some rb ← toRingExpr? b | return ()
|
||||
let p ← (ra.sub rb).toPolyM
|
||||
-- TODO: delete this `if` after simplifier is fully integrated
|
||||
if let .num k := p then
|
||||
if k == 0 then
|
||||
trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} = 0"
|
||||
else if (← hasChar) then
|
||||
trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} = 0"
|
||||
setEqUnsat k a b ra rb
|
||||
else
|
||||
-- Remark: we currently don't do anything if the characteristic is not known.
|
||||
trace_goal[grind.ring.assert.discard] "{← p.denoteExpr} = 0"
|
||||
return ()
|
||||
addNewEq (← mkEqCnstr p (.core a b ra rb))
|
||||
|
||||
@[export lean_process_ring_diseq]
|
||||
|
|
@ -249,16 +260,10 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
|
|||
let some ra ← toRingExpr? a | return ()
|
||||
let some rb ← toRingExpr? b | return ()
|
||||
let p ← (ra.sub rb).toPolyM
|
||||
if let .num k := p then
|
||||
if k == 0 then
|
||||
trace_goal[grind.ring.assert.unsat] "{← p.denoteExpr} ≠ 0"
|
||||
setNeUnsat a b ra rb
|
||||
else
|
||||
-- Remark: if the characteristic is known, it is trivial.
|
||||
-- Otherwise, we don't do anything.
|
||||
trace_goal[grind.ring.assert.trivial] "{← p.denoteExpr} ≠ 0"
|
||||
return ()
|
||||
trace_goal[grind.ring.assert.store] "{← p.denoteExpr} ≠ 0"
|
||||
-- TODO: save disequalitys
|
||||
addNewDiseq {
|
||||
lhs := a, rhs := b
|
||||
rlhs := ra, rrhs := rb
|
||||
d := .input p
|
||||
}
|
||||
|
||||
end Lean.Meta.Grind.Arith.CommRing
|
||||
|
|
|
|||
|
|
@ -47,6 +47,9 @@ structure PreNullCert where
|
|||
d : Int := 1
|
||||
deriving Inhabited
|
||||
|
||||
def PreNullCert.zero : PreNullCert :=
|
||||
{ qs := #[] }
|
||||
|
||||
def PreNullCert.unit (i : Nat) (n : Nat) : PreNullCert :=
|
||||
let qs := Array.replicate n (.num 0)
|
||||
let qs := qs.set! i (.num 1)
|
||||
|
|
@ -131,6 +134,23 @@ partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching
|
|||
| .mul k c => (← c.toPreNullCert).mul k
|
||||
| .div k c => (← c.toPreNullCert).div k
|
||||
|
||||
def PolyDerivation.toPreNullCert (d : PolyDerivation) : ProofM PreNullCert := do
|
||||
match d with
|
||||
| .input _ => return .zero
|
||||
| .step _p k₁ d k₂ m₂ c₂ =>
|
||||
-- Recall that _p = k₁*d.getPoly + k₂*m₂*c.p
|
||||
trace[grind.debug.ring.proof] ">> k₁: {k₁}, {(← d.toPreNullCert).d}, {(← c₂.toPreNullCert).d}"
|
||||
(← d.toPreNullCert).combine k₁ .unit (-k₂) m₂ (← c₂.toPreNullCert)
|
||||
|
||||
/-- Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`. -/
|
||||
def PolyDerivation.getMultiplier (d : PolyDerivation) : Int :=
|
||||
go d 1
|
||||
where
|
||||
go (d : PolyDerivation) (acc : Int) : Int :=
|
||||
match d with
|
||||
| .input _ => acc
|
||||
| .step _ k₁ d .. => go d (k₁ * acc)
|
||||
|
||||
structure NullCertExt where
|
||||
d : Int
|
||||
qhs : Array (Poly × NullCertHypothesis)
|
||||
|
|
@ -139,6 +159,10 @@ def EqCnstr.mkNullCertExt (c : EqCnstr) : RingM NullCertExt := do
|
|||
let (nc, s) ← c.toPreNullCert.run {}
|
||||
return { d := nc.d, qhs := nc.qs.zip s.hyps }
|
||||
|
||||
def DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM NullCertExt := do
|
||||
let (nc, s) ← c.d.toPreNullCert.run {}
|
||||
return { d := nc.d, qhs := nc.qs.zip s.hyps }
|
||||
|
||||
def NullCertExt.toPoly (nc : NullCertExt) : RingM Poly := do
|
||||
let mut p : Poly := .num 0
|
||||
for (q, h) in nc.qhs do
|
||||
|
|
@ -150,33 +174,75 @@ def NullCertExt.check (c : EqCnstr) (nc : NullCertExt) : RingM Bool := do
|
|||
let p₂ ← nc.toPoly
|
||||
return p₁ == p₂
|
||||
|
||||
def setUnsatEq (c : EqCnstr) : RingM Unit := do
|
||||
trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
|
||||
let nc ← c.mkNullCertExt
|
||||
trace_goal[grind.ring.assert.unsat] "{nc.d}*({← c.p.denoteExpr}), {← (← nc.toPoly).denoteExpr}"
|
||||
trace_goal[grind.ring.assert.unsat] "{nc.d}*({← c.p.denoteExpr}), {← nc.qhs.mapM fun (p, h) => return (← p.denoteExpr, ← h.lhs.denoteExpr, ← h.rhs.denoteExpr) }"
|
||||
-- TODO
|
||||
def NullCertExt.toNullCert (nc : NullCertExt) : Grind.CommRing.NullCert :=
|
||||
go nc.qhs.size .empty (by omega)
|
||||
where
|
||||
go (i : Nat) (acc : Grind.CommRing.NullCert) (h : i ≤ nc.qhs.size) : Grind.CommRing.NullCert :=
|
||||
if h : i > 0 then
|
||||
let i := i - 1
|
||||
let (p, h) := nc.qhs[i]
|
||||
go i (.add p h.lhs h.rhs acc) (by omega)
|
||||
else
|
||||
acc
|
||||
|
||||
private def mkLemmaPrefix (declName declNameC : Name) : RingM Expr := do
|
||||
/--
|
||||
Given a `pr`, returns `pr h₁ ... hₙ`, where `n` is size `nc.qhs.size`, and `hᵢ`s
|
||||
are the equalities in the certificate.
|
||||
-/
|
||||
def NullCertExt.applyEqs (pr : Expr) (nc : NullCertExt) : Expr :=
|
||||
go 0 pr
|
||||
where
|
||||
go (i : Nat) (pr : Expr) : Expr :=
|
||||
if _ : i < nc.qhs.size then
|
||||
let (_, h) := nc.qhs[i]
|
||||
go (i + 1) (mkApp pr h.h)
|
||||
else
|
||||
pr
|
||||
|
||||
private def getNoZeroDivInstIfNeeded? (k : Int) : RingM (Option Expr) := do
|
||||
if k == 1 then
|
||||
return none
|
||||
else
|
||||
let some inst ← noZeroDivisorsInst?
|
||||
| throwError "`grind` internal error, `NoZeroNatDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
|
||||
return some inst
|
||||
|
||||
def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
|
||||
trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
|
||||
let .num k := c.p
|
||||
| throwError "`grind` internal error, constant polynomial expected {indentExpr (← c.p.denoteExpr)}"
|
||||
let ncx ← c.mkNullCertExt
|
||||
trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
|
||||
let ring ← getRing
|
||||
let some (charInst, char) := ring.charInst?
|
||||
| throwError "`grind` internal error, `IsCharP` insrtance is needed, but it is not available for{indentExpr (← getRing).type}"
|
||||
let h := if char == 0 then
|
||||
mkApp (mkConst ``Grind.CommRing.NullCert.eq_unsat [ring.u]) ring.type
|
||||
else
|
||||
mkApp2 (mkConst ``Grind.CommRing.NullCert.eq_unsatC [ring.u]) ring.type (toExpr char)
|
||||
let ctx ← toContextExpr
|
||||
let nc := toExpr (ncx.toNullCert)
|
||||
let h := mkApp6 h ring.commRingInst charInst ctx nc (toExpr k) reflBoolTrue
|
||||
closeGoal <| ncx.applyEqs h
|
||||
|
||||
def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
|
||||
trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
|
||||
let ncx ← c.mkNullCertExt
|
||||
trace_goal[grind.ring.assert.unsat] "{ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
|
||||
let nc := toExpr (ncx.toNullCert)
|
||||
let ring ← getRing
|
||||
let ctx ← toContextExpr
|
||||
if let some (charInst, c) ← nonzeroCharInst? then
|
||||
return mkApp5 (mkConst declNameC [ring.u]) ring.type (toExpr c) ring.commRingInst charInst ctx
|
||||
else
|
||||
return mkApp3 (mkConst declName [ring.u]) ring.type ring.commRingInst ctx
|
||||
|
||||
-- TODO: delete
|
||||
def setNeUnsat (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
|
||||
let h ← mkLemmaPrefix ``Grind.CommRing.ne_unsat ``Grind.CommRing.ne_unsatC
|
||||
closeGoal <| mkApp4 h (toExpr ra) (toExpr rb) reflBoolTrue (← mkDiseqProof a b)
|
||||
|
||||
-- TODO: delete
|
||||
def setEqUnsat (k : Int) (a b : Expr) (ra rb : RingExpr) : RingM Unit := do
|
||||
let mut h ← mkLemmaPrefix ``Grind.CommRing.eq_unsat ``Grind.CommRing.eq_unsatC
|
||||
let (charInst, c) ← getCharInst
|
||||
if c == 0 then
|
||||
h := mkApp h charInst
|
||||
closeGoal <| mkApp5 h (toExpr ra) (toExpr rb) (toExpr k) reflBoolTrue (← mkEqProof a b)
|
||||
|
||||
let k := c.d.getMultiplier
|
||||
let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with
|
||||
| some (charInst, char), some nzDivInst =>
|
||||
mkApp8 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k)
|
||||
| some (charInst, char), none =>
|
||||
mkApp6 (mkConst ``Grind.CommRing.NullCert.ne_unsatC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx nc
|
||||
| none, some nzDivInst =>
|
||||
mkApp6 (mkConst ``Grind.CommRing.NullCert.ne_nzdiv_unsat [ring.u]) ring.type ring.commRingInst nzDivInst ctx nc (toExpr k)
|
||||
| none, none =>
|
||||
mkApp4 (mkConst ``Grind.CommRing.NullCert.ne_unsat [ring.u]) ring.type ring.commRingInst ctx nc
|
||||
let h := mkApp4 h (toExpr c.rlhs) (toExpr c.rrhs) reflBoolTrue (← mkDiseqProof c.lhs c.rhs)
|
||||
closeGoal <| ncx.applyEqs h
|
||||
|
||||
end Lean.Meta.Grind.Arith.CommRing
|
||||
|
|
|
|||
|
|
@ -54,4 +54,13 @@ instance : ToExpr CommRing.Expr where
|
|||
toExpr := ofRingExpr
|
||||
toTypeExpr := mkConst ``CommRing.Expr
|
||||
|
||||
def ofNullCert (nc : NullCert) : Expr :=
|
||||
match nc with
|
||||
| .empty => mkConst ``CommRing.NullCert.empty
|
||||
| .add q lhs rhs nc => mkApp4 (mkConst ``CommRing.NullCert.add) (toExpr q) (toExpr lhs) (toExpr rhs) (ofNullCert nc)
|
||||
|
||||
instance : ToExpr CommRing.NullCert where
|
||||
toExpr := ofNullCert
|
||||
toTypeExpr := mkConst ``CommRing.NullCert
|
||||
|
||||
end Lean.Meta.Grind.Arith.CommRing
|
||||
|
|
|
|||
|
|
@ -54,13 +54,13 @@ using the equations `x - 1 = 0` (`c₁`) and `y - 2 = 0` (`c₂`).
|
|||
```
|
||||
2*x^2 + x*y | s₁ := .input (2*x^2 + x*y)
|
||||
= - 2*x*(x - 1)
|
||||
(2*x + x*y) | s₂ := .simp (2*x + x*y) c₁ 1 (-2) x s₁
|
||||
(2*x + x*y) | s₂ := .step (2*x + x*y) 1 s₁ (-2) x c₁
|
||||
= - 2*1*(x - 1)
|
||||
(x*y + 2) | s₃ := .simp (x*y + 2) c₁ 1 (-2) 1 s₂
|
||||
(x*y + 2) | s₃ := .step (x*y + 2) 1 s₂ (-2) 1 c₁
|
||||
= - 1*y*(x - 1)
|
||||
(y + 2) | s₄ := .simp (y+2) c₁ 1 (-1) y s₃
|
||||
(y + 2) | s₄ := .step (y+2) 1 s₃ (-1) y c₁
|
||||
= - 1*1*(y - 2)
|
||||
4 | s₅ := .simp 4 c₂ 1 1 1 s₄
|
||||
4 | s₅ := .step 4 1 s₄ 1 1 c₂
|
||||
```
|
||||
From the chain above, we build the certificate
|
||||
```
|
||||
|
|
@ -88,12 +88,12 @@ inductive PolyDerivation where
|
|||
x + y + z | s₁ := .input (x + y + z)
|
||||
*2
|
||||
= - 1*1*(2*x - 1)
|
||||
2*y + 2*z + 1 | s₂ := .simp (2*y + 2*z + 1) c₁ 2 (-1) 1 s₁
|
||||
2*y + 2*z + 1 | s₂ := .step (2*y + 2*z + 1) 2 s₁ (-1) 1 c₁
|
||||
*3
|
||||
= - 2*1*(3*y - 1)
|
||||
6*z + 5 | s₃ := .simp (6*z + 5) c₂ 3 (-2) 1 s₂
|
||||
6*z + 5 | s₃ := .step (6*z + 5) 3 s₂ (-2) 1 c₂
|
||||
= - 1*1*(6*z + 5)
|
||||
0 | s₄ := .simp (0) c₃ 1 (-1) 1 s₃
|
||||
0 | s₄ := .step (0) 1 s₃ (-1) 1 c₃
|
||||
```
|
||||
For this chain, we build the certificate
|
||||
```
|
||||
|
|
@ -115,6 +115,17 @@ def PolyDerivation.p : PolyDerivation → Poly
|
|||
| .input p => p
|
||||
| .step p .. => p
|
||||
|
||||
/-- A disequality `lhs ≠ rhs` asserted by the core. -/
|
||||
structure DiseqCnstr where
|
||||
lhs : Expr
|
||||
rhs : Expr
|
||||
/-- Reified `lhs` -/
|
||||
rlhs : RingExpr
|
||||
/-- Reified `rhs` -/
|
||||
rrhs : RingExpr
|
||||
/-- `lhs - rhs` simplication chain. If it becomes `0` we have an inconsistency. -/
|
||||
d : PolyDerivation
|
||||
|
||||
/-- State for each `CommRing` processed by this module. -/
|
||||
structure Ring where
|
||||
id : Nat
|
||||
|
|
@ -154,6 +165,9 @@ structure Ring where
|
|||
in the leading monomial is `x`.
|
||||
-/
|
||||
varToBasis : PArray (List EqCnstr) := {}
|
||||
/-- Disequalities. -/
|
||||
-- TODO: add indexing
|
||||
diseqs : PArray DiseqCnstr := {}
|
||||
deriving Inhabited
|
||||
|
||||
/-- State for all `CommRing` types detected by `grind`. -/
|
||||
|
|
|
|||
|
|
@ -61,6 +61,9 @@ def nonzeroCharInst? : RingM (Option (Expr × Nat)) := do
|
|||
return some (inst, c)
|
||||
return none
|
||||
|
||||
def noZeroDivisorsInst? : RingM (Option Expr) := do
|
||||
return (← getRing).noZeroDivInst?
|
||||
|
||||
/--
|
||||
Returns `true` if the current ring satifies the property
|
||||
```
|
||||
|
|
|
|||
44
tests/lean/run/grind_ring_2.lean
Normal file
44
tests/lean/run/grind_ring_2.lean
Normal file
|
|
@ -0,0 +1,44 @@
|
|||
set_option grind.warning false
|
||||
open Lean.Grind
|
||||
|
||||
example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example [CommRing α] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
|
||||
fail_if_success grind +ring
|
||||
sorry
|
||||
|
||||
example [CommRing α] (x y : α) : x = 1 → y = 2 → 2*x + y = 4 := by
|
||||
grind +ring
|
||||
|
||||
example [CommRing α] [IsCharP α 7] (x y : α) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example [CommRing α] [IsCharP α 7] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example [CommRing α] [IsCharP α 8] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
|
||||
fail_if_success grind +ring
|
||||
sorry
|
||||
|
||||
example [CommRing α] [IsCharP α 8] [NoZeroNatDivisors α] (x y : α) : 2*x = 1 → 2*y = 1 → x + y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example (x y : UInt8) : 3*x = 1 → 3*y = 2 → x + y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example (x y : UInt8) : 3*x = 1 → 3*y = 2 → False := by
|
||||
fail_if_success grind +ring
|
||||
sorry
|
||||
|
||||
example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 6*x = 1 → 3*y = 2 → 2*x + y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example [CommRing α] [NoZeroNatDivisors α] (x y : α) : 600000*x = 1 → 300*y = 2 → 200000*x + 100*y = 1 := by
|
||||
grind +ring
|
||||
|
||||
example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
|
||||
grind +ring
|
||||
|
||||
example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
|
||||
grind +ring
|
||||
|
|
@ -37,4 +37,4 @@ def nc : NullCert := .add q₁ lhs₁ rhs₁ (.add q₂ lhs₂ rhs₂ .empty)
|
|||
|
||||
example (x y : Int) : x = y → y - x*y + y^2 = 1 → y = 1 :=
|
||||
let ctx := #R[x, y]
|
||||
nc.eq ctx lhs rhs (Eq.refl true)
|
||||
nc.eq ctx (lhs := lhs) (rhs := rhs) (Eq.refl true)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue