The Coq mailing list

[C T McBride <c.t.mcbride AT durham.ac.uk>]

Hi

DY> I think many people have encoded certain systems in Coq using de Bruijn
DY> indices. But I was wondering if anyone has encoded their de Bruijn
DY> indices using dependent types so that the level information (i.e., how
DY> many variables are free in the current terms) is captured in the types,
DY> for instance, as follows:
DY>
DY> Inductive exp : nat -> Type :=
DY>  | ref : (i:nat) (exp (S i))
DY>  | lam: (i:nat) (exp (S i)) -> (exp i)
DY>  | app: (i:nat) (exp i) -> (exp i) -> (exp i)
DY>  | lift: (i:nat) (exp i) -> (exp (S i)).

The LEGO development of substitution (and its laws) for a very similar
representation to this can be found in chapter 7 of my thesis.

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

The extra lifting is inevitable, but should not be too tricky. The
failure to typecheck seems odd to me. How are you trying to write this
function? I wouldn't necessarily expect Coq's pattern matching syntax
to cope with it, but it should be fairly straightforward to build this
function with tactics.

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

It's not necessarily the dependent products which are
unwieldy. There's a standard technique which can be used
systematically (or even implemented as a tactic) to program with data
structures like exp. Details can be found in my thesis, or in my TYPES
2000 paper `Elimination with a Motive'. The basic idea is that if
you're trying to write a program whose type is

  (x1:X1,..,xn:Xn,e:exp (f x1 .. xn))(T x1 .. xn e)

you transform that goal into the equivalent

  (n:nat,e':exp n,x1:X1,..,xn:Xn,e:exp (f x1 .. xn))
    (n = f x1 .. xn) -> (e' = e) -> (T x1 .. xn e)

where = here is John Major equality.

Now you can eliminate e' by the usual induction principle for exp,
leaving subgoals which contain equational constraints. Discrimination
can often get rid of impossible cases. Injectivity and substitutivity
can often simplify the possible cases. Basically, you apply a
first-order unification algorithm to the equational hypotheses.

Even without a tactic to do all this for you, it should not be too
difficult (although perhaps a bit tiresome) to follow this procedure by
hand.

By the way, this de Bruijn representation is discussed in Thorsten
Altenkirch and Bernhard Reus's CSL 1999 paper, called something like
`Monadic presentations of lambda terms'. The well-scoped terms are
just for breakfast. Lunch is the well-typed terms in the simply-typed
lambda-calculus. A typechecker for the latter (which is guaranteed to
be correct just by its own rather informative type) can be found in my
recent paper with James McKinna `The view from the left'.

Programming with inductive families is pleasurable and highly
addictive. There is no good reason not to do it in Coq.

Cheers

Conor