The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Adam Koprowski wrote:
>   ... or if you are not a huge fun of 'refine' and you don't like to 
> define things by means of tactics, then the new Program feature of Coq 
> is your friend. You can define your function in pretty much the same 
> way as you'd do in some functional programming language and then you 
> can prove properties about this function; and the two steps are nicely 
> coupled together with Program (see solution below, which gives exactly 
> the same program as the previous solution but I think the definitions 
> & proofs are cleaner; although that's always a matter of taste).

"Program" is a useful feature, but I think a lot of Coq users (and 
potential users) have gotten a very inaccurate idea of what it 
provides.  It may be discomfiting at first to build a program using the 
[refine] tactic, but there is really no practical difference between 
that style and the style of [Program].  [Program] provides some new 
features that [refine] doesn't, but, for instance, your example of 
[is_prefix_dec] uses just one of those features, which lets you avoid 
annotations on dependent [match]es.  A little extra verbosity (of the 
easy-to-write-and-follow kind) makes up for that in the implementation I 
sent to the list earlier, and I believe 8.2 is doing some new [match] 
annotation inference that either now or in future iterations will remove 
this advantage altogether.

On the issue of proofs, I think the proof scripts in both your (Adam 
Koprowski's) code and the code of the mysterious "muad" are manual 
enough that I would refuse to accept them in a serious development. ;-)  
I say that every certified function should have a single proof script 
associated with it, and that proof script should be a single tactic, 
with no intermediate periods.  That style (which I used in my 
implementation posted earlier) is easy to use when you commit to 
following it, and it has many advantages in brevity of code and 
resilience to changes in specs and implementations.