20.6 How does it work?

The code of Ring a good example of tactic written using reflection (or internalization, it is synonymous). What is reflection? Basically, it is writing Coq tactics in Coq, rather than in Objective Caml. From the philosophical point of view, it is using the ability of the Calculus of Constructions to speak and reason about itself. For the Ring tactic we used Coq as a programming language and also as a proof environment to build a tactic and to prove it correctness.

The interested reader is strongly advised to have a look at the file Ring_normalize.v. Here a type for polynomials is defined: 

Inductive Type polynomial := 
  Pvar : idx -> polynomial
| Pconst : A -> polynomial
| Pplus : polynomial -> polynomial -> polynomial
| Pmult : polynomial -> polynomial -> polynomial
| Popp : polynomial -> polynomial.

There is also a type to represent variables maps, and an interpretation function, that maps a variables map and a polynomial to an element of the concrete ring:

Definition polynomial_simplify := [...]
Definition interp : (varmap A) -> (polynomial A) -> A := [...]

A function to normalize polynomials is defined, and the big theorem is its correctness w.r.t interpretation, that is:

Theorem polynomial_simplify_correct : (v:(varmap A))(p:polynomial)
  (interp v (polynomial_simplify p))
  ==(interp v p).

(The actual code is slightly more complex: for efficiency, there is a special datatype to represent normalized polynomials, i.e. ``canonical sums''. But the idea is still the same).

So now, what is the scheme for a normalization proof? Let p be the polynomial expression that the user wants to normalize. First a little piece of ML code guesses the type of p, the ring theory T to use, an abstract polynomial ap and a variables map v such that p is bdi-equivalent to (interp v ap). Then we replace it by (interp v (polynomial_simplify ap)), using the main correctness theorem and we reduce it to a concrete expression p', which is the concrete normal form of p. This is summarized in this diagram:
p ®bdi (interp v ap)
    =(by the main correctness theorem)
p' ¬bdi (interp v (polynomial_simplify ap))

The user do not see the right part of the diagram. From outside, the tactic behaves like a bdi simplification extended with AC rewriting rules. Basically, the proof is only the application of the main correctness theorem to well-chosen arguments.