The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

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.

  Still I completely miss why would Program be any inferior to refine for such examples, which you seem to be implicitly claiming. Your solution, using your proof-in-one-go style, can be similarly expressed using Program (see attached script) resulting in a cleaner, shorter script. And I think that using Program merely as a substitute for refine (without using more advanced features of Program), already takes the advantage of the Program syntax (equivalent of the syntax of "normal" definitions), which nicely separates the definition (skeleton) and the generated proof obligations (which is not the case with refine, which operates on the level of proof tactics).

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski
The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================

Attachment: prefix-ac.v
Description: Binary data