20.8 Discussion
Efficiency is not the only motivation to use reflection
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 1) Å V3,
with the variables mapping
{V0 |® 34; V1 |® 2; V2 |® x; V3 |® 12 }. Then it is
rewritten 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 computation) to achieve the
normalization.
The tactic Ring is not only faster than a classical one:
using reflection, we get for free integration of computation and
reasoning that would be very complex to implement in the classic fashion.
Is it the ultimate way to write tactics?
The answer is: yes and no. The Ring tactic
uses intensively the conversion
rule of Cic, that is replaces proof by computation the most as it is
possible. It can be useful in all situations where a classical tactic
generates huge proof terms. Symbolic Processing and Tautologies are
in that case. But there are also tactics like Auto or
Linear: that do many complex computations, using side-effects
and backtracking, and generate
a small proof term. Clearly, it would be a non-sense to
replace them by tactics using reflection.
Another argument against the reflection is that Coq, as a
programming language, has many nice features, like dependent types,
but is very far from the
speed and the expressive power of Objective Caml. Wait a minute! With Coq
it is possible to extract ML code from Cic terms, right? So, why not
to link the extracted code with Coq to inherit the benefits of the
reflection and the speed of ML tactics? That is called total
reflection, 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 some work to achieve that goal.
Another brilliant idea from Benjamin Werner: reflection could be used
to couple a external tool (a rewriting program or a model checker)
with Coq. We define (in Coq) a type of terms, a type of
traces, and prove a correction theorem that states that
replaying traces is safe w.r.t some interpretation. Then we let
the external tool do every computation (using side-effects,
backtracking, exception, or others features that are not available in
pure lambda calculus) to produce the trace: now we replay the trace in
Coq, and apply the correction lemma. So internalization seems to be
the best way to import ... external proofs!