The ring tactic
The ring tactic does associative-commutative rewriting in ring and semi-ring structures. It allows to check automatically equalities in a ring structure. Basically, the idea is to represent ring expressions by polynomials and to compare the normal forms of the polynomials. In a first version, normal forms were ordered sums of ordered products. Here we use the Sparse Horner form to represent normalized polynomials.This development is a joint work with Assia Mahboubi
Thanks to Bruno Barras for is brilliant contribution.
This development is now integrated in Coq