Module ring 

Ring Tactic: Polynomial Equality by Normalization

This module implements the ring decision procedure, which proves polynomial equalities by converting terms to canonical polynomial form and comparing them.

Algorithm

The ring tactic works in three steps:

1. Reification: Convert Syntax terms to internal polynomial representation
2. Normalization: Expand and combine like terms into canonical form
3. Comparison: Check if normalized forms are structurally equal

Supported Operations

• Addition (add)
• Subtraction (sub)
• Multiplication (mul)

Division and modulo are not polynomial operations and are rejected.

Canonical Form

Polynomials are stored as a map from monomials to coefficients. Monomials are maps from variable indices to exponents. BTreeMap ensures deterministic ordering for canonical comparison.

Exactness

Coefficients and exponents are arbitrary-precision (BigInt): the verdict feeds trusted reflection reductions, so the arithmetic must be exact at every magnitude — a wrapped coefficient or exponent would equate unequal polynomials.

Structs

Monomial

A monomial is a product of variables with their powers.

Polynomial

A polynomial is a sum of monomials with integer coefficients.

Enums

ReifyError

Error during reification of a term to polynomial form.

Functions

reify

Reify a Syntax term into a polynomial representation.