]> matita.cs.unibo.it Git - helm.git/blob - matita/library_auto/auto/nat/sigma_and_pi.ma
debian package for matita
[helm.git] / 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.