The Coq mailing list

[James Wilcox <wilcoxjay AT gmail.com>]

Hi Zoe,

Program often leads to this kind of dilemma: either prove everything in the definition using dependent types, or deal with massive proof terms. The latter approach is basically untenable (if you google you won't find any examples that do it...). I forked and updated your gist with an example of how to use the former approach. https://gist.github.com/wilcoxjay/8b05e7e408c7eb9c733b

If you prefer to have your proofs separate, I recommend staying away from Program. If you need to do general recursion, you can program directly with Fix, as described by Adam here: http://adam.chlipala.net/cpdt/html/GeneralRec.html

Good luck!

James

On Sun, Mar 29, 2015 at 2:06 PM, Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com> 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 (the problematic lemma is at the end of the file)

Any help would be greatly appreciated. 

Cheers, 

Zoe