19.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 undex coqtop -opt because the compiled ML files used by the tactic are not linked in this binary image, and dynamic loading of native code is not possible in Objective Caml.
Two structures are pre-loaded: the semi-ring of naturals and the ring of integers.
Then, to normalize the terms term1, ..., termn in the current subgoal, use the command :
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. The latter case has to be preferred because the normal is unique only for a given variables map. In the first case, it is possible for a common subterm t of term1 and term2 to have the variable number 1 in term1 and 3 in term2, and then the normalization has no utility.
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 refl_equal to reduce x + y = x + z to y = z and x * z = x * y to y = z.
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