20.4 Concrete usage in Coq
Under a session launched by coqtop or coqtop -full,
load the Ring files with the command:
Require Ring.
It does not work under coqtop -opt because the compiled ML
objects used by the tactic are not linked in this binary image, and
dynamic loading of native code is not possible in Objective Caml.
In order to use Ring on naturals, load ArithRing
instead; for binary integers, load the module ZArithRing.
Then, to normalize the terms term1, ..., termn in
the current subgoal, use the tactic:
Ring term1 ... termn
Then the tactic guesses the type of given terms, the ring theory to
use, the variables map, and replace each term with its normal form.
The variables map is common to all terms
Warning: Ring term1; Ring term2 is not equivalent to
Ring term1 term2. In the latter case the variables map
is shared between the two terms, and common subterm t of term1
and term2 will have the same associated variable number.
Error messages:
-
All terms must have the same type
- Don't know what to do with this goal
- No Declared Ring Theory for term.
Use Add [Semi] Ring to declare it
That happens when all terms have the same type term, but there is
no declared ring theory for this set. See below.
Variants:
-
Ring
That works if the current goal is an equality between two
polynomials. It will normalize both sides of the
equality, solve it if the normal forms are equal and in other cases
try to simplify the equality using congr_eqT and refl_equal
to reduce x + y = x + z to y = z and x * z = x * y to y = z.
Error message: This goal is not an equality