The Coq mailing list

[Nadeem Abdul Hamid <nadeem AT acm.org>]

Hello,

I am trying to encode a certain type system in Coq and have come
across a difficulty. The basic question is this: I have a definition
of a list of pairs, associating a key (nat) with a value (say, also a
nat). I also have an "if" statement which compares two nat's for
equality and chooses an appropriate branch. Finally, I have a "select"
function which, given a key, s, will search the list, kl, for the key
and return the associated value (or O if not there).  Thus, the Coq
definitions would be something like:

 Inductive KeyList : Set := nil : KeyList
    |  cons : nat -> nat -> KeyList -> KeyList.

 Definition ifeq : (k:Set) nat -> nat -> k -> k -> k := ...

 Fixpoint select [ kl : KeyList ] : nat -> nat
   := [s:nat]
       Cases kl of
     nil => O
   | (cons k v kl') => (ifeq nat s k v (select kl' s)) end.

So, my type system has a "KeyList" in it and a "select" type operator.
Now, say the type system also has polymorphism and thus a key in the
KeyList might actually be a type variable rather than a concrete
natural number. But the type system can still match on these
variables, hence
  select ((alpha, 1)::nil) alpha   |--reduces to-->  1.
Now, I don't know how to encode this in Coq, because the "ifeq" thing
will only reduce on concrete natural numbers, whereas in the
meta-level description of my type system I can also specify rules for
matching and reducing on variables. One option is to encode variables
using a first order encoding (eg. deBruijn indices), instead of higher
order abstract syntax. But are there other, more elegant, ways of
doing this?

Any comments/ideas will be greatly appreciated.

--- nadeem