The Coq mailing list

[Zoe Paraskevopoulou <zoe.paraskevopoulou AT gmail.com>]

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