feat: add interactive `simp` tactic for `sym =>` mode

This PR adds the `simp` tactic to the `sym =>` interactive mode, completing
the `Sym.simp` interactive infrastructure.

The `simp` tactic supports:
- `simp` — default (identity) variant
- `simp myVariant` — named variant registered via `register_sym_simp`
- `simp [thm₁, thm₂]` — default variant with extra rewrite theorems
- `simp myVariant [thm₁, thm₂]` — named variant with extra theorems

Extra theorems are composed into the variant's `post` chain via `>>`.

Per-variant persistent caching: each unique (variant name, extra theorem list)
combination gets its own `Sym.Simp.State` cache, shared across invocations
within a `sym =>` block. This avoids redundant simplification of identical
subterms when `simp` is called repeatedly (e.g., in branching proofs).

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>