The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/01/2014 02:16 PM, Craig McLaughlin wrote:
> Thanks Jonathan! I was hesitant to use the proof mechanism to define 
> functions
> for fear that the implementation would be much less efficient than 
> PROGRAM.
> However, it seems much easier to define dependently typed functions 
> this way;
> in the past I also have tried the [refine] tactic but found it to be 
> awkward
> to use for the impossible cases.
>
> Is there much consensus within the Coq community on the most favourable
> approach?

I don't know anything about a consensus.  Probably the only consensus 
is: whatever works for you.

But, note that there are several disadvantages to using proofs to define 
functions.  One is that the resulting proof term can be quite unwieldy, 
and is going to make some proofs about the function - those which have 
to unfold the function - more difficult (although using Program often 
creates a similar problem).  Another is that a tactic script proof 
doesn't resemble what most people consider a program, so if you care 
about the appearance of the script instead of just how it extracts, that 
might discourage you.  Another is that while formulating the proof 
script, if the goal type isn't sufficiently constrained, then one can 
easily get confused about how subgoals within the proof correspond to 
points within the function definition.

But, even if one or more of the above (or something else) is reason 
enough for you to not use proofs to define functions - if you get stuck, 
it might help you to try a proof to see how the subgoals proceed during 
proof interaction, or even what the resulting proof term is (by using 
Print, or Compute to get some simplification).

Personally, I view the advantages of using proofs to define functions 
(tactic power with respect to dependent types, incremental interaction 
with the prover, proof automation and user-defined tactics) to outweigh 
the disadvantages.  I try to arrange things such that the dependent type 
of functions I define is sufficiently constrained so that I don't need 
to unfold functions (I view unfolding of non-trivial functions as 
unmodular anyway) in other proofs, and also don't need to keep precise 
track of the correspondence between subgoals and points within the 
function definition.  I also do extraction after every non-trivial 
function definition to make sure the proof did what I wanted.

-- Jonathan