4c1e4a77b4
This PR adds a new benchmark `shallow_add_sub_cancel.lean` that demonstrates symbolic simulation using a shallow embedding into monadic `do` notation, as opposed to the deep embedding approach in `add_sub_cancel.lean`. The shallow embedding approach: - Uses Lean's `StateM` monad directly instead of a custom command language - Defines `Exec s k post` as a simple predicate: `post (k s).1 (k s).2` - Proves helper theorems for reasoning about monadic operations (`pure`, `bind`, `get`, `set`, `modify`, `ite`) - Programs are written in actual `do`-notation rather than a custom AST The benchmark solves goals using both the `MetaM` and `SymM` frameworks, showing that the shallow embedding integrates well with the symbolic simulation infrastructure. `SymM` is again way faster than `MetaM` ### Symbolic simulation benchmark — tactic time only Problem size `n` corresponds to a program with `4·n` monadic actions. | n | MetaM tactic (ms) | SymM tactic (ms) | Speedup | |-----|-------------------|------------------|---------| | 10 | 82.10 | 11.37 | ~7.2× | | 20 | 176.21 | 17.71 | ~9.9× | | 30 | 306.47 | 25.39 | ~12.1× | | 40 | 509.52 | 34.53 | ~14.7× | | 50 | 689.19 | 43.51 | ~15.8× | | 60 | 905.86 | 52.47 | ~17.3× | | 70 | 1172.31 | 62.50 | ~18.8× | | 80 | 1448.48 | 70.65 | ~20.5× | | 90 | 1787.15 | 80.89 | ~22.1× | | 100 | 2128.12 | 90.77 | ~23.5× | <img width="580" height="455" alt="image" src="https://github.com/user-attachments/assets/3511aaab-4d53-4520-8302-65d2d100df4a" /> |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||