The Coq mailing list

[Robin Green <greenrd AT greenrd.org>]

On Fri, 21 Dec 2007 10:15:32 +0100
Pierre Casteran 
<pierre.casteran AT labri.fr>
 wrote:

> > (2) You can use these techniques for programm building: if you
> > "prouve" the goal of type: forall l:list, Sorted_list(l). With
> > Sorted_list(l) the type of all sorted lists of l (i.e. sorted lists
> > with the same elements than l), than you have built a programm that
> > sorts a list, and in the same time proven it's correctness.
> >   
> 
> Yes, but consider also  that, if you build a term of such a type by 
> using automatic tactics,
> you may not control the underlying algorithm, and obtain a very 
> inefficient sorting algorithm.

Well, the generated term can be (in principle at least) inspected with
the Print command afterwards, and you can use more "specific" tactics
such as refine, apply and exact instead of more "general" tactics such
as auto, to control what is produced to an (in principle) arbitrary
level of detail. Also, understanding what terms the tactics generate is
an advantage here.

The real danger, I think is automation tactics such as auto and
firstorder. If you change your hints, or a new version of Coq starts to
use new algorithms, for example, the program generated may be changed
for the worse. (It is particularly dangerous if your goal underspecifies
the algorithm, of course, because then the "wrong" algorithm altogether
may be generated. But that's easily fixed by correcting the goal.)

-- 
Robin