The Coq mailing list

[Thorsten Altenkirch <txa AT Cs.Nott.AC.UK>]

Hi,

some comments on the Benjamins' emails:

Indeed, every strictly positive operator on types F : Type -> Type  
gives rise to a modality:

        P : A -> Type
        ---------------------
        [] F : F A -> Type

moreover, we have a dependent version of map

        f : forall a:A, P a
        ---------------------------------
        dmap f : forall x:F A,[] P x

Using this, one can formulate a generic eliminator for the inductive  
type mu F:Type with the constructor
in : F(mu F) -> mu F:

        P : mu F -> Type
        m :  forall x:F(mu F), [] P x -> P (in x)
        ------------------------------------------------
        elim P m : forall x:mu F,  P x

and the computation rule

        elim P m (in x) = dmap (elim P m) x

Benjamin P's type is isomorphic to the inductive type generated by

        F X = nat + X * X + list X

which is strictly positive because X appears strictly positive in  
list X. This is the theory, how difficult (and how useful) it would  
be to implement it in Coq, I don't know.

Peter Morris investigated the [] modality (and its dual <>) in his  
recent PhD thesis on generic programming with dependent types (http:// 
www.cs.nott.ac.uk/~pwm/thesis.pdf).

Actually, in an extensional theory every functor gives rise to the []- 
modality, but only strictly positive ones (or containers) give rise  
to the dual <>, it seems. In any case, from a foundational point of  
view one may not want to accept non-strictly positive inductive types  
(like mu X.(X->Bool)->Bool) anyway.
        
Cheers,
Thorsten



On 21 Nov 2007, at 10:32, Benjamin Werner wrote:

>      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
>
> --------------------------------------------------------
> 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


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.