19.8 Discussion about the usage of reflexion
But efficieny is not the only motivation to use reflexion here. Ring also deals with constants, it rewrites for example the expression 34 + 2*x -x + 12 to the expected result x + 46. For the tactic ACDSimpl, the only constants were 0 and 1. So the expression 34 + 2*(x - 1) + 12 is interpreted as V0 Å V1 Ä (V2 Q 1) Å V3, with the variables mapping {V0 |¬ 34; V1 |¬ 2; V2 |¬ x; V3 |¬ 12 }. Then it is rewrited to 34 - x + 2*x + 12, very far from the expected result. Here rewriting is not sufficient : you have to do some kind of reduction (some kind of calculus, in other words) to achieve the normalization.So here in the case of Ring we implement using reflexion a tactic that would be much more complex and slow if we wrote it like a classical tactic.
Is it the ultimate way to write tactics ? The answer is : yes and no. Tactics Ring uses intensively the conversion rule of Cic, that is replaces proof by calculus the most as it is possible. It can be useful in all situations where a classical tactic generates huge proof terms. Formal calculus and Tautologies solver are such situations. But consider a tactic like Auto or Linar : it does many complex and unsafe calculations and generates a small proof term. Clearly, it would be useless to try to replace it by a reflexion tactic.
Another argument against the reflexion is that Coq, as a programming langage, has many nice features, but is very far from the speed and the expressive power of Objective Caml. Wait a minute ! With Coq it is possible to extact ML code from Cicterms, right ? So, why not to link the extracted code with Coqto inherit the benefits of the reflexion and the speed of ML tactics ? That is called total reflexion, and is still an active research subject. With these technologies it will become possible to bootstrap the type-checker of Cic, but there is still a bit work to achieve that far goal.