The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Zoe,

  the classic answer is to build an unfolded version (without Program and which 

calls the folded version at recursive calls) and show extensional equivalence of 

the two definitions, then you can easily control unfolding using rewriting, and 

avoid the clutter due to decoration of matches with equalities at matches. 

Otherwise you might find the [lazy] reduction strategy useful, but mainly for 

full normalization. [Function] might help too but I couldn't manage to make 

it work on this example. 

Best,

-- Matthieu

2015-03-29 23:06 GMT+02:00 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