The Coq mailing list

[t x <txrev319 AT gmail.com>]

Guillaume, Matthieu:

Understood.

Thanks for explaining all the subtleties of these two techniques. (I can easily imagine a world where I stupidly run into problems with Program Fixpoint and not realize the problem is with the auto generated obligations.)

On Thu, Jun 27, 2013 at 2:35 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

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