From 097952c48fcfae853cdffff8d0e784b68d6d069b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 17 Jul 2025 13:53:48 +0200
Subject: [PATCH] perf: simp subexpr benchmark (#9404)

This PR adds a simp benchmark to our suite, specifically targeting
caching of subexpression
rewriting results.
---
 tests/bench/simp_subexpr.lean            | 41 ++++++++++++++++++++++++
 tests/bench/speedcenter.exec.velcom.yaml |  6 ++++
 2 files changed, 47 insertions(+)
 create mode 100644 tests/bench/simp_subexpr.lean

diff --git a/tests/bench/simp_subexpr.lean b/tests/bench/simp_subexpr.lean
new file mode 100644
index 0000000000..5d8a179179
--- /dev/null
+++ b/tests/bench/simp_subexpr.lean
@@ -0,0 +1,41 @@
+/-!
+A micro-benchmark based on `simp_bubblesort`, designed specifically to use the subexpression
+cache for rewriting in `simp`.
+-/
+
+inductive V where | a | b
+open V
+
+axiom L : Type
+axiom N : Type
+axiom z : N
+axiom s : N → N
+axiom nil : L
+axiom f : V → L → L
+axiom iter : N → (L → L) → (L → L)
+axiom combine : L → L → L
+
+axiom swap : f b (f a xs) = f a (f b xs)
+axiom iter_zero : iter z g x = g x
+axiom iter_succ : iter (s i) g x = iter i g (iter i g x)
+
+noncomputable def steps : N := s (s (s (s (s (s (s z))))))
+
+set_option maxRecDepth 100000
+set_option profiler true
+
+syntax "tree(" num "," term "," term ")" : term
+
+macro_rules
+  | `(tree($n, $l, $r)) =>
+    match n.getNat with
+    | 0 => `(combine $l $r)
+    | n + 1 => `(combine tree($(Lean.quote n), $l, $r) tree($(Lean.quote n), $r, $l))
+
+
+-- If run with -memoize or caching fails otherwise this regresses to timeout
+
+theorem normalized:
+  tree(0, (iter steps (f a) (iter steps (f b) nil)), (iter steps (f b) (iter steps (f a) nil))) =
+  tree(0, (iter steps (f b) (iter steps (f a) nil)), (iter steps (f a) (iter steps (f b) nil))) :=
+by simp (maxSteps := 1000000) only [swap, iter_zero, iter_succ, steps]
diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml
index 42396a3adb..599be10fd8 100644
--- a/tests/bench/speedcenter.exec.velcom.yaml
+++ b/tests/bench/speedcenter.exec.velcom.yaml
@@ -413,6 +413,12 @@
   run_config:
     <<: *time
     cmd: lean simp_local.lean
+- attributes:
+    description: simp_subexpr
+    tags: [fast, suite]
+  run_config:
+    <<: *time
+    cmd: lean simp_subexpr.lean
 - attributes:
     description: nat_repr
     tags: [fast, suite]