The Coq mailing list

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

Thank you, everybody!!!  This is all extremely useful...

    - Benjamin


On Nov 21, 2007, at 8:14 AM, Stéphane Lescuyer wrote:

> Hi Benjamin,
>
> Although Benjamin W's solution will do the trick in most situations,
> you may find yourself a situation where the 'lifted predicate' for  
> lists
> associated with the predicate P you want to prove is not of the above
> form, namely you cannot prove (P (ty_rcd tl)) by just knowing (P t)  
> for
> every t in tl, but you need a more global property of the list tl,  
> which
> means you would design an ad hoc predicate over lists corresponding  
> to P.
> In such cases, you might need the following (and I believe, more  
> general)
> induction principle :
>
>  Inductive ty : Set :=
>      | ty_base     : nat -> ty
>      | ty_arrow    : ty -> ty -> ty
>      | ty_rcd      : (list ty) -> ty.
>
> Section ty_ind.
>   (** P is the predicate you wish to prove, liftedP is P lifted over
> lists in "some way" *)
>   Variables (P : ty -> Type) (liftedP : list ty -> Type).
>
>   Hypotheses
>    (** Traditional induction hypotheses *)
>    (Hbase : forall n, P (ty_base n))
>    (Harrow : forall ty1 ty2, P ty1 -> P ty2 -> P (ty_arrow ty1 ty2))
>    (** Special hypotheses for the ty_rcd case *)
>    (H_rcd   : forall lt, liftedP lt -> P (ty_rcd lt))
>    (H_rcd0 : liftedP nil)
>    (H_rcd1 : forall t lt, P t -> (liftedP lt) -> liftedP (t::lt)).
>
>   (** Then you can define the induction principle *)
>   Fixpoint ty_ind_alt (t : ty) : P t :=
>     match t as x return P x with
>     | ty_base n => Hbase n
>     | ty_arrow t1 t2 => Harrow t1 t2 (ty_ind_alt t1) (ty_ind_alt t2)
>     | ty_rcd lt =>
>       H_rcd lt (((fix l_ind (lty : list ty) : liftedP lty :=
>                      match lty as x return liftedP x with
>                      | nil => H_rcd0
>                      | cons t lty' => H_rcd1 t lty' (ty_ind_alt t)  
> (l_ind lty')
>                      end)) lt)
>    end.
> End ty_ind.
>
> You can easily design the same kind of induction principles for a
> predicate over two types t1 and t2, which comes in handy at times.
>
> Hope this helps,
>
> Stéphane Lescuyer
> --
> http://www.lri.fr/~lescuyer/
>
> On Nov 21, 2007 12:50 PM, Thorsten Altenkirch <txa AT cs.nott.ac.uk>  
> wrote:
> > 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.
> >
> >
> > --------------------------------------------------------
> > 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