The Coq mailing list

[Randy Pollack <rap AT dcs.ed.ac.uk>]

Consider the following natural definition of lambda terms with de
Bruijn indexes for bound variables.

Parameter id: Set.

Inductive obj: Set :=
   vg: id -> obj             (* global name *)
 | vi: nat -> obj            (* local index *)
 | vlam: obj -> obj
 | vapp: obj -> obj -> obj.

Fixpoint shift [i,d:nat; u:obj] : obj := 
  Cases i d u of
    O d u => u
  | i d (vg x) => (vg x)
  | i d (vi j) => (vi (ifdec (* j>= d *) (le_lt_dec d j) (plus j i) j))
  | i d (vlam u) => (vlam (shift i (S d) u))
  | i d (vapp u v) => (vapp (shift i d u) (shift i d v))
  end.

This function "shift" doesn't compute as I expected, because
"le_lt_dec" is Opaque in the library.  Of course, this is just one
lemma; I simply proved it again for myself, making it Transparent.

However when I had finished a small example with these lambda terms, I
had reproved 20 or 30 lemmas from the library.  (When making a library
entry into a defintion one may have to reprove everything it depends
on hereditarily.)

I also find it difficult to discover what lemmas really need to be
made transparent, as "Change", "Exact", etc give no information, and
even tiny examples blow up to thousands of lines when computed as far
as possible.

Is there something I'm missing, that relatively simple examples seem
to require reproving some of the library?

Randy