The Coq mailing list

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

Hello, 

Thank you all for your answers, I really appreciate your help!

On Mar 30, 2015, at 1:16 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

  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. 

With this I had with the same problem with the original proof, I cannot handle the inductive case. Further case analysis also does not seem to help.

On Mar 30, 2015, at 1:16 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

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

it work on this example. 

I also tried (unsuccessfully) make it work with [Function].

On Mar 30, 2015, at 12:31 AM, Jonathan Leivent <jonikelee AT gmail.com> wrote:

Definition infer_sort':= Eval compute in infer_sort.

Unfortunately, this takes way to much time (even with a lazy evaluation strategy) so I was not able to see if it is helpful at all. 

I think I will go for one of the following: 

- The dependent types solution (proposed by Jonathan and James) which seems to work fine and I hope it scales to more complex functions and specifications.

- I also think that I can completely circumvent the problem (for now) by defining everything relationally as inductive definitions (I won’t need sort_infer for this). 

- Switch to plain De Bruijn indices instead of locally nameless representation that will allow me to define such functions with structural recursion. 

Cheers, 

Zoe