The Coq mailing list

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

> * 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).

BTW, all I can find in the tutorial is one example with a short  
paragraph of explanation (on p. 47) -- not really enough to get the  
full picture of what "fix" is doing.  Is there a longer discussion  
anyplace, or should I just try to read the source?

Meta-question: This discussion has been extremely informative and it  
would be a shame for it to get lost in the mailing list archives.  I  
would be very happy to cut and paste all of the relevant emails into  
a Wiki page or some such if there were an easy and obvious way to do  
it.  Is there?  (It's not clear whether the cocorico site is still  
alive -- all the recent edits seem to be spam.)

    - Benjamin



> 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