The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hello,

Le 27 juin 2013 à 09:03, Guillaume Melquiond 
<guillaume.melquiond AT inria.fr>
 a écrit :

> Le 27/06/2013 08:28, t x a écrit :
>> >> The process of writing such functions is a bit convoluted, so you
>> may first want to experiment with Program, as suggested by Daniel
>> Schepler, as it offers a trade-off between ease-of-use and term ugliness.
>> 
>> Given my ignorance, can you expand on this? (I see no tradeoff at all.)
>> 
>> Naively, it appears to me that Daniel's solution (Program Fixpoint) is
>> superior for both ease-of-use _and_ term elegance? In fact, it's not
>> clear to me why I would ever want to use "Definition ... Proof. ....
>> Defined." rather than "Program Fixpoint" for these situations.
> 
> The thing is, Program Definition is a heuristic. It puts in the context 
> everything it thinks you might need to perform the proof. If it puts too 
> much, you get a lot of noise in the resulting term. If it puts too little, 
> you can no longer prove your function. So it tries to be clever and makes 
> choices. Your example is a bit too simple for these issues to occur, but 
> still you can get a feel of them.
> 
> For the "too much" case, look at the term generated by Program. You will 
> notice an "eq_refl" term lying around, while it is not present in a 
> manually-produced term.
> 
> For the "too little" case, replace Z_eq_dec by Zeq_bool inside your 
> definition and try to prove it again with Program. Surprise! You cannot any 
> longer, because the heuristic decided that the value of this boolean was 
> useless for the proof, while it is obviously mandatory.

Indeed, it's a tradeoff. To tame these issues of heuristic choice of what to 
reflect in the context and what
to leave out, there's a few tricks you can use:

- (too much) putting a [return _] after a [match] construct in a Program will 
deactivate
the generation of equalities between the pattern-matched object and it's 
constructors and
use the regular pattern-matching compilation scheme of Coq.

- (too little) [if then else] does not add an equality by default, but 
using [dec b = sumbool_of_bool b], you can get the equality (e.g., [if (dec 
b) then _ else _])

Regarding term ugliness, I suggest proving the equations defining your 
function and/or
its graph after its definition and rely on that view instead of the term 
generated by Program.

Best,
-- Matthieu