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:
  1. All terms must have the same type
  2. Don't know what to do with this goal
  3. 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:
  1. 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