— The Rocqshop 2026 —

In an attempt to study how the Rocq prover can help teaching mathematics, we propose to exploit the ring and field tactics extensively to let students justify elementary steps in calculational proofs. These tactics manipulate formulas where they recognize a restricted set of operations and handle every value involving other functions as variables. As a result, they only work at the surface of formulas and their behavior can be puzzling, especially for beginners.
We designed an extension where arguments of non-ring or non-field functions are simplified progressively. We will show how this extension makes declarative proof scripts closer to usual mathematical text.
This extension is based on companion tactics, ring_simplify and field_simplify. It appears that field_simplify only performs half the simplification we expect. To improve on this, we propose implementing an extension where an external program is called to compute greatest common divisors of polynomials as an oracle and the result is checked in a traditional manner.
This talk should interest any user of the Rocq prover interested in developing their own tactics combining some amount of reflexive computation, some amount of external untrusted computation, and some amount of meta-programming, in this case using Ltac and Rocq-Elpi.
This is joint work with Thomas Portet, with contributions by Davide Fissore, Laurent Théry, and Enrico Tassi.