The Coq mailing list

[G�rard Huet <Gerard.Huet AT inria.fr>]

Le vendredi, 23 mai 2003, à 19:56 Europe/Paris, Dachuan Yu a écrit :

> 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!

Well, I tried that a long time ago, when I was doing the proof of 
Church-Rosser theorem
in Coq. THis looked like a natural idea. But dependent products are 
very unwieldy, and
so I backtracked and put the contextual invariants in logic rather than 
in the types.
G. Huet