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"
/>
4c1e4a77b4