Induction Principles

This short file gives some induction principles which deal with the recursor and iterator on the natural numbers. For their use in inductive proofs using deliverables see (##mckinnaphd ##mckinnaphd).

 ** Module lib_more_induction Imports lib_nat
  nat_iter_induction = ... :
    [Pred=[a:Type]a->Prop]{gamma|Type}{z|gamma}{s|gamma->gamma}
    {phi:Pred gamma}(phi z)->({g:gamma}(phi g)->phi (s g))->
    [rec=nat_iter z s]{n:nat}phi (rec n)
  nat_rec_induction = ... :
    [Rel=[a:Type][b:Type]a->b->Prop]{gamma|Type}{z|gamma}
    {s|nat->gamma->gamma}{phi:Rel nat gamma}(phi zero z)->
    ({m:nat}{g:gamma}(phi m g)->phi (suc m) (s m g))->[rec=nat_rec z s]
    {n:nat}phi n (rec n)
  nat_iter_induction_rev = ... :
    [Pred=[a:Type]a->Prop]{gamma|Type}{z|gamma}{s|gamma->gamma}
    {phi:Pred gamma}{n:nat}(phi (nat_iter z s n))->
    ({g:gamma}(phi (s g))->phi g)->phi z