The Coq mailing list

[Benjamin Pierce <bcpierce AT cis.upenn.edu>]

This week, I wanted to show my programming languages class how to  
extend the simply typed lambda-calculus with records.  So I wrote the  
obvious thing:

   Inductive ty : Set :=
     | ty_base     : nat -> ty
     | ty_arrow    : ty -> ty -> ty
     | ty_rcd      : (alist ty) -> ty.

This seemed happy for a while, until I discovered that the induction  
principle Coq had generated

   ty_ind
     : forall P : ty -> Prop,
       (forall n : nat, P (ty_base n)) ->
       (forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t  
t0)) ->
       (forall a : alist ty, P (ty_rcd a)) -> forall t : ty, P t

was completely useless!  (The last case gives no IH for reasoning  
about records.)

I asked around a little at Penn and was told that this was a common  
issue and the usual way around it was to "lift" the nil and cons  
constructors of lists into my term syntax, like this:

  Inductive ty : Set :=
    | ty_base     : nat -> ty
    | ty_arrow    : ty -> ty -> ty
    | ty_rcd_nil  : ty
    | ty_rcd_cons : nat -> ty -> ty -> ty.

This made me a little less happy because it slightly changes the  
language I'm defining, but I pushed ahead and succeeded in proving  
all the things I wanted to about the system.

Next, I'd like to show the class the "dual" extension: variants  
(i.e., disjoint sums with any number of labeled summands).  But this  
time I'm even less happy.  I'd like to write

  Inductive tm : Set :=
    | tm_var : nat -> tm
    | tm_app : tm -> tm -> tm
    | tm_abs : nat -> ty -> tm -> tm
    | tm_inj : nat -> tm -> tm
    | tm_case : tm -> list (nat * tm) -> tm.

where the last constructor represents an n-ary case construct whose  
concrete syntax might look like this:

     case t0 of <l1=x1> => t1
              | ...
              | <ln=xn> => tn

This won't work for the same reason as before.  And, while I can  
roughly see how to generalize the "case" constructor into a "nil" and  
a "cons" part as I did for records, this is really getting a bit  
awkward.

Is there a more direct way to do such things?

Thanks!

    - Benjamin