The Coq mailing list

[Robert Dockins <robdockins AT fastmail.fm>]

On Tuesday 20 November 2007 10:20:03 pm Benjamin Pierce wrote:
> 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
[snip]
> was completely useless!  (The last case gives no IH for reasoning
> about records.)

[snip more discussion]


One way to do it is to define the list as a mutually recursive type:

  Inductive ty : Set :=
    | ty_base : nat -> ty
    | ty_arrow : ty -> ty -> ty
    | ty_rcd : ty_list -> ty
   with ty_list : Set :=
    | tyl_nil : ty_list
    | tyl_cons : ty -> ty_list -> ty_list.

  Reset ty_ind.

  Scheme ty_ind := Induction for ty Sort Prop
    with ty_list_ind := Induction for ty_list Sort Prop.

  Check ty_ind.
  (*
  ty_ind
     : forall (P : ty -> Prop) (P0 : ty_list -> Prop),
       (forall n : nat, P (ty_base n)) ->
       (forall t : ty, P t -> forall t0 : ty, P t0 -> P (ty_arrow t t0)) ->
       (forall t : ty_list, P0 t -> P (ty_rcd t)) ->
       P0 tyl_nil ->
       (forall t : ty,
        P t -> forall t0 : ty_list, P0 t0 -> P0 (tyl_cons t t0)) ->
       forall t : ty, P t
  *)

Unfortunately, you lose all the nice list operators and lemmas that are 
defined in the standard libraries.  Also, the mutually recursive induction 
principle above is kind of a pain to use because you have to specify the 'P0' 
predicate on list types.  On the whole, it's maybe not a lot nicer than 
directly lifting the list into the type, at least for this example.  Maybe it 
wins out for the language with sums.

The other way I could imagine doing it would be to directly prove the 
induction principle you want using 'fix'.  It's sort of tedious to do this, 
but not really very difficult.  The trick is inventing the "right" induction 
principle to prove in the first place.  This is nicer in terms of the end 
result, but it is obviously sort of lame that you have to prove the induction 
principle yourself.


  Require Import List.

  Inductive ty : Set :=
    | ty_base : nat -> ty
    | ty_arrow : ty -> ty -> ty
    | ty_rcd : list ty -> ty.

  Reset ty_ind.

  Definition 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 l : list ty, (forall t, In t l -> P t) -> P (ty_rcd l)) ->
    forall t : ty, P t.

  intros P Hbase Harr Hrcd.
  refine (fix IH (t:ty) {struct t} : P t := _).
  case t; intros.
  apply Hbase.
  apply Harr; apply IH.
  apply Hrcd.
  induction l.
  simpl; intros; contradiction.
  simpl; intros; destruct H.
  subst t0.
  apply IH.
  apply IHl; apply H.
  Qed.  
  
  Check ty_ind.
  (*
  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 l : list ty, (forall t : ty, In t l -> P t) -> P (ty_rcd l)) ->
       forall t : ty, P t
  *)




I don't know of a better solution offhand.  Maybe the experts know some other 
strategy.

Rob Dockins