The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/29/2015 05:06 PM, Zoe Paraskevopoulou wrote:
> Hello everyone,
>
> I am trying to define a recursive function using Program Fixpoint. In 
> particular, I am providing a measure and I am proving that this measure 
> decreases in every recursive call.
>
> However, when I try to prove a lemma involving this function I am unable to 
> use simpl in order to prove the inductive cases and when I try to manually 
> unfold the definition I am getting a very big term.
>
> A simplified and self contained example of the problem I am running into can be 
> found here: https://gist.github.com/zoep/6167e14ed0ebe0887a03 
> <https://gist.github.com/zoep/6167e14ed0ebe0887a03> (the problematic lemma is 
> at the end of the file)
>
> Any help would be greatly appreciated.
>
> Cheers,
> Zoe

I think this is a standard issue with Program - it often produces very 
large proof terms that are very hard to deal with when unfolded.  That's 
just the price of using its automation instead of going it alone.

My way of dealing with functions that have large proof terms is to make 
sure I don't need to unfold them - that their dependent types are 
sufficiently expressive such that the functions themselves can be left 
opaque.  Note that this technique has its own issues - but if it can be 
mastered, I think it has other benefits.  After all, unfolding a 
function is an inherently unmodular thing to do, as it will make any 
resulting proofs very dependent on the current implementation of that 
function.

Assuming you want to stick with what you already have, one thing you 
might want to try is to define a second already reduced version of 
infer_sort as:

Definition infer_sort':= Eval compute in infer_sort.

and see if the proof term of infer_sort' can be dealt with more easily 
when unfolded.  Another thing to try is to use refine instead of Program 
- you'll still get some ability to handle obligations later in proof 
mode, and you'll end up with a less complex proof term (assuming you can 
handle the proof obligations, and that they don't add too much heft).  
Hmmm - I see you use omega.  That in itself can lead to pretty large 
proof terms.  It might be best to use abstract omega instead, making 
sure you export the resulting abstractions so that they aren't just inlined.

-- Jonathan