From a228380626987c8d6737dc004ffa747ba45036b9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Apr 2025 21:49:35 -0700 Subject: [PATCH] fix: `shareCommon` issues in `grind` (#7834) This PR fixes some of the `shareCommon` issues in `grind`. --- src/Lean/Meta/Tactic/Grind.lean | 1 + src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean | 1 + .../Tactic/Grind/Arith/Cutsat/DvdCnstr.lean | 2 +- .../Tactic/Grind/Arith/Cutsat/EqCnstr.lean | 8 +++--- .../Tactic/Grind/Arith/Cutsat/Foreign.lean | 3 +++ .../Tactic/Grind/Arith/Cutsat/LeCnstr.lean | 4 +-- .../Meta/Tactic/Grind/Arith/Cutsat/Nat.lean | 25 +++++++++++-------- .../Meta/Tactic/Grind/Arith/Cutsat/Norm.lean | 2 +- .../Meta/Tactic/Grind/Arith/Cutsat/Var.lean | 1 + src/Lean/Meta/Tactic/Grind/Simp.lean | 2 ++ 10 files changed, 30 insertions(+), 19 deletions(-) diff --git a/src/Lean/Meta/Tactic/Grind.lean b/src/Lean/Meta/Tactic/Grind.lean index 1b8f84b683..a6d1d7d34c 100644 --- a/src/Lean/Meta/Tactic/Grind.lean +++ b/src/Lean/Meta/Tactic/Grind.lean @@ -73,5 +73,6 @@ builtin_initialize registerTraceClass `grind.debug.matchCond.proveFalse builtin_initialize registerTraceClass `grind.debug.mbtc builtin_initialize registerTraceClass `grind.debug.ematch builtin_initialize registerTraceClass `grind.debug.proveEq +builtin_initialize registerTraceClass `grind.debug.pushNewFact end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean index 8d9a7cfd0a..c8e7f15b64 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean @@ -66,5 +66,6 @@ builtin_initialize registerTraceClass `grind.debug.cutsat.nat builtin_initialize registerTraceClass `grind.debug.cutsat.proof builtin_initialize registerTraceClass `grind.debug.cutsat.internalize builtin_initialize registerTraceClass `grind.debug.cutsat.markTerm +builtin_initialize registerTraceClass `grind.debug.cutsat.natCast end Lean diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean index f122f77274..34235fca5c 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean @@ -106,7 +106,7 @@ def propagateNatDvd (e : Expr) : GoalM Unit := do let some (d, b) ← Int.OfNat.toIntDvd? e | return () let gen ← getGeneration e let ctx ← getForeignVars .nat - let b' ← toLinearExpr (b.denoteAsIntExpr ctx) gen + let b' ← toLinearExpr (← b.denoteAsIntExpr ctx) gen let p := b'.norm if (← isEqTrue e) then let c := { d, p, h := .coreNat e d b b' : DvdCnstr } diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean index a131b8326e..5d54ee5263 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean @@ -243,8 +243,8 @@ private def processNewNatEq (a b : Expr) : GoalM Unit := do let (lhs, rhs) ← Int.OfNat.toIntEq a b let gen ← getGeneration a let ctx ← getForeignVars .nat - let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen - let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen + let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen + let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen 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}" @@ -290,8 +290,8 @@ private def processNewNatDiseq (a b : Expr) : GoalM Unit := do let (lhs, rhs) ← Int.OfNat.toIntEq a b let gen ← getGeneration a let ctx ← getForeignVars .nat - let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen - let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen + let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen + 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 } trace[grind.debug.cutsat.nat] "{← c.pp}" diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.lean index 57707b8635..71487ccc46 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Foreign.lean @@ -31,6 +31,9 @@ def mkForeignVar (e : Expr) (t : ForeignType) : GoalM Var := do def foreignTerm? (e : Expr) : GoalM (Option ForeignType) := do return (·.2) <$> (← get').foreignVarMap.find? { expr := e } +def hasForeignVar (e : Expr) : GoalM Bool := + return (← get').foreignVarMap.contains { expr := e } + def foreignTermOrLit? (e : Expr) : GoalM (Option ForeignType) := do if isNatNum e then return some .nat foreignTerm? e diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean index d14efe9a45..01fd1a9c62 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean @@ -152,8 +152,8 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do let some (lhs, rhs) ← Int.OfNat.toIntLe? e | return () let gen ← getGeneration e let ctx ← getForeignVars .nat - let lhs' ← toLinearExpr (lhs.denoteAsIntExpr ctx) gen - let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen + let lhs' ← toLinearExpr (← lhs.denoteAsIntExpr ctx) gen + let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen let p := lhs'.sub rhs' |>.norm trace[grind.debug.cutsat.nat] "{← p.pp}" let c ← if eqTrue then diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean index dc74e158ab..1fc9c74578 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Nat.lean @@ -27,20 +27,23 @@ instance : ToExpr OfNat.Expr where toExpr a := OfNat.toExpr a toTypeExpr := mkConst ``OfNat.Expr -def Expr.denoteAsIntExpr (ctx : PArray Lean.Expr) (e : Expr) : Lean.Expr := - match e with - | .num v => mkIntLit v - | .var i => mkIntNatCast ctx[i]! - | .add a b => mkIntAdd (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b) - | .mul a b => mkIntMul (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b) - | .div a b => mkIntDiv (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b) - | .mod a b => mkIntMod (denoteAsIntExpr ctx a) (denoteAsIntExpr ctx b) - open Lean.Meta.Grind open Lean.Meta.Grind.Arith.Cutsat open Meta +def Expr.denoteAsIntExpr (ctx : PArray Lean.Expr) (e : Expr) : GoalM Lean.Expr := + shareCommon (go e) +where + go (e : Expr) : Lean.Expr := + match e with + | .num v => mkIntLit v + | .var i => mkIntNatCast ctx[i]! + | .add a b => mkIntAdd (go a) (go b) + | .mul a b => mkIntMul (go a) (go b) + | .div a b => mkIntDiv (go a) (go b) + | .mod a b => mkIntMod (go a) (go b) + partial def toOfNatExpr (e : Lean.Expr) : GoalM Expr := do let mkVar (e : Lean.Expr) : GoalM Expr := do let x ← mkForeignVar e .nat @@ -125,13 +128,13 @@ namespace Lean.Meta.Grind.Arith.Cutsat If `e` is of the form `a.denoteAsInt ctx` for some `a` and `ctx`, assert that `e` is nonnegative. -/ -def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := do +def assertDenoteAsIntNonneg (e : Expr) : GoalM Unit := withIncRecDepth do if e.isAppOf ``NatCast.natCast then return () let some rhs ← Int.OfNat.ofDenoteAsIntExpr? e |>.run | return () let gen ← getGeneration e let ctx ← getForeignVars .nat let lhs' : Int.Linear.Expr := .num 0 - let rhs' ← toLinearExpr (rhs.denoteAsIntExpr ctx) gen + let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen let p := lhs'.sub rhs' |>.norm trace[grind.debug.cutsat.nat] "{← p.pp}" let c := { p, h := .denoteAsIntNonneg rhs rhs' : LeCnstr } diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean index 870d05505d..2a6e5ca614 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Norm.lean @@ -16,10 +16,10 @@ and these expressions must be normalized inside of the cutsat module. /-- Converts the given integer expression into `Int.Linear.Expr` -/ partial def toLinearExpr (e : Expr) (generation : Nat := 0) : GoalM Int.Linear.Expr := do let toVar (e : Expr) := do + let e ← shareCommon e if (← alreadyInternalized e) then return .var (← mkVar e) else - let e ← shareCommon e internalize e generation return .var (← mkVar e) let mul (a b : Expr) := do diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean index bf6435efc7..2cb5874399 100644 --- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean +++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean @@ -14,6 +14,7 @@ namespace Lean.Meta.Grind.Arith.Cutsat private def assertNatCast (e : Expr) : GoalM Unit := do let_expr NatCast.natCast _ inst a := e | return () let_expr instNatCastInt := inst | return () + trace[grind.debug.cutsat.natCast] "{a}" pushNewFact <| mkApp (mkConst ``Int.Linear.natCast_nonneg) a discard <| mkForeignVar a .nat diff --git a/src/Lean/Meta/Tactic/Grind/Simp.lean b/src/Lean/Meta/Tactic/Grind/Simp.lean index e52e85526a..18b3c387ec 100644 --- a/src/Lean/Meta/Tactic/Grind/Simp.lean +++ b/src/Lean/Meta/Tactic/Grind/Simp.lean @@ -53,12 +53,14 @@ def pushNewFact' (prop : Expr) (proof : Expr) (generation : Nat := 0) : GoalM Un mkApp4 (mkConst ``Eq.mp [levelZero]) prop prop' h proof else proof + trace[grind.debug.pushNewFact] "{prop} ==> {prop'}" modify fun s => { s with newFacts := s.newFacts.push <| .fact prop' proof generation } /-- Infers the type of the proof, preprocess it, and adds it to todo list. -/ def pushNewFact (proof : Expr) (generation : Nat := 0) : GoalM Unit := do let prop ← inferType proof + trace[grind.debug.pushNewFact] "{prop}" pushNewFact' prop proof generation end Lean.Meta.Grind