max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: trim grind cutsat proof context (#9945)

Browse source 
This PR optimizes the proof terms produced by `grind cutsat`. It removes
unused entries from the context objects when generating the final proof,
significantly reducing the amount of junk in the resulting terms.
Example:
```lean
/--
trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
      let ctx := RArray.leaf (f 2);
      let p_1 := Poly.add 1 0 (Poly.num 0);
      let p_2 := Poly.add (-1) 0 (Poly.num 1);
      let p_3 := Poly.num 1;
      le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1)
-/
#guard_msgs in -- Context should contain only `f 2`
open Lean Int Linear in
set_option trace.grind.debug.proof true in
example (f : Nat → Int) :
    f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 → 
    f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
  grind
```
This commit is contained in:
Leonardo de Moura 2025-08-16 19:53:19 -07:00 • committed by GitHub
parent 4a6004b8fa
commit 010468699f
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 311 additions and 85 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Meta/Tactic/Grind/Arith.lean
View file

@ -15,5 +15,6 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat
public import Lean.Meta.Tactic.Grind.Arith.CommRing
public import Lean.Meta.Tactic.Grind.Arith.Linear
public import Lean.Meta.Tactic.Grind.Arith.Simproc
public import Lean.Meta.Tactic.Grind.Arith.VarRename
public section

1
src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean
View file

@ -19,6 +19,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
public section

40
src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
View file

@ -17,7 +17,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
public section
namespace Lean.Meta.Grind.Arith.CommRing
/--
Returns a context of type `RArray α` containing the variables of the given ring.
`α` is the type of the ring.
@ -354,33 +353,24 @@ private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
modify fun s => { s with cache := s.cache.insert addr h }
return h
local macro "declare! " decls:ident a:ident : term =>
`(do if let some x := (← get).$decls[$a]? then
return x
let x := mkFVar (← mkFreshFVarId);
modify fun s => { s with $decls:ident := (s.$decls).insert $a x };
return x)
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
declare! polyMap p
def mkExprDecl (e : RingExpr) : 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
declare! exprMap e
def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do
if let some x := (← get).sexprMap[e]? then
return x
let x := mkFVar (← mkFreshFVarId)
modify fun s => { s with sexprMap := s.sexprMap.insert e x }
return x
declare! sexprMap e
def mkMonDecl (m : Mon) : ProofM Expr := do
if let some x := (← get).monMap[m]? then
return x
let x := mkFVar (← mkFreshFVarId)
modify fun s => { s with monMap := s.monMap.insert m x }
return x
declare! monMap m
private def mkStepBasicPrefix (declName : Name) : ProofM Expr := do
let ctx ← getContext
@ -516,10 +506,10 @@ private abbrev withProofContext (x : ProofM Expr) : RingM Expr := do
where
go : ProofM Expr := do
let h ← x
let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.CommRing.Poly) toExpr
let h ← mkLetOfMap (← get).monMap h `m (mkConst ``Grind.CommRing.Mon) toExpr
let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.CommRing.Expr) toExpr
let h ← mkLetOfMap (← get).sexprMap h `s (mkConst ``Grind.Ring.OfSemiring.Expr) toExpr
let h := mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.CommRing.Poly) toExpr
let h := mkLetOfMap (← get).monMap h `m (mkConst ``Grind.CommRing.Mon) toExpr
let h := mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.CommRing.Expr) toExpr
let h := mkLetOfMap (← get).sexprMap h `s (mkConst ``Grind.Ring.OfSemiring.Expr) toExpr
let h ← if let some sctx := (← read).sctx? then mkLetFVars #[sctx] h else pure h
mkLetFVars #[(← getContext)] h

58
src/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.lean Normal file
View 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
-/
module
prelude
public import Init.Grind.Ring.Poly
public import Lean.Meta.Tactic.Grind.Arith.VarRename
namespace Lean.Grind.CommRing
open Lean.Meta.Grind.Arith
public def Power.renameVars (pw : Power) (f : VarRename) : Power :=
{ pw with x := (f pw.x) }
public def Mon.renameVars (m : Mon) (f : VarRename) : Mon :=
match m with
| .unit => .unit
| .mult pw m => .mult (pw.renameVars f) (renameVars m f)
public def Poly.renameVars (p : Poly) (f : VarRename) : Poly :=
match p with
| .num _ => p
| .add k m p => .add k (m.renameVars f) (renameVars p f)
public def Expr.renameVars (e : Expr) (f : VarRename) : Expr :=
match e with
| .num .. | .natCast .. | .intCast .. => e
| .var x => .var (f x)
| .neg a => .neg (renameVars a f)
| .add a b => .add (renameVars a f) (renameVars b f)
| .sub a b => .sub (renameVars a f) (renameVars b f)
| .mul a b => .mul (renameVars a f) (renameVars b f)
| .pow a k => .pow (renameVars a f) k
public def Power.collectVars (pw : Power) : VarCollector :=
collectVar pw.x
public def Mon.collectVars (m : Mon) : VarCollector :=
match m with
| .unit => id
| .mult pw m => pw.collectVars >> m.collectVars
public def Poly.collectVars (p : Poly) : VarCollector :=
match p with
| .num _ => id
| .add _ m p => m.collectVars >> p.collectVars
public def Expr.collectVars (e : Expr) : VarCollector :=
match e with
| .num .. | .natCast .. | .intCast .. => id
| .var x => collectVar x
| .neg a | .pow a _ => a.collectVars
| .add a b | .sub a b | .mul a b => a.collectVars >> b.collectVars
end Lean.Grind.CommRing

1
src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
View file

@ -21,6 +21,7 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.MBTC
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
public section

181
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
View file

@ -14,6 +14,9 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
public import Lean.Meta.Tactic.Grind.Arith.VarRename
import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
public section
@ -22,12 +25,47 @@ namespace Lean.Meta.Grind.Arith.Cutsat
deriving instance Hashable for Int.Linear.Expr
/--
State for the cutsat proof construction monad.
The final proof may reference only a small subset of the cutsat variables.
Thus, we normalize the variables and remove any that are unused from the context.
The variable order must be preserved, as the cutsat auxiliary theorems assume the polynomials are ordered.
Another complication is that cutsat may reorder variables during the search.
This is why we maintain two fields: `vars` and `vars'`.
We create auxiliary free variables for variables, polynomials, and expressions.
Cutsat also uses the ring solver to normalize nonlinear polynomials.
Remark: after normalization variable declarations are expanded. We do not create let-declarations for them
since they are just a numeral.
Remark: if cutsat did not reorder variables during the search, then the prime variables and declarations
are not used.
Remark: recall that the `.reorder` proof objects are delimiters for indicating whether regular variables and
declarations or the prime ones should be used.
-/
structure ProofM.State where
cache : Std.HashMap UInt64 Expr := {}
polyMap : Std.HashMap Poly Expr := {}
exprMap : Std.HashMap Int.Linear.Expr Expr := {}
ringPolyMap : Std.HashMap CommRing.Poly Expr := {}
ringExprMap : Std.HashMap CommRing.RingExpr Expr := {}
/-- Cache for visited cutsat proof terms. The key is the pointer address. -/
cache : Std.HashMap UInt64 Expr := {}
/-- Map from used variables to (temporary) free variable. -/
varDecls : Std.HashMap Var Expr := {}
/-- Map from used polynomials to free variable. -/
polyDecls : Std.HashMap Poly Expr := {}
/-- Map from used cutsat expressions to free variable. -/
exprDecls : Std.HashMap Int.Linear.Expr Expr := {}
/-- Map from used variables (before reordering) to (temporary) free variable. -/
varDecls' : Std.HashMap Var Expr := {}
/-- Map from used polynomials (before reordering) to free variable. -/
polyDecls' : Std.HashMap Poly Expr := {}
/-- Map from used cutsat expressions (before reordering) to free variable. -/
exprDecls' : Std.HashMap Int.Linear.Expr Expr := {}
/-- Map from used ring polynomials to free variable. -/
ringPolyDecls : Std.HashMap CommRing.Poly Expr := {}
/-- Map from used ring expressions to free variable. -/
ringExprDecls : Std.HashMap CommRing.RingExpr Expr := {}
structure ProofM.Context where
ctx : Expr
@ -44,7 +82,7 @@ structure ProofM.Context where
abbrev ProofM := ReaderT ProofM.Context (StateRefT ProofM.State GoalM)
/-- Returns a Lean expression representing the variable context used to construct cutsat proofs. -/
private abbrev getContext : ProofM Expr := do
private def getContext : ProofM Expr := do
return (← read).ctx
/--
@ -54,7 +92,11 @@ We use this combinator to process `.reorder c` justifications.
private abbrev withUnordered (k : ProofM α) : ProofM α := do
withReader (fun c => { c with ctx := c.ctx', unordered := true }) k
private abbrev getVarMap : ProofM (PHashMap ExprPtr Var) := do
/--
Returns the mapping from expressions to cutsat variables.
These are variables before the renaming them.
-/
private def getVarMap : ProofM (PHashMap ExprPtr Var) := do
if (← read).unordered then
return (← get').varMap'
else
@ -69,65 +111,94 @@ private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
modify fun s => { s with cache := s.cache.insert addr h }
return h
local macro "declare! " decls:ident a:ident : term =>
`(do if let some x := (← get).$decls[$a]? then
return x
let x := mkFVar (← mkFreshFVarId);
modify fun s => { s with $decls:ident := (s.$decls).insert $a x };
return x)
private def mkVarDecl (x : Var) : ProofM Expr := do
if (← read).unordered then
declare! varDecls' x
else
declare! varDecls x
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
if (← read).unordered then
declare! polyDecls' p
else
declare! polyDecls p
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
if (← read).unordered then
declare! exprDecls' e
else
declare! exprDecls e
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
declare! ringPolyDecls p
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
declare! ringExprDecls e
private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
private def toContextExprCore (vars : Array Expr) (type : Expr) : MetaM Expr :=
if h : 0 < vars.size then
RArray.toExpr type id (RArray.ofFn (vars[·]) h)
else
RArray.toExpr type id (RArray.leaf (mkIntLit 0))
private def toContextExpr : GoalM Expr := do
toContextExprCore (← getVars) Int.mkType
private def mkContext
(ctxVar : Expr) (vars : PArray Expr) (varDecls : Std.HashMap Var Expr) (polyDecls : Std.HashMap Poly Expr) (exprDecls : Std.HashMap Int.Linear.Expr Expr)
(h : Expr) : GoalM Expr := do
let usedVars := collectMapVars varDecls collectVar >> collectMapVars polyDecls (·.collectVars) >> collectMapVars exprDecls (·.collectVars) <| {}
let vars' := usedVars.toArray
let varRename := mkVarRename vars'
let vars := vars'.map fun x => vars[x]!
let varFVars := vars'.map fun x => varDecls[x]?.getD default
let varIdsAsExpr := List.range vars'.size |>.toArray |>.map toExpr
let h := h.replaceFVars varFVars varIdsAsExpr
let h := mkLetOfMap exprDecls h `e (mkConst ``Int.Linear.Expr) fun e => toExpr <| e.renameVars varRename
let h := mkLetOfMap polyDecls h `p (mkConst ``Int.Linear.Poly) fun p => toExpr <| p.renameVars varRename
let h := h.abstract #[ctxVar]
if h.hasLooseBVars then
let ctxType := mkApp (mkConst ``RArray [levelZero]) Int.mkType
let ctxVal ← toContextExprCore vars Int.mkType
return .letE `ctx ctxType ctxVal h (nondep := false)
else
return h
private def toContextExpr' : GoalM Expr := do
toContextExprCore (← get').vars' Int.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 def mkRingContext (h : Expr) : ProofM Expr := do
unless (← get').usedCommRing do return h
let some ringId ← getIntRingId? | return h
let vars ← CommRing.RingM.run ringId do return (← CommRing.getRing).vars
let usedVars := collectMapVars (← get).ringPolyDecls (·.collectVars) >> collectMapVars (← get).ringExprDecls (·.collectVars) <| {}
let vars' := usedVars.toArray
let varRename := mkVarRename vars'
let vars := vars'.map fun x => vars[x]!
let h := mkLetOfMap (← get).ringExprDecls h `re (mkConst ``Grind.CommRing.Expr) fun e => toExpr <| e.renameVars varRename
let h := mkLetOfMap (← get).ringPolyDecls h `rp (mkConst ``Grind.CommRing.Poly) fun p => toExpr <| p.renameVars varRename
let h := h.abstract #[(← read).ringCtx]
if h.hasLooseBVars then
let ctxType := mkApp (mkConst ``RArray [levelZero]) Int.mkType
let ctxVal ← toContextExprCore vars Int.mkType
return .letE `rctx ctxType ctxVal h (nondep := false)
else
return h
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
go { ctx, ctx', ringCtx } |>.run' {}
let ctx := mkFVar (← mkFreshFVarId)
let ctx' := mkFVar (← mkFreshFVarId)
let ringCtx := mkFVar (← mkFreshFVarId)
go { ctx, ctx', ringCtx } |>.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).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 ] h
let h ← mkRingContext h
let h ← mkContext (← read).ctx' (← get').vars' (← get).varDecls' (← get).polyDecls' (← get).exprDecls' h
let h ← mkContext (← read).ctx (← get').vars (← get).varDecls (← get).polyDecls (← get).exprDecls h
trace[Meta.debug] "{h}"
return h
/--
Returns a Lean expression representing the auxiliary `CommRing` variable context needed for normalizing
@ -155,9 +226,9 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
return mkApp6 (mkConst ``Int.Linear.eq_norm_expr) (← getContext) (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) eagerReflBoolTrue h
| .defn e p =>
let some x := (← getVarMap).find? { expr := e } | throwError "`grind` internal error, missing cutsat variable{indentExpr e}"
return mkApp6 (mkConst ``Int.Linear.eq_def) (← getContext) (toExpr x) (← mkPolyDecl p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkEqRefl e)
return mkApp6 (mkConst ``Int.Linear.eq_def) (← getContext) (← mkVarDecl x) (← mkPolyDecl p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkEqRefl e)
| .defnNat h x e =>
return mkApp6 (mkConst ``Int.Linear.eq_def') (← getContext) (toExpr x) (← mkExprDecl e) (← mkPolyDecl c'.p) eagerReflBoolTrue h
return mkApp6 (mkConst ``Int.Linear.eq_def') (← getContext) (← mkVarDecl x) (← mkExprDecl e) (← mkPolyDecl c'.p) eagerReflBoolTrue h
| .norm c =>
return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← c.toExprProof)
| .divCoeffs c =>
@ -181,11 +252,11 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) eagerReflBoolTrue
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)
(← mkVarDecl x) (← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p)
eagerReflBoolTrue (← mkEqRefl e) h
| .defnNatCommRing h₁ x e' p re rp p' =>
let h₂ := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) eagerReflBoolTrue
return mkApp9 (mkConst ``Int.Linear.eq_def'_norm) (← getContext) (toExpr x) (← mkExprDecl e')
return mkApp9 (mkConst ``Int.Linear.eq_def'_norm) (← getContext) (← mkVarDecl x) (← mkExprDecl e')
(← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p) eagerReflBoolTrue h₁ h₂
partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
@ -218,11 +289,11 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
| .ofEq x c =>
return mkApp7 (mkConst ``Int.Linear.dvd_of_eq)
(← getContext) (toExpr x) (← mkPolyDecl c.p) (toExpr c'.d) (← mkPolyDecl c'.p)
(← getContext) (← mkVarDecl x) (← mkPolyDecl c.p) (toExpr c'.d) (← mkPolyDecl c'.p)
eagerReflBoolTrue (← c.toExprProof)
| .subst x c₁ c₂ =>
return mkApp10 (mkConst ``Int.Linear.eq_dvd_subst)
(← getContext) (toExpr x) (← mkPolyDecl c₁.p) (toExpr c₂.d) (← mkPolyDecl c₂.p) (toExpr c'.d) (← mkPolyDecl c'.p)
(← getContext) (← mkVarDecl x) (← mkPolyDecl c₁.p) (toExpr c₂.d) (← mkPolyDecl c₂.p) (toExpr c'.d) (← mkPolyDecl c'.p)
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
| .cooper₁ s =>
let { c₁, c₂, c₃?, left } := s.pred
@ -291,7 +362,7 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
else
mkConst ``Int.Linear.eq_le_subst_nonpos
return mkApp8 thm
(← getContext) (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
(← getContext) (← mkVarDecl x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
eagerReflBoolTrue
(← c₁.toExprProof) (← c₂.toExprProof)
| .ofLeDiseq c₁ c₂ =>
@ -350,7 +421,7 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
return mkApp5 (mkConst ``Int.Linear.diseq_neg) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← c.toExprProof)
| .subst x c₁ c₂ =>
return mkApp8 (mkConst ``Int.Linear.eq_diseq_subst)
(← getContext) (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
(← getContext) (← mkVarDecl x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
| .reorder c => withUnordered <| c.toExprProof
| .commRingNorm c e p =>

42
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.lean Normal file
View file

@ -0,0 +1,42 @@
/-
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
-/
module
prelude
public import Init.Data.Int.Linear
public import Lean.Meta.Tactic.Grind.Arith.VarRename
namespace Int.Linear
open Lean.Meta.Grind.Arith
public def Poly.renameVars (p : Poly) (f : VarRename) : Poly :=
match p with
| .num .. => p
| .add k x p => .add k (f x) (renameVars p f)
public def Expr.renameVars (e : Expr) (f : VarRename) : Expr :=
match e with
| .num .. => e
| .var x => .var (f x)
| .neg a => .neg (renameVars a f)
| .add a b => .add (renameVars a f) (renameVars b f)
| .sub a b => .sub (renameVars a f) (renameVars b f)
| .mulL k a => .mulL k (renameVars a f)
| .mulR a k => .mulR (renameVars a f) k
public def Poly.collectVars (p : Poly) : VarCollector :=
match p with
| .num .. => id
| .add _ x p => collectVar x >> p.collectVars
public def Expr.collectVars (e : Expr) : VarCollector :=
match e with
| .num .. => id
| .var x => collectVar x
| .neg a | .mulL _ a | .mulR a _ => a.collectVars
| .add a b | .sub a b => a.collectVars >> b.collectVars
end Int.Linear

8
src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean
View file

@ -115,10 +115,10 @@ private abbrev withProofContext (x : ProofM Expr) : LinearM Expr := do
where
go : ProofM Expr := do
let h ← x
let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr
let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr
let h ← mkLetOfMap (← get).ringPolyMap h `rp (mkConst ``Grind.CommRing.Poly) toExpr
let h ← mkLetOfMap (← get).ringExprMap h `re (mkConst ``Grind.CommRing.Expr) toExpr
let h := mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr
let h := mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr
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), (← getRingContext)] h
/--

2
src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
View file

@ -13,7 +13,7 @@ public section
namespace Lean.Meta.Grind.Arith
def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr)
(varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr := do
(varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : Expr := Id.run do
if m.isEmpty then
return e
else

48
src/Lean/Meta/Tactic/Grind/Arith/VarRename.lean Normal file
View file

@ -0,0 +1,48 @@
/-
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
-/
module
prelude
public import Init.Prelude
public import Init.Data.Array.QSort
public import Std.Data.HashSet
public section
namespace Lean.Meta.Grind.Arith
abbrev Var : Type := Nat
abbrev FoundVars := Std.HashSet Nat
abbrev VarCollector := FoundVars → FoundVars
def collectVar (x : Var) : VarCollector := (·.insert x)
instance : AndThen VarCollector where
andThen c₁ c₂ := fun s => c₂ () (c₁ s)
def collectMapVars {_ : BEq α} {_ : Hashable α} (m : Std.HashMap α Expr) (k : α → VarCollector) : VarCollector := fun s => Id.run do
let mut s := s
for (a, _) in m do
s := k a s
return s
def FoundVars.toArray (s : FoundVars) : Array Var :=
Std.HashSet.toArray s |>.qsort
structure VarRename where
map : Std.HashMap Var Var
instance : CoeFun VarRename (fun _ => Var → Var) where
coe := fun s x => s.map[x]?.getD 0
def mkVarRename (new2old : Array Var) : VarRename := Id.run do
let mut old2new : Std.HashMap Var Var := {}
let mut new := 0
for old in new2old do
old2new := old2new.insert old new
new := new + 1
{ map := old2new }
end Lean.Meta.Grind.Arith

14
tests/lean/run/grind_cutsat_trim_context.lean Normal file
View file

@ -0,0 +1,14 @@
/--
trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
let ctx := RArray.leaf (f 2);
let p_1 := Poly.add 1 0 (Poly.num 0);
let p_2 := Poly.add (-1) 0 (Poly.num 1);
let p_3 := Poly.num 1;
le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1)
-/
#guard_msgs in -- `cutsat` context should contain only `f 2`
open Lean Int Linear in
set_option trace.grind.debug.proof true in
example (f : Nat → Int) :
f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 → f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
grind