The Coq mailing list

["St�phane Lescuyer" <lescuyer AT lri.fr>]

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
>