matita/library_auto/auto/nat/sigma_and_pi.ma

   1 (**************************************************************************)
   2 (*       ___                                                                *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        Matita is distributed under the terms of the          *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/library_auto/nat/sigma_and_pi".
  16
  17 include "auto/nat/factorial.ma".
  18 include "auto/nat/exp.ma".
  19 include "auto/nat/lt_arith.ma".
  20
  21 let rec sigma n f m \def
  22   match n with
  23   [ O \Rightarrow (f m)
  24   | (S p) \Rightarrow (f (S p+m))+(sigma p f m)].
  25
  26 let rec pi n f m \def
  27   match n with
  28   [ O \Rightarrow f m
  29   | (S p) \Rightarrow (f (S p+m))*(pi p f m)].
  30
  31 theorem eq_sigma: \forall f,g:nat \to nat.
  32 \forall n,m:nat.
  33 (\forall i:nat. m \le i \to i \le m+n \to f i = g i) \to
  34 (sigma n f m) = (sigma n g m).
  35 intros 3.
  36 elim n
  37 [ simplify.
  38   auto
  39   (*apply H
  40   [ apply le_n
  41   | rewrite < plus_n_O.
  42     apply le_n
  43   ]*)
  44 | simplify.
  45   apply eq_f2
  46   [ apply H1
  47     [ auto
  48       (*change with (m \le (S n1)+m).
  49       apply le_plus_n*)
  50     | auto
  51       (*rewrite > (sym_plus m).
  52       apply le_n*)
  53     ]
  54   | apply H.
  55     intros.
  56     apply H1
  57     [ assumption
  58     | auto
  59       (*rewrite < plus_n_Sm.
  60       apply le_S.
  61       assumption*)
  62     ]
  63   ]
  64 ]
  65 qed.
  66
  67 theorem eq_pi: \forall f,g:nat \to nat.
  68 \forall n,m:nat.
  69 (\forall i:nat. m \le i \to i \le m+n \to f i = g i) \to
  70 (pi n f m) = (pi n g m).
  71 intros 3.
  72 elim n
  73 [ simplify.
  74   auto
  75   (*apply H
  76   [ apply le_n
  77   | rewrite < plus_n_O.
  78     apply le_n
  79   ] *)
  80 | simplify.
  81   apply eq_f2
  82   [ apply H1
  83     [ auto
  84       (*change with (m \le (S n1)+m).
  85       apply le_plus_n*)
  86     | auto
  87       (*rewrite > (sym_plus m).
  88       apply le_n*)
  89     ]
  90   | apply H.
  91     intros.
  92     apply H1
  93     [ assumption
  94     | auto
  95       (*rewrite < plus_n_Sm.
  96       apply le_S.
  97       assumption*)
  98     ]
  99   ]
 100 ]
 101 qed.
 102
 103 theorem eq_fact_pi: \forall n. (S n)! = pi n (\lambda m.m) (S O).
 104 intro.
 105 elim n
 106 [ auto
 107   (*simplify.
 108   reflexivity*)
 109 | change with ((S(S n1))*(S n1)! = ((S n1)+(S O))*(pi n1 (\lambda m.m) (S O))).
 110   rewrite < plus_n_Sm.
 111   rewrite < plus_n_O.
 112   auto
 113   (*apply eq_f.
 114   assumption*)
 115 ]
 116 qed.
 117
 118 theorem exp_pi_l: \forall f:nat\to nat.\forall n,m,a:nat.
 119 (exp a (S n))*pi n f m= pi n (\lambda p.a*(f p)) m.
 120 intros.
 121 elim n
 122 [ auto
 123   (*simplify.
 124   rewrite < times_n_SO.
 125   reflexivity*)
 126 | simplify.
 127   rewrite < H.
 128   rewrite > assoc_times.
 129   rewrite > assoc_times in\vdash (? ?  ? %).
 130   apply eq_f.
 131   rewrite < assoc_times.
 132   rewrite < assoc_times.
 133   auto
 134   (*apply eq_f2
 135   [ apply sym_times
 136   | reflexivity
 137   ]*)
 138 ]
 139 qed.