A tactic for canceling numeric denominators #
This file defines tactics that cancel numeric denominators from field expressions.
As an example, we want to transform a comparison
5*(a/3 + b/4) < c/3 into the equivalent
5*(4*a + 3*b) < 4*c.
Implementation notes #
The tooling here was originally written for
linarith, not intended as an interactive tactic.
The interactive version has been split off because it is sometimes convenient to use on its own.
There are likely some rough edges to it.
Improving this tactic would be a good project for someone interested in learning tactic programming.