This PR prevents `Sym.simp` from looping on permutation theorems like
`∀ x y, x + y = y + x`.
- Add `perm : Bool` field to `Theorem`
- Add `isPerm` that checks if LHS and RHS have the same structure with
pattern variables (de Bruijn indices) rearranged via a consistent
bijection. Uses `ReaderT` (offset for binder entry), `StateT`
(forward/backward maps), `ExceptT` (failure).
- Compute `perm` in `mkTheoremFromDecl` / `mkTheoremFromExpr`
- In `Theorem.rewrite`, when `perm` is true, only apply the rewrite if
the result is strictly less than the input (using `acLt`)
- Tests include the classic AC normalization stress test with
`add_comm`, `add_assoc`, `add_left_comm`
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
This PR adds per-result `contextDependent` tracking to `Sym.Simp.Result`
and splits the simplifier cache into persistent (context-independent)
and transient (context-dependent, cleared on binder entry). This
replaces the coarse `wellBehavedMethods` flag.
Key changes:
- Add `contextDependent : Bool := false` to `Result.rfl` and
`Result.step`
- Split `State.cache` into `persistentCache` and `transientCache`
- Remove `wellBehavedMethods` from `Methods`
- Replace `withoutModifyingCacheIfNotWellBehaved` with
`withFreshTransientCache`
- Change `DischargeResult` to an inductive (`.failed`/`.solved`)
- Add `dischargeAssumption` (context-dependent discharger for testing)
- Add `sym.simp.debug.cache` trace class
- Propagate `contextDependent` through all combinators (congruence,
transitivity, control flow, arrows, rewriting)
- Add `mkRflResult`/`mkRflResultCD` to avoid dynamic allocation of rfl
results
- Fix `isRfl` to ignore `contextDependent` (was silently broken by the
extra field)
Propagation invariant: when combining sub-results, `cd` is the
disjunction of ALL sub-results' flags — including `.rfl` results. If
`simp` returned `.rfl (contextDependent := true)`, it means `simp` might
take a completely different code path in another local context, so all
downstream results must be marked context-dependent.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
