The Coq mailing list

[Xavier Leroy <Xavier.Leroy AT inria.fr>]

> [...] Also, my understanding is that if this work is not done
> generically by Coq, it is a.o. because it is not so trivial to state
> the good induction principle.

I believe there exists a "best" (most general) induction principle,
which is the one given by Stéphane Lescuyer -- the one with two
parameterized Props, one for "ty" and the other for "list ty".
Indeed, this is the principle that Scheme generates if you define "ty"
and "list_of_ty" by mutual induction:

    Inductive ty : Set :=
      | ty_base     : nat -> ty
      | ty_arrow    : ty -> ty -> ty
      | ty_rcd      : list_of_ty -> ty
    with list_of_ty : Set :=
      | ty_nil      : list_of_ty
      | ty_cons     : ty -> list_of_ty -> list_of_ty.

I would be very happy indeed if "Scheme" was extended to generate the
(mutual) induction principle for "ty" and "list ty", or more generally
"T" and "OP T" where OP: Set -> Set is a covariant type operator.
In Coq developments related to programming language theory, that would
save a lot of redefinitions of list types like in the example above.

From this mutual induction principle, it is rather easy to prove more
specialized principles like the one Benjamin W. showed, with "liftp P"
as the property for "list ty" --- certainly easier than proving them
from scratch.

One last remark: in Benjamin's solution, an arguably nicer definition
of "liftp" would be

Definition liftp (P:ty->Prop)(l:list ty) : Prop :=
  forall x, In x l -> P x.

instead of

Fixpoint liftp (P:ty->Prop)(l:list ty) {struct l} : Prop := match l with
| cons t l => P t /\ liftp P l
| _ => True
end.

I think it's nicer because the user can then reuse properties of "In"
found in the standard library, rather than having to prove their
equivalents for "liftp".

- Xavier Leroy

PS for Benjamin P: now you understand why there are very few POPLmark
solutions that address part B of the challenge :-)