The Coq mailing list

[Benjamin Werner <Benjamin.Werner AT inria.fr>]

     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


Le 21 nov. 07 à 04:20, Benjamin Pierce a écrit :

> 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
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>          http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club