20.7 History of Ring

20.7 History of `Ring`

First Samuel Boutin designed the tactic ACDSimpl. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big for Coq's type-checker. Let us see why:

Coq < Goal (x,y,z:Z)`x + 3 + y + y*z = x + 3 + y + z*y`.
1 subgoal

  ============================
   (x,y,z:Z)`x+3+y+y*z = x+3+y+z*y`

Coq < Intros; Rewrite (Zmult_sym y z); Reflexivity.

Coq < Save toto.

Coq < Print toto.
toto =
[x,y,z:Z]
(eq_ind_r Z `z*y` [z0:Z]`x+3+y+z0 = x+3+y+z*y`
(refl_equal Z `x+3+y+z*y`) `y*z` (Zmult_sym y z))
: (x,y,z:Z)`x+3+y+y*z = x+3+y+z*y`

At each step of rewriting, the whole context is duplicated in the proof term. Then, a tactic that does hundreds of rewriting generates huge proof terms. Since ACDSimpl was too slow, Samuel Boutin rewrote it using reflection (see his article in TACS'97 [14]). Later, the stuff was rewritten by Patrick Loiseleur: the new tactic does not any more require ACDSimpl to compile and it makes use of bdi-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see 20.8). He also wrote a few ML code for the Add Ring command, that allow to register new rings dynamically.

Proofs terms generated by Ring are quite small, they are linear in the number of Å and Ä operations in the normalized terms. Type-checking those terms requires some time because it makes a large use of the conversion rule, but memory requirements are much smaller.