The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Some months ago there was a discussion on "Inductive definitions that
go through lists", in which Benjamin Werner sent the message appended
below.  

Consider the following version of Benjamin's example, where I have
used a (trivially) indexed family of ty instead of Benjamin's
datatype:

  Inductive tag : Set := Tag.
  Inductive ty : tag -> Set :=
  | ty_base : nat -> ty Tag
  | ty_arr  : ty Tag -> ty Tag -> ty Tag
  | ty_rcd  : (List.list (ty Tag)) -> ty Tag.

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

  Lemma ty_myind : forall P: forall (T:tag), (ty T) -> Prop,
       (forall (n:nat), P Tag (ty_base n)) ->
       (forall (t:ty Tag), P Tag t ->
             forall (t0:ty Tag), P Tag t0 -> P Tag (ty_arr t t0)) ->
       (forall (a:list (ty Tag)), liftp Tag (P Tag) a -> P Tag (ty_rcd a)) ->
         (forall (T:tag) (t:ty T), P T t).
  Proof.
  fix 5.
  intros P pb pa pl T. intros [n|t u|l].
  apply pb.
  apply pa; apply ty_myind; assumption.
  apply pl.
  elim l.
    simpl; trivial.
  clear l; intros t l hl; split.
    apply ty_myind; assumption.
  assumption.
  Qed.

The proof is the same as Benjamin's proof, but this one fails at
"Qed", apparently something about the use of "fix".  What is the
problem, and how do I make this work?

My real example has several syntactic classes of object terms,
mutually defined, using lists in various constructors.  I want to use
an indexed family of object terms, instead of explicit mutual
inductive definition, to take advantage of uniformity: e.g. only one
predicate P needs to be lifted.

Thanks,
Randy
---
Benjamin Werner writes:
 >       Hello Benjamin,
 > 
 > The Coq implementation does not provide a good induction principle,  
 > but the type theory does not forbid it.
 > 
 > You first have to state what your induction principle has to look  
 > like, and thus what the induction
 > hypothesis for the   (alist ty)  looks like.
 > 
 > Here is one possibility. I just replaced alist by list for  
 > simplification:
 > 
 > 
 > 
 > 
 >     Inductive ty : Set :=
 >       | ty_base     : nat -> ty
 >       | ty_arrow    : ty -> ty -> ty
 >       | ty_rcd      : (list ty) -> ty.
 > 
 > Fixpoint liftp (P:ty->Prop)(l:list ty) {struct l} : Prop := match l with
 > | cons t l => P t /\ liftp P l
 > | _ => True
 > end.
 > 
 > Lemma ty_myind : 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 : list ty,liftp P a ->  P (ty_rcd a)) ->
 >           (forall t : ty, P t).
 > Proof.
 > fix 5.
 > intros P pb pa pl [n|t u|l].
 > apply pb.
 > apply pa; apply ty_myind; auto.
 > apply pl.
 > elim l.
 >   simpl; trivial.
 > clear l; intros t l hl; split.
 >   apply ty_myind; trivial.
 > assumption.
 > Qed.
 > 
 > 
 > Note that:
 > 
 > * When using the (not very documented) fix tactic, you have to be  
 > careful
 > not using your induction hypothesis too early in the proof. If not,  
 > you get
 > an unpleasant surprise when you do Qed.
 > (basically, fix gives you a too strong IH, it is your responsability  
 > to apply
 > it only to arguments which are structurally smaller).
 > 
 > * In the example above, you then have to prove that under the same  
 > hypotheses
 > you have (liftp P l) for any  l: list ty
 > but this should be easy by (regular) induction over l and using  
 > ty_myind.
 > 
 > * The definitions of the type theory which make this correct are  
 > described in the ref man.
 > The fix tactic is in the tutorial on recursive types (Gimenez and  
 > Casteran).
 > 
 > 
 > Maybye there are smoother versions of the above. 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.
 > 
 > Hope this helps,
 > 
 > 
 > Benjamin