This PR adds the shared infrastructure for arithmetic normalization in
`Sym.Arith/`,
laying the groundwork for both `Sym.simp`'s arith pre-simproc and the
eventual
unification of grind's `CommRing` module.
The key components:
- **`Types.lean`**: Classification structures (`Semiring`, `Ring`,
`CommRing`,
`CommSemiring`) stored in a `SymExtension`. These are the
classification-only
subset of grind's ring types — no solver state. Includes
`withExpThreshold` for
controlling exponent evaluation limits.
- **`EvalNum.lean`**: `evalNat?`/`evalInt?` for evaluating ground
Nat/Int
expressions in type classes (e.g., `IsCharP`), adapted from grind to
`SymM`.
- **`Classify.lean`**: Algebraic structure detection (CommRing > Ring >
CommSemiring > Semiring) with a single `typeClassify : PHashMap ExprPtr
ClassifyResult` cache.
Detects `IsCharP`, `NoNatZeroDivisors`, and `Field` instances.
- **Type classes**: `MonadCanon`, `MonadRing`/`MonadCommRing`,
`MonadSemiring`/`MonadCommSemiring`, `MonadGetVar`/`MonadMkVar` —
abstract over
the monad so the same code works in both `SymM` and grind's
`RingM`/`SemiringM`.
Grind's `MonadCanon` is deleted; grind's monads inherit it from `SymM`
via
`MonadLift`.
- **`Functions.lean`**: Cached function getters (`getAddFn`, `getMulFn`,
etc.)
generic over the type classes. Synthesizes instances, validates via
`isDefEqI`,
canonicalizes via `canonExpr`.
- **`Reify.lean`**: Converts Lean expressions into
`RingExpr`/`SemiringExpr` for
reflection-based normalization. Variable creation abstracted via
`MonadMkVar`.
- **`DenoteExpr.lean`**: Converts reified expressions back to Lean
`Expr`s.
Roundtrip tests confirm reify→denote produces definitionally equal
results.
- **`ToExpr.lean`**, **`VarRename.lean`**, **`Poly.lean`**: Moved from
`Grind.Arith.CommRing/` — pure utilities on `Grind.CommRing` types with
no
solver dependencies.
- **Tests**: Unit tests for classification (`Int` → commRing, `Nat` →
commSemiring,
`Rat` → commRing), `evalNat?`/`evalInt?`, exp threshold, and
reify-denote roundtrips.
**TODO**: use abstractions to implement `grind` ring module, and delete
code duplication.
---------
Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
