From bba35e45320f8fa52247178418ae3bf2b0929d67 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 29 Dec 2025 18:42:04 -0800 Subject: [PATCH] perf: add performance comparison tests for `SymM` vs `MetaM` (#11838) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds performance comparison tests between the new `SymM` monad and the standard `MetaM` for `intros`/`apply` operations. The tests solve problems of the form: ```lean let z := 0; ∀ x, ∃ y, x = z + y ∧ let z := z + x; ∀ x, ∃ y, x = z + y ∧ ... ∧ True ``` using repeated `intros` and `apply` with `Exists.intro`, `And.intro`, `Eq.refl`, and `True.intro`. **Results show 10-20x speedup:** | Size | MetaM | SymM | Speedup | |------|-------|------|---------| | 1000 | 226ms | 21ms | 10.8x | | 2000 | 582ms | 44ms | 13.2x | | 3000 | 1.08s | 72ms | 15.0x | | 4000 | 1.72s | 101ms | 17.0x | | 5000 | 2.49s | 125ms | 19.9x | | 6000 | 3.45s | 157ms | 22.0x | --- tests/lean/sym/perf_meta_apply.lean | 78 +++++++++++++++++++++++++++ tests/lean/sym/perf_sym_apply.lean | 83 +++++++++++++++++++++++++++++ 2 files changed, 161 insertions(+) create mode 100644 tests/lean/sym/perf_meta_apply.lean create mode 100644 tests/lean/sym/perf_sym_apply.lean diff --git a/tests/lean/sym/perf_meta_apply.lean b/tests/lean/sym/perf_meta_apply.lean new file mode 100644 index 0000000000..41c6b1f56a --- /dev/null +++ b/tests/lean/sym/perf_meta_apply.lean @@ -0,0 +1,78 @@ +import Lean.Meta.Tactic + +open Lean Meta +def profileM {α : Type} (k : MetaM α) (msg : String := "experiment") : MetaM α := + profileitM Exception msg ({ : Options }.setBool `profiler true |>.setNat `profiler.threshold 0) k + +def genTerm (n : Nat) : Expr := Id.run do + let mut e := mkConst ``True + let nat := mkConst ``Nat + for _ in 0...n do + let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1)) + e := mkApp2 (mkConst ``And) eq e + e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e) + e := mkForall `x .default nat e + e := mkLet `z nat (mkNatAdd (mkBVar 1) (mkBVar 0)) e + let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1)) + e := mkApp2 (mkConst ``And) eq e + e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e) + e := mkForall `x .default nat e + e := mkLet `z nat (mkNatLit 0) e + return e + +set_option maxRecDepth 10000000 + +def tryIntros? (goals : List MVarId) : MetaM (Option (List MVarId)) := do + let goal :: goals := goals | return none + let (fvars, goal') ← goal.intros + if fvars.isEmpty then return none + return some (goal' :: goals) + +def tryApply? (declName : Name) (goals : List MVarId) : MetaM (Option (List MVarId)) := do + let goal :: goals := goals | return none + try + let goals' ← goal.applyConst declName + return some (goals' ++ goals) + catch _ => + return none + +def tryApplyAny? (declNames : List Name) (goals : List MVarId) : MetaM (Option (List MVarId)) := do + match declNames with + | [] => return none + | declName :: declNames => + if let some goals' ← tryApply? declName goals then + return some goals' + else + tryApplyAny? declNames goals + +def solve (n : Nat) (type : Expr) : MetaM Unit := profileM (msg := s!"size {n}") do + let mvarId := (← mkFreshExprMVar type).mvarId! + discard <| go 10000000 [mvarId] + return () +where + go (fuel : Nat) (goals : List MVarId) : MetaM Bool := do + let fuel + 1 := fuel | throwError "out of fuel" + let goal :: goals' := goals | return true + if (← goal.isAssigned) then + go fuel goals' + else + if let some goals' ← tryIntros? goals then + go fuel goals' + else if let some goals' ← tryApplyAny? [``Exists.intro, ``And.intro, ``Eq.refl, ``True.intro] goals then + go fuel goals' + else + throwError "Stuck at {goal}" + +def test (n : Nat) : MetaM Unit := do + let e := genTerm n + solve n e + +-- We are solving problems of the following form +#eval logInfo (genTerm 2) + +#eval test 1000 +#eval test 2000 +#eval test 3000 +#eval test 4000 +#eval test 5000 +#eval test 6000 diff --git a/tests/lean/sym/perf_sym_apply.lean b/tests/lean/sym/perf_sym_apply.lean new file mode 100644 index 0000000000..373b147a96 --- /dev/null +++ b/tests/lean/sym/perf_sym_apply.lean @@ -0,0 +1,83 @@ +import Lean.Meta.Tactic +import Lean.Meta.Sym + +open Lean Meta Sym +def profileM {α : Type} (k : MetaM α) (msg : String := "experiment") : MetaM α := + profileitM Exception msg ({ : Options }.setBool `profiler true |>.setNat `profiler.threshold 0) k + +def genTerm (n : Nat) : Expr := Id.run do + let mut e := mkConst ``True + let nat := mkConst ``Nat + for _ in 0...n do + let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1)) + e := mkApp2 (mkConst ``And) eq e + e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e) + e := mkForall `x .default nat e + e := mkLet `z nat (mkNatAdd (mkBVar 1) (mkBVar 0)) e + let eq := mkApp3 (mkConst ``Eq [1]) nat (mkBVar 0) (mkNatAdd (mkBVar 2) (mkBVar 1)) + e := mkApp2 (mkConst ``And) eq e + e := mkApp2 (mkConst ``Exists [1]) nat (mkLambda `y .default nat e) + e := mkForall `x .default nat e + e := mkLet `z nat (mkNatLit 0) e + return e + +set_option maxRecDepth 10000000 + +def tryIntros? (goals : List Goal) : SymM (Option (List Goal)) := do + try + let goal :: goals := goals | return none + let (_, goal') ← intros goal + return some (goal' :: goals) + catch _ => + return none + +def tryApply? (rule : BackwardRule) (goals : List Goal) : SymM (Option (List Goal)) := do + let goal :: goals := goals | return none + try + let goals' ← rule.apply goal + return some (goals' ++ goals) + catch _ => + return none + +def tryApplyAny? (rules : List BackwardRule) (goals : List Goal) : SymM (Option (List Goal)) := do + match rules with + | [] => return none + | rule :: rules => + if let some goals' ← tryApply? rule goals then + return some goals' + else + tryApplyAny? rules goals + +def solve (n : Nat) (type : Expr) : MetaM Unit := profileM (msg := s!"size {n}") <| SymM.run' do + let mvarId := (← mkFreshExprMVar type).mvarId! + let rules ← [``Exists.intro, ``And.intro, ``Eq.refl, ``True.intro].mapM fun declName => mkBackwardRuleFromDecl declName + let goal ← mkGoal mvarId + discard <| go 10000000 rules [goal] + return () +where + go (fuel : Nat) (rules : List BackwardRule) (goals : List Goal) : SymM Bool := do + let fuel + 1 := fuel | throwError "out of fuel" + let goal :: goals' := goals | return true + if (← goal.mvarId.isAssigned) then + go fuel rules goals' + else + if let some goals' ← tryIntros? goals then + go fuel rules goals' + else if let some goals' ← tryApplyAny? rules goals then + go fuel rules goals' + else + throwError "Stuck at {goal.mvarId}" + +def test (n : Nat) : MetaM Unit := do + let e := genTerm n + solve n e + +-- We are solving problems of the following form +#eval logInfo (genTerm 2) + +#eval test 1000 +#eval test 2000 +#eval test 3000 +#eval test 4000 +#eval test 5000 +#eval test 6000