The Coq mailing list

[t x <txrev319 AT gmail.com>]

Hi,

Short question: what am I doing wrong with dependent-types?

Long question: consider this example here:

https://gist.github.com/anonymous/ebbf5a5fc3be7b0f0bfa

We have

  inRange, validRange, validIndex

both as _prop and as _dtype.

Imagine we have:

  (1) lst: a list,

  (2) r: a valid range of the list

  (3) i: a element in range r

and we want to call a function which takes:

  (1) lst: the above list

  (2) i: above i, with proof its a validIndex of lst

Now, in the _prop world, this transform can be phrased as lem_000_prop (line 39). In the _dtype world, how do I phrase this?

In particular, I get stuck on the following:

  * in the _prop world, $i$ is a Z, with property that it's inRange r, and I want to to show that $i$ also has property validIndex lst

  * in the _dtype world, $i$ has type {i: nat| inRange r i}, and I want to construct something of dtype validIndex lst -- so somehow, I want to say:

  there exists an $j$ of type validIndex lst,

    where proj1_sig j = proj1_sig i

  (because I want to use "the same" i)

  Naively, to me, it appears the _prop world is better since it's easier to say "use the same i; we're now going to show it has more properties" whereas the _dtype world I have to say "well, there exists an element of type validIndex lst, such that their proj1_sig are the same"

Clearly I'm misunderstanding something. What am I doing wrong?

(I've looked at chapter 6 of CPDT, I don't see anything that adresses my particular problem.)