The Coq mailing list

[Gyesik Lee <gslee AT ropas.snu.ac.kr>]

Hi, thanks for the replies.

2010/3/18 Roman Beslik
> Hi. It is not clear, what do you suppose "to_T" to do. In "(const _ n)" "n"
> is of arbitrary type, but in "A n" "n" is of type "nat".

Because we are instantiating with RT, n should be a natural number.
Indeed if we use the proof mode as in third and fourth attempt, we can
make that type check.

As you see in fourth attempt, the proof mode doesn't work when
recursive cases are involved.
Coq fails to do the termination check although the proof is based on a
well-founded (structural) relation.

So we were asking two questions:

a) How to use Fixpoint to deal with dependent type matching similar to
the first and second attempt?
b) How to overcome the termination check in proof mode when using
well-founded (structural) relation as in the fourth attempt?

2010/3/18 Adam Chlipala 
<adam AT chlipala.net>:
> It's possible that there are some issues specific to your problem that
> deserve discussion on this list, but my recommendation is to read some parts
> of CPDT that discuss programming with dependent types:
>    http://adam.chlipala.net/cpdt/
> I expect Chapter 7 is the most relevant, as I see your code contains some of
> the mistakes described there.  Really, of course, I recommend the whole book
> up to Part III for anyone who wants to put Coq to work. ;)

Indeed, I was reading that Chapter 7 and noticed that generalizing the
resulting type would solve the problem. But then this forces us to
generalize other definitions we want to avoid when possible.

Gyesik