19.7 History of Ring
First Samuel Boutin designed the tactic ACDSimpl. This tactic did intensive use of rewriting. But the proofs terms generated by rewriting are big and the proof-checker of Coqexplodes on big examples of ACDSimpl, even on a fast workstation with a big amount of RAM. 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 copied in the proof term. So tactics that do hundreds of rewriting generate huge proof terms. Since ACDSimpl was too slow, Samuel Boutin rewrite it using reflexion. Later, the stuff was completely rewritten by Patrick Loiseleur: the new tactic does not any more require ACDSimpl to compile and it integrates the notion of constants. He also writes a few ML code for the Add Ring command, that allow to register new rings dynamically.
Poofs 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 certain time because it makes a large use of the conversion rule, but memory requirements are much smaller.