The Coq mailing list

[Dachuan Yu <dachuan.yu AT yale.edu>]

Hi,

I think many people have encoded certain systems in Coq using de Bruijn
indices. But I was wondering if anyone has encoded their de Bruijn
indices using dependent types so that the level information (i.e., how
many variables are free in the current terms) is captured in the types,
for instance, as follows:

Inductive exp : nat -> Type :=
 | ref : (i:nat) (exp (S i))
 | lam: (i:nat) (exp (S i)) -> (exp i)
 | app: (i:nat) (exp i) -> (exp i) -> (exp i)
 | lift: (i:nat) (exp i) -> (exp (S i)).

where "ref" is the index case, "lam" is the abstraction case, "app" is
application and "lift" is to increase the level. For example, the closed
term "\lambda(0 (\lambda 0 1))" (indices start from 0) would be encoded
as
"lam
    (app
        (ref O)
        (lam
            (app
                (lift (ref 0))
                (ref 1))))"

I'm doing something similar for a certain system. The trouble I'm having
is that I cannot manage to get my meta-updating function to type-check,
especially in the cases when the "exp" being updated is a "ref" or a
"lift". In addition, an easier but still annoying problem is that, when
updating a "ref", a bunch of extra "lift" is needed, since it is being
put at a deeper level.

Just to clarify, by meta-updating, I meant the function which updates
the indices of B when doing A{{i<-B}} (substituting B for i in A).

I was wondering if anybody has done or tried similar things before. Any
pointers/comments/insights/... would be more than welcome!

Many Thanks

Dachuan