chore: remove grind +ringNull option (#9954)
This PR removes the option `grind +ringNull`. It provided an alternative proof term construction for the `grind ring` module, but it was less effective than the default proof construction mode and had effectively become dead code. This PR also optimizes semiring normalization proof terms using the infrastructure added in #9946. **Remark:** After updating stage0, we can remove several background theorems from the `Init/Grind` folder.
This commit is contained in:
Leonardo de Moura
GitHub
parent
84fecdc042
commit
a4496a4a6b
6 changed files with 43 additions and 321 deletions
|
|
@ -102,11 +102,6 @@ structure Config where
|
|||
ring := true
|
||||
ringSteps := 10000
|
||||
/--
|
||||
When `true` (default: `false`), the commutative ring procedure in `grind` constructs stepwise
|
||||
proof terms, instead of a single-step Nullstellensatz certificate
|
||||
-/
|
||||
ringNull := false
|
||||
/--
|
||||
When `true` (default: `true`), uses procedure for handling linear arithmetic for `IntModule`, and
|
||||
`CommRing`.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -341,7 +341,6 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
|
|||
let p ← (ra.sub rb).toPolyM
|
||||
addNewEq (← mkEqCnstr p (.core a b ra rb))
|
||||
else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do
|
||||
if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter
|
||||
trace_goal[grind.ring.assert] "{← mkEq a b}"
|
||||
let some sa ← toSemiringExpr? a | return ()
|
||||
let some sb ← toSemiringExpr? b | return ()
|
||||
|
|
@ -405,7 +404,6 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
|
|||
}
|
||||
else if let some semiringId ← inSameSemiring? a b then SemiringM.run semiringId do
|
||||
if (← getAddRightCancelInst?).isSome then
|
||||
if (← getConfig).ringNull then return () -- TODO: remove after we add Nullstellensatz certificates for semiring adapter
|
||||
trace_goal[grind.ring.assert] "{mkNot (← mkEq a b)}"
|
||||
let some sa ← toSemiringExpr? a | return ()
|
||||
let some sb ← toSemiringExpr? b | return ()
|
||||
|
|
|
|||
|
|
@ -19,181 +19,27 @@ import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
|
|||
public section
|
||||
|
||||
namespace Lean.Meta.Grind.Arith.CommRing
|
||||
|
||||
def toContextExprCore (vars : Array Expr) : RingM Expr := do
|
||||
/--
|
||||
Returns a context of type `RArray α` containing the variables `vars` where
|
||||
`α` is the type of the ring.
|
||||
-/
|
||||
private def toContextExpr (vars : Array Expr) : RingM Expr := do
|
||||
let ring ← getRing
|
||||
if h : 0 < vars.size then
|
||||
RArray.toExpr ring.type id (RArray.ofFn (vars[·]) h)
|
||||
else
|
||||
RArray.toExpr ring.type id (RArray.leaf (mkApp (← getNatCastFn) (toExpr 0)))
|
||||
|
||||
/--
|
||||
Returns a context of type `RArray α` containing the variables of the given ring.
|
||||
`α` is the type of the ring.
|
||||
-/
|
||||
def toContextExpr : RingM Expr := do
|
||||
toContextExprCore (← getRing).vars.toArray
|
||||
|
||||
private def toSContextExprCore' (vars : Array Expr) : SemiringM Expr := do
|
||||
private def toSContextExpr' (vars : Array Expr) : SemiringM Expr := do
|
||||
let semiring ← getSemiring
|
||||
if h : 0 < vars.size then
|
||||
RArray.toExpr semiring.type id (RArray.ofFn (vars[·]) h)
|
||||
else
|
||||
RArray.toExpr semiring.type id (RArray.leaf (mkApp (← getNatCastFn') (toExpr 0)))
|
||||
|
||||
private def toSContextExpr' : SemiringM Expr := do
|
||||
toSContextExprCore' (← getSemiring).vars.toArray
|
||||
|
||||
/-- Similar to `toContextExpr`, but for semirings. -/
|
||||
private def toSContextExpr (semiringId : Nat) (vars : Array Expr) : RingM Expr := do
|
||||
SemiringM.run semiringId do toSContextExprCore' vars
|
||||
|
||||
def throwNoNatZeroDivisors : RingM α := do
|
||||
throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
|
||||
|
||||
def getPolyConst (p : Poly) : RingM Int := do
|
||||
let .num k := p
|
||||
| throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
|
||||
return k
|
||||
|
||||
namespace Null
|
||||
/-!
|
||||
Proof term for a Nullstellensatz certificate.
|
||||
-/
|
||||
|
||||
/--
|
||||
A "pre" Nullstellensatz certificate.
|
||||
Recall that, given the hypotheses `h₁ : lhs₁ = rhs₁` ... `hₙ : lhsₙ = rhsₙ`,
|
||||
a Nullstellensatz certificate is of the form
|
||||
```
|
||||
q₁*(lhs₁ - rhs₁) + ... + qₙ*(lhsₙ - rhsₙ)
|
||||
```
|
||||
Each hypothesis is an `EqCnstr` justified by a `.core ..` `EqnCnstrProof`.
|
||||
We dynamically associate them with unique indices based on the order we find them
|
||||
during traversal.
|
||||
For the other `EqCnstr`s we compute a "pre" certificate as a dense array
|
||||
containing `q₁` ... `qₙ` needed to create the `EqCnstr`.
|
||||
|
||||
We are assuming the number of hypotheses used to derive a conclusion is small
|
||||
and a dense array is a reasonable representation.
|
||||
-/
|
||||
structure PreNullCert where
|
||||
qs : Array Poly
|
||||
/--
|
||||
We don't use rational coefficients in the polynomials.
|
||||
Thus, we need to track a denominator to justify the proof step `div`.
|
||||
-/
|
||||
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)
|
||||
{ qs }
|
||||
|
||||
def PreNullCert.div (c : PreNullCert) (k : Int) : RingM PreNullCert := do
|
||||
return { c with d := c.d * k }
|
||||
|
||||
def PreNullCert.mul (c : PreNullCert) (k : Int) : RingM PreNullCert := do
|
||||
if k == 1 then
|
||||
return c
|
||||
else
|
||||
let g := Int.gcd k c.d
|
||||
let k := k / g
|
||||
let d := c.d / g
|
||||
if k == 1 then
|
||||
return { c with d }
|
||||
else
|
||||
let qs ← c.qs.mapM fun q => q.mulConstM k
|
||||
return { qs, d }
|
||||
|
||||
def PreNullCert.combine (k₁ : Int) (m₁ : Mon) (c₁ : PreNullCert) (k₂ : Int) (m₂ : Mon) (c₂ : PreNullCert) : RingM PreNullCert := do
|
||||
let d₁ := c₁.d
|
||||
let d₂ := c₂.d
|
||||
let k₁_d₂ := k₁*d₂
|
||||
let k₂_d₁ := k₂*d₁
|
||||
let d₁_d₂ := d₁*d₂
|
||||
let g := Int.gcd (Int.gcd k₁_d₂ k₂_d₁) d₁_d₂
|
||||
let k₁ := k₁_d₂ / g
|
||||
let k₂ := k₂_d₁ / g
|
||||
let d := d₁_d₂ / g
|
||||
let qs₁ := c₁.qs
|
||||
let qs₂ := c₂.qs
|
||||
let n := Nat.max qs₁.size qs₂.size
|
||||
let mut qs : Vector Poly n := Vector.replicate n (.num 0)
|
||||
for h : i in *...n do
|
||||
if h₁ : i < qs₁.size then
|
||||
let q₁ ← qs₁[i].mulMonM k₁ m₁
|
||||
if h₂ : i < qs₂.size then
|
||||
let q₂ ← qs₂[i].mulMonM k₂ m₂
|
||||
qs := qs.set i (← q₁.combineM q₂)
|
||||
else
|
||||
qs := qs.set i q₁
|
||||
else
|
||||
have : i < n := Std.PRange.lt_upper_of_mem h
|
||||
have : qs₁.size = n ∨ qs₂.size = n := by simp +zetaDelta only [Nat.max_def, right_eq_ite_iff]; split <;> simp [*]
|
||||
have : i < qs₂.size := by omega
|
||||
let q₂ ← qs₂[i].mulMonM k₂ m₂
|
||||
qs := qs.set i q₂
|
||||
return { qs := qs.toArray, d }
|
||||
|
||||
structure NullCertHypothesis where
|
||||
h : Expr
|
||||
lhs : RingExpr
|
||||
rhs : RingExpr
|
||||
|
||||
structure ProofM.State where
|
||||
/-- Mapping from `EqCnstr` to `PreNullCert` -/
|
||||
cache : Std.HashMap UInt64 PreNullCert := {}
|
||||
hyps : Array NullCertHypothesis := #[]
|
||||
|
||||
abbrev ProofM := StateRefT ProofM.State RingM
|
||||
|
||||
private abbrev caching (c : α) (k : ProofM PreNullCert) : ProofM PreNullCert := do
|
||||
let addr := unsafe (ptrAddrUnsafe c).toUInt64 >>> 2
|
||||
if let some h := (← get).cache[addr]? then
|
||||
return h
|
||||
else
|
||||
let h ← k
|
||||
modify fun s => { s with cache := s.cache.insert addr h }
|
||||
return h
|
||||
|
||||
structure NullCertExt where
|
||||
d : Int
|
||||
qhs : Array (Poly × NullCertHypothesis)
|
||||
|
||||
end Null
|
||||
|
||||
section
|
||||
open Null
|
||||
partial def EqCnstr.toPreNullCert (c : EqCnstr) : ProofM PreNullCert := caching c do
|
||||
match c.h with
|
||||
| .core a b lhs rhs =>
|
||||
let i := (← get).hyps.size
|
||||
let h ← mkEqProof a b
|
||||
modify fun s => { s with hyps := s.hyps.push { h, lhs, rhs } }
|
||||
return PreNullCert.unit i (i+1)
|
||||
| .coreS _a _b _sa _sb _ra _rb =>
|
||||
throwError "`grind +ringNull` is not supported yet for this goal"
|
||||
| .superpose k₁ m₁ c₁ k₂ m₂ c₂ => (← c₁.toPreNullCert).combine k₁ m₁ k₂ m₂ (← c₂.toPreNullCert)
|
||||
| .simp k₁ c₁ k₂ m₂ c₂ => (← c₁.toPreNullCert).combine k₁ .unit k₂ m₂ (← c₂.toPreNullCert)
|
||||
| .mul k c => (← c.toPreNullCert).mul k
|
||||
| .div k c => (← c.toPreNullCert).div k
|
||||
| .gcd .. | .numEq0 .. =>
|
||||
throwError "`grind +ringNull` is not supported yet for this goal"
|
||||
|
||||
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)
|
||||
| .normEq0 .. =>
|
||||
throwError "`grind +ringNull` is not supported yet for this goal"
|
||||
SemiringM.run semiringId do toSContextExpr' vars
|
||||
|
||||
/-- Returns the multiplier `k` for the input polynomial. See comment at `PolyDerivation.step`. -/
|
||||
def PolyDerivation.getMultiplier (d : PolyDerivation) : Int :=
|
||||
|
|
@ -205,126 +51,13 @@ where
|
|||
| .step _ k₁ d .. => go d (k₁ * acc)
|
||||
| .normEq0 _ d .. => go d acc
|
||||
|
||||
def EqCnstr.mkNullCertExt (c : EqCnstr) : RingM NullCertExt := do
|
||||
let (nc, s) ← c.toPreNullCert.run {}
|
||||
return { d := nc.d, qhs := nc.qs.zip s.hyps }
|
||||
private def throwNoNatZeroDivisors : RingM α := do
|
||||
throwError "`grind` internal error, `NoNatZeroDivisors` instance is needed, but it is not available for{indentExpr (← getRing).type}"
|
||||
|
||||
def PolyDerivation.mkNullCertExt (d : PolyDerivation) : RingM NullCertExt := do
|
||||
let (nc, s) ← d.toPreNullCert.run {}
|
||||
return { d := nc.d, qhs := nc.qs.zip s.hyps }
|
||||
|
||||
def DiseqCnstr.mkNullCertExt (c : DiseqCnstr) : RingM NullCertExt :=
|
||||
c.d.mkNullCertExt
|
||||
end
|
||||
|
||||
namespace Null
|
||||
def NullCertExt.toPoly (nc : NullCertExt) : RingM Poly := do
|
||||
let mut p : Poly := .num 0
|
||||
for (q, h) in nc.qhs do
|
||||
p ← p.combineM (← q.mulM (← (h.lhs.sub h.rhs).toPolyM))
|
||||
return p
|
||||
|
||||
def NullCertExt.check (c : EqCnstr) (nc : NullCertExt) : RingM Bool := do
|
||||
let p₁ := c.p.mulConst' nc.d (← nonzeroChar?)
|
||||
let p₂ ← nc.toPoly
|
||||
return p₁ == p₂
|
||||
|
||||
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
|
||||
|
||||
/--
|
||||
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? | throwNoNatZeroDivisors
|
||||
return some inst
|
||||
|
||||
def setEqUnsat (c : EqCnstr) : RingM Unit := do
|
||||
trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
|
||||
let k ← getPolyConst c.p
|
||||
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` instance is needed, but it is not available for{indentExpr (← getRing).type}\nconsider not using `+ringNull`"
|
||||
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) eagerReflBoolTrue
|
||||
closeGoal <| ncx.applyEqs h
|
||||
|
||||
def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do
|
||||
trace_goal[grind.ring.assert.unsat] "{← c.denoteExpr}"
|
||||
let ncx ← c.mkNullCertExt
|
||||
trace_goal[grind.ring.assert.unsat] "multiplier: {c.d.getMultiplier}, {ncx.d}*({← c.d.p.denoteExpr}), {← (← ncx.toPoly).denoteExpr}"
|
||||
let nc := toExpr (ncx.toNullCert)
|
||||
let ring ← getRing
|
||||
let ctx ← toContextExpr
|
||||
let k := c.d.getMultiplier * ncx.d
|
||||
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) eagerReflBoolTrue (← mkDiseqProof c.lhs c.rhs)
|
||||
closeGoal <| ncx.applyEqs h
|
||||
|
||||
def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do
|
||||
let ncx ← d.mkNullCertExt
|
||||
let nc := toExpr (ncx.toNullCert)
|
||||
let ring ← getRing
|
||||
let ctx ← toContextExpr
|
||||
let k := d.getMultiplier * ncx.d
|
||||
let h := match (← nonzeroCharInst?), (← getNoZeroDivInstIfNeeded? k) with
|
||||
| some (charInst, char), some nzDivInst =>
|
||||
mkApp8 (mkConst ``Grind.CommRing.NullCert.eq_nzdivC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst nzDivInst ctx nc (toExpr k)
|
||||
| some (charInst, char), none =>
|
||||
mkApp6 (mkConst ``Grind.CommRing.NullCert.eqC [ring.u]) ring.type (toExpr char) ring.commRingInst charInst ctx nc
|
||||
| none, some nzDivInst =>
|
||||
mkApp6 (mkConst ``Grind.CommRing.NullCert.eq_nzdiv [ring.u]) ring.type ring.commRingInst nzDivInst ctx nc (toExpr k)
|
||||
| none, none =>
|
||||
mkApp4 (mkConst ``Grind.CommRing.NullCert.eq [ring.u]) ring.type ring.commRingInst ctx nc
|
||||
let h := mkApp3 h (toExpr ra) (toExpr rb) eagerReflBoolTrue
|
||||
trace_goal[grind.debug.ring.impEq] "{a}, {b}"
|
||||
let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b
|
||||
pushEq a b <| mkExpectedPropHint (ncx.applyEqs h) eq
|
||||
|
||||
end Null
|
||||
|
||||
namespace Stepwise
|
||||
/-!
|
||||
Alternative proof term construction where we generate a sub-term for each step in
|
||||
the derivation.
|
||||
-/
|
||||
private def getPolyConst (p : Poly) : RingM Int := do
|
||||
let .num k := p
|
||||
| throwError "`grind` internal error, constant polynomial expected {indentExpr (← p.denoteExpr)}"
|
||||
return k
|
||||
|
||||
structure ProofM.State where
|
||||
cache : Std.HashMap UInt64 Expr := {}
|
||||
|
|
@ -369,16 +102,16 @@ local macro "declare! " decls:ident a:ident : term =>
|
|||
modify fun s => { s with $decls:ident := (s.$decls).insert $a x };
|
||||
return x)
|
||||
|
||||
def mkPolyDecl (p : Poly) : ProofM Expr := do
|
||||
private def mkPolyDecl (p : Poly) : ProofM Expr := do
|
||||
declare! polyDecls p
|
||||
|
||||
def mkExprDecl (e : RingExpr) : ProofM Expr := do
|
||||
private def mkExprDecl (e : RingExpr) : ProofM Expr := do
|
||||
declare! exprDecls e
|
||||
|
||||
def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do
|
||||
private def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do
|
||||
declare! sexprDecls e
|
||||
|
||||
def mkMonDecl (m : Mon) : ProofM Expr := do
|
||||
private def mkMonDecl (m : Mon) : ProofM Expr := do
|
||||
declare! monDecls m
|
||||
|
||||
private def mkStepBasicPrefix (declName : Name) : ProofM Expr := do
|
||||
|
|
@ -516,7 +249,7 @@ private def mkContext (h : Expr) : ProofM Expr := do
|
|||
if h.hasLooseBVars then
|
||||
let ring ← getRing
|
||||
let ctxType := mkApp (mkConst ``RArray [ring.u]) ring.type
|
||||
let ctxVal ← toContextExprCore vars
|
||||
let ctxVal ← toContextExpr vars
|
||||
return .letE `ctx ctxType ctxVal h (nondep := false)
|
||||
else
|
||||
return h
|
||||
|
|
@ -549,7 +282,7 @@ where
|
|||
mkSemiringContext h
|
||||
|
||||
open Lean.Grind.CommRing in
|
||||
def setEqUnsat (c : EqCnstr) : RingM Unit := do
|
||||
def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
|
||||
let h ← withProofContext do
|
||||
let ring ← getRing
|
||||
if let some (charInst, char) := ring.charInst? then
|
||||
|
|
@ -565,7 +298,7 @@ def setEqUnsat (c : EqCnstr) : RingM Unit := do
|
|||
throwError "`grind ring` internal error, unexpected unsat eq proof {← c.denoteExpr}"
|
||||
closeGoal h
|
||||
|
||||
def setDiseqUnsat (c : DiseqCnstr) : RingM Unit := do
|
||||
def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
|
||||
let h ← withProofContext do
|
||||
let heq ← mkImpEqExprProof c.rlhs c.rrhs c.d
|
||||
let hne ← if let some (sa, sb) := c.ofSemiring? then
|
||||
|
|
@ -583,34 +316,21 @@ def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Uni
|
|||
let eq := mkApp3 (mkConst ``Eq [.succ ring.u]) ring.type a b
|
||||
pushEq a b <| mkExpectedPropHint heq eq
|
||||
|
||||
end Stepwise
|
||||
|
||||
def EqCnstr.setUnsat (c : EqCnstr) : RingM Unit := do
|
||||
if (← getConfig).ringNull then
|
||||
Null.setEqUnsat c
|
||||
else
|
||||
Stepwise.setEqUnsat c
|
||||
|
||||
def DiseqCnstr.setUnsat (c : DiseqCnstr) : RingM Unit := do
|
||||
if (← getConfig).ringNull then
|
||||
Null.setDiseqUnsat c
|
||||
else
|
||||
Stepwise.setDiseqUnsat c
|
||||
|
||||
def propagateEq (a b : Expr) (ra rb : RingExpr) (d : PolyDerivation) : RingM Unit := do
|
||||
if (← getConfig).ringNull then
|
||||
Null.propagateEq a b ra rb d
|
||||
else
|
||||
Stepwise.propagateEq a b ra rb d
|
||||
|
||||
/--
|
||||
Given `a` and `b`, such that `a ≠ b` in the core and `sa` and `sb` their reified semiring
|
||||
terms s.t. `sa.toPoly == sb.toPoly`, close the goal.
|
||||
-/
|
||||
def setSemiringDiseqUnsat (a b : Expr) (sa sb : SemiringExpr) : SemiringM Unit := do
|
||||
let ctx ← toSContextExpr'
|
||||
let semiring ← getSemiring
|
||||
let hne ← mkDiseqProof a b
|
||||
let usedVars := sa.collectVars >> sb.collectVars <| {}
|
||||
let vars' := usedVars.toArray
|
||||
let varRename := mkVarRename vars'
|
||||
let vars := (← getSemiring).vars
|
||||
let vars := vars'.map fun x => vars[x]!
|
||||
let sa := sa.renameVars varRename
|
||||
let sb := sb.renameVars varRename
|
||||
let ctx ← toSContextExpr' vars
|
||||
let h := mkApp3 (mkConst ``Grind.Ring.OfSemiring.eq_normS [semiring.u]) semiring.type semiring.commSemiringInst ctx
|
||||
let h := mkApp3 h (toExpr sa) (toExpr sb) eagerReflBoolTrue
|
||||
closeGoal (mkApp hne h)
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
// update me!
|
||||
#include "util/options.h"
|
||||
|
||||
namespace lean {
|
||||
|
|
|
|||
|
|
@ -40,15 +40,9 @@ example [CommRing α] [NoNatZeroDivisors α] (x y : α) : 600000*x = 1 → 300*y
|
|||
example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
|
||||
grind
|
||||
|
||||
example (x y : Int) : y = 0 → (x + 1)*(x - 1) + y = x^2 → False := by
|
||||
grind +ringNull
|
||||
|
||||
example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
|
||||
grind
|
||||
|
||||
example (x y z : BitVec 8) : z = y → (x + 1)*(x - 1)*y + y = z*x^2 + 1 → False := by
|
||||
grind +ringNull
|
||||
|
||||
example [CommRing α] (x y : α) : x*y*x = 1 → x*y*y = y → y = 1 := by
|
||||
grind
|
||||
|
||||
|
|
|
|||
|
|
@ -11,4 +11,18 @@ example (a b : R) : (a + 2 * b)^2 = 4 * b^2 + b * 4 * a + a^2 := by grind
|
|||
|
||||
example (a b : R) : (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind
|
||||
|
||||
/--
|
||||
trace: [grind.debug.proof] fun h h_1 =>
|
||||
h_1
|
||||
(Ring.OfSemiring.eq_normS (RArray.branch 1 (RArray.leaf a) (RArray.leaf b))
|
||||
(((Ring.OfSemiring.Expr.var 0).add (Ring.OfSemiring.Expr.var 1)).pow 2)
|
||||
((((Ring.OfSemiring.Expr.var 0).pow 2).add
|
||||
(((Ring.OfSemiring.Expr.num 2).mul (Ring.OfSemiring.Expr.var 0)).mul (Ring.OfSemiring.Expr.var 1))).add
|
||||
((Ring.OfSemiring.Expr.var 1).pow 2))
|
||||
(eagerReduce (Eq.refl true)))
|
||||
-/
|
||||
#guard_msgs in -- context should contain only `a` and `b`
|
||||
set_option trace.grind.debug.proof true in
|
||||
example (a b c d : R) : c + d = d → (a + b)^2 ≠ a^2 + 2 * a * b + b^2 → False := by grind
|
||||
|
||||
end CommSemiring
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue