19.6 How does it work ?
The code of Ring a good example of tactic written using reflexion (or internalization, it is synonymous). What is reflexion ? Basically, it is writing Coq tactics in Coq, rather than in O'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 langage 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 Abstract_polynom.v. Here a type for polynoms is defined :
Variable A : Set. Variable C : (Ring_Constants A). Variable T : (Ring_Theory C). Inductive Set polynom := Pvar : idx -> polynom | Pconst : A -> polynom | Pplus : polynom -> polynom -> polynom | Pmult : polynom -> polynom -> polynom | Popp : polynom -> polynom.
There is also a type to represent variables maps, and an interpretation function, that maps a variables map and a polynom to an element of the concrete ring :
Definition polynom_simplify : polynom -> (spolynom A) := [...] Definition interp : varmap -> (polynnom A) -> A := [...]
A function to normalize polynoms is defined, and the big theorem is its correctness w.r.t interpretation, that is :
Theorem polynom_simplify_correct : (v:(varmap A))(p:polynom) (interp C v (polynom_simplify p)) = (interp C v p).
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 (A,C) to use, an abstract polynomial ap and a variables map v such that p is bdi-equivalent to
(interp A C v ap). Then we
replace it by (interp A C v (polynom\_simplify ap)), using the
main correctness theorem and we reduce it to a concrete expression
p', which is precisely the normalized form of
p. This is explained in this diagram:| p | ®bdi | (interp A C v ap) |
| =(by the main correctness theorem) | ||
| p' | ¬bdi | (interp A C v (polynom_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. So, basically the proof is only the application of the main correctness theorem to well-choosen arguments. We made a huge cut.