The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

          Hello,

There certainly is use for such kind of features. In John Harrison's
terminology, this would mean introducing a little piece of declarative
proof-style, in coq's overhelmingly procedural style (*).  The way I
understand Jean-Christophe remark, is that the problem, or the
question, is a matter of style. In other words, the level this feature
would be introduced will probably induce users to use it in one or
another way, and this is a relevant point.

I mean that if Freek's feature is included in the system, it will not
be long before it is used not only to retrieve lemmas proved not long
ago, but also as a short-cut to retrieve a lemma in some loaded
library, without having to find its name by hand. The name of the
lemma being the calculated at script-run-time.

Then, the next step is probably to have the search in the environement
being done modulo some isomorphisms over the type/proposition, in the
style of the searchiso facility.

All this obviously raises questions of efficiency and of
proof-style. One should not use this kind of facilities anywhere in
the proof. We have already seen that using time-consuming tactics
inside complex scripts involving branching tacticals results in
explosions of the time and memory consumption.

This should however not be understood as a jesuistic plea against
progress. But I do believe these questions are important, and that is
always difficult to back-track once an extension of the system has
been proposed. So I would advocate to be careful and propose a feature
as modest as possible, if it appears necessary.

In the long-run, this is another illustration for a general reflection
about what a good proof-laguage ought to be.




Benjamin




(*) In declaratively style proof languages, one mainly writes
propositions. In procedural-style, on mainly writes proof-steps.