The Coq mailing list

[t x <txrev319 AT gmail.com>]

I was confused due to not understanding the fundamentals. The link was very helpful (since the code lacked comments).

Are the following correct?

Assertion 1: so informally,

  "index n" is a way to encode {x : 0 <= x < n} as

    None, Some None, Some (Some None), ..., Some^{n-1} None

Assertion 2:

  first always returns None

  last n always returns Some^{n-1} None

  next is meant to build intermediate terms

  lift is from {x : 0 <= x < n} to {x : 0 <= x < n+1}

Assertion 3:

  select is "safe nth"

  eta_index is "safe map"

On Mon, Aug 12, 2013 at 4:56 PM, Valentin Robert <valentin.robert.42 AT gmail.com> wrote:

Hmmm, I don't think there's much to point you at.

Maybe you will want to take a look at the paragraph "Recursive Type
Definitions" in this chapter of CPDT:
http://adam.chlipala.net/cpdt/html/DataStruct.html

This is a fixpoint encoding of homogeneous nested tuples (repeat) and
of finite natural numbers (index).
The latters allow you to safely index a position inside the formers.

The functions are then defined in a somewhat straightforward way:

first is a safe zero.
next is a safe successor function.
last builds (n - 1), the biggest safe index in a set of n elements.
lift lifts an index in a bigger set: it has the same value, but
indexes a set with an additional element.
select safely retrieves an element from a tuple.
eta_index is just some sort of eta-expansion for safely-indexed
collections apparently.

What is confusing you? Is it how these typecheck, what they define, or
the reason why they are defined this way? Or something else?

- Valentin

On Mon, Aug 12, 2013 at 5:36 PM, t x <txrev319 AT gmail.com> wrote:
> In the lambda tamer source, /src/coq/Util.v, there's the following block of
> code:
>
> https://gist.github.com/anonymous/76f36130b1bb9a2f6786
>
> I've played around with a few "Eval compute in ... "
>
> however, it's not clear to me what the intuitive definitions for:
> "first, next, last, lift, select, eta_index"
> are.
>
> Can someone point me at a paper/reference on the theoretical model behind
> this "tuple" ?
>
> Thanks!