From e8870da205af61d98edb0ae9a7fb73b050abd299 Mon Sep 17 00:00:00 2001 From: Sebastian Graf Date: Mon, 26 Jan 2026 18:58:33 +0100 Subject: [PATCH] chore: improve performance of mpure_intro and mvcgen by avoiding whnfD (#12165) New measurements: ``` goal_10: 181.910200 ms, kernel: 37.241050 ms goal_20: 386.540215 ms, kernel: 83.497428 ms goal_30: 648.282057 ms, kernel: 117.038447 ms goal_40: 946.733191 ms, kernel: 168.369124 ms goal_50: 1325.846873 ms, kernel: 223.838786 ms goal_60: 1734.175705 ms, kernel: 285.594486 ms goal_70: 2199.522317 ms, kernel: 351.659865 ms goal_80: 2700.077802 ms, kernel: 428.303337 ms goal_90: 3260.446641 ms, kernel: 515.976499 ms goal_100: 3865.503733 ms, kernel: 600.229962 ms ``` Previously, goal_100 took 7.8s. --- src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean | 35 ++++++++++--------- tests/bench/mvcgen/add_sub_cancel_StateM.lean | 26 +++++++------- tests/lean/run/mvcgenTutorial.lean | 2 ++ 3 files changed, 33 insertions(+), 30 deletions(-) diff --git a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean index 86102ef498..dd0d7f5933 100644 --- a/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean +++ b/src/Lean/Elab/Tactic/Do/ProofMode/Pure.lean @@ -82,13 +82,27 @@ def elabMPureIntro : Tactic replaceMainGoal [mv] | _ => throwUnsupportedSyntax +private def extractPureProp (e : Expr) : MetaM (Option Expr) := do + let e ← instantiateMVarsIfMVarApp e + let some (_, e) := e.app2? ``ULift.down | return none + let f := e.getAppFn + unless f.isConstOf ``SPred.pure do return none + let args := e.getAppArgs + if args.size < 2 then return none + let σs := args[0]! + let n ← TypeList.length σs + unless n = args.size - 2 do return none + let p := args[1]! + return p + partial def _root_.Lean.MVarId.applyRflAndAndIntro (mvar : MVarId) : MetaM Unit := do - -- The target might look like `(⌜?n = nₛ ∧ ?m = b⌝ s).down`, which we reduce to - -- `?n = nₛ ∧ ?m = b` by `whnfD`. + -- The target might look like `(⌜nₛ = ?n ∧ ?m = b⌝ s).down`, which we reduce to + -- `nₛ = ?n ∧ ?m = b` with `extractPureProp`. -- (Recall that `⌜s = 4⌝ s` is `SPred.pure (σs:=[Nat]) (s = 4) s` and `SPred.pure` is -- semi-reducible.) - let ty ← whnfD (← mvar.getType) - trace[Elab.Tactic.Do.spec] "whnf: {ty}" + let ty ← mvar.getType >>= instantiateMVarsIfMVarApp + let ty ← (·.getD ty) <$> extractPureProp ty + trace[Elab.Tactic.Do.spec] "pure Prop: {ty}" if ty.isAppOf ``True then mvar.assign (mkConst ``True.intro) else if let some (lhs, rhs) := ty.app2? ``And then @@ -127,16 +141,3 @@ def MGoal.pureTrivial (goal : MGoal) : OptionT MetaM Expr := do return ((), m) return prf catch _ => failure - -/- -def MGoal.pureRfl (goal : MGoal) : OptionT MetaM Expr := do - let mv ← mkFreshExprMVar goal.toExpr - let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); rfl)) catch _ => failure - | failure - return mv -def MGoal.pureRfl (goal : MGoal) : OptionT MetaM Expr := do - let mv ← mkFreshExprMVar goal.toExpr - let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); rfl)) catch _ => failure - | failure - return mv --/ diff --git a/tests/bench/mvcgen/add_sub_cancel_StateM.lean b/tests/bench/mvcgen/add_sub_cancel_StateM.lean index bf5d9682d3..8bce8e9a4f 100644 --- a/tests/bench/mvcgen/add_sub_cancel_StateM.lean +++ b/tests/bench/mvcgen/add_sub_cancel_StateM.lean @@ -62,26 +62,26 @@ def solveUsingMeta (n : Nat) (check := true) : MetaM Unit := do let ([], _) ← runTactic mvarId (← `(tactic| solve)).raw {} {} | throwError "FAILED!" def runBenchUsingMeta (sizes : List Nat) : MetaM Unit := do - IO.println "=== Symbolic Simulation Tests ===" + IO.println "=== VCGen tests ===" IO.println "" for n in sizes do solveUsingMeta n set_option maxRecDepth 10000 set_option maxHeartbeats 10000000 -/- -info: === Symbolic Simulation Tests === +/-- +info: === VCGen tests === -goal_10: 245.576221 ms, kernel: 134.134182 ms -goal_20: 613.945320 ms, kernel: 115.453811 ms -goal_30: 1074.053596 ms, kernel: 179.076070 ms -goal_40: 1680.678302 ms, kernel: 252.066677 ms -goal_50: 2457.209584 ms, kernel: 293.974096 ms -goal_60: 3271.773330 ms, kernel: 368.394386 ms -goal_70: 3981.247921 ms, kernel: 434.297822 ms -goal_80: 5077.300540 ms, kernel: 507.047772 ms -goal_90: 6486.990060 ms, kernel: 556.952095 ms -goal_100: 7791.399986 ms, kernel: 623.605163 ms +goal_10: 181.910200 ms, kernel: 37.241050 ms +goal_20: 386.540215 ms, kernel: 83.497428 ms +goal_30: 648.282057 ms, kernel: 117.038447 ms +goal_40: 946.733191 ms, kernel: 168.369124 ms +goal_50: 1325.846873 ms, kernel: 223.838786 ms +goal_60: 1734.175705 ms, kernel: 285.594486 ms +goal_70: 2199.522317 ms, kernel: 351.659865 ms +goal_80: 2700.077802 ms, kernel: 428.303337 ms +goal_90: 3260.446641 ms, kernel: 515.976499 ms +goal_100: 3865.503733 ms, kernel: 600.229962 ms -/ #guard_msgs in #eval runBenchUsingMeta [10, 20, 30, 40, 50, 60, 70, 80, 90, 100] diff --git a/tests/lean/run/mvcgenTutorial.lean b/tests/lean/run/mvcgenTutorial.lean index 4588f7665b..f34e46189a 100644 --- a/tests/lean/run/mvcgenTutorial.lean +++ b/tests/lean/run/mvcgenTutorial.lean @@ -128,6 +128,8 @@ theorem mkFresh_spec [Monad m] [WPMonad m ps] (c : Nat) : @[spec] theorem mkFreshN_spec (n : Nat) : ⦃⌜True⌝⦄ mkFreshN n ⦃⇓ r => ⌜r.Nodup⌝⦄ := by + -- This is a great test case for `applyRflAndAndIntro` because it requires + -- reducing `(⌜s₁.counter = ?c⌝ s).down` to `s₁ = ?c`. mvcgen [mkFreshN, liftCounterM] case inv1 => exact ⇓⟨xs, acc⟩ _ state => ⌜(∀ n ∈ acc, n < state.counter) ∧ acc.toList.Nodup⌝ all_goals mleave; grind