]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/lib/arithmetics/sigma_pi.ma
- probe: new application to compute some data on the proof objects of
[helm.git] / matita / matita / lib / arithmetics / sigma_pi.ma
1 (*
2     ||M||  This file is part of HELM, an Hypertextual, Electronic        
3     ||A||  Library of Mathematics, developed at the Computer Science     
4     ||T||  Department of the University of Bologna, Italy.                     
5     ||I||                                                                 
6     ||T||  
7     ||A||  This file is distributed under the terms of the 
8     \   /  GNU General Public License Version 2        
9      \ /      
10       V_______________________________________________________________ *)
11
12 include "arithmetics/primes.ma".
13 include "arithmetics/bigops.ma".
14
15 (* Sigma e Pi *)
16
17 notation "∑_{ ident i < n | p } f"
18   with precedence 80
19 for @{'bigop $n plus 0 (λ${ident i}. $p) (λ${ident i}. $f)}.
20
21 notation "∑_{ ident i < n } f"
22   with precedence 80
23 for @{'bigop $n plus 0 (λ${ident i}.true) (λ${ident i}. $f)}.
24
25 notation "∑_{ ident j ∈ [a,b[ } f"
26   with precedence 80
27 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
28   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
29   
30 notation "∑_{ ident j ∈ [a,b[ | p } f"
31   with precedence 80
32 for @{'bigop ($b-$a) plus 0 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
33   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
34  
35 notation "∏_{ ident i < n | p} f"
36   with precedence 80
37 for @{'bigop $n times 1 (λ${ident i}.$p) (λ${ident i}. $f)}.
38  
39 notation "∏_{ ident i < n } f"
40   with precedence 80
41 for @{'bigop $n times 1 (λ${ident i}.true) (λ${ident i}. $f)}.
42
43 notation "∏_{ ident j ∈ [a,b[ } f"
44   with precedence 80
45 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.true) (${ident j}+$a)))
46   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
47   
48 notation "∏_{ ident j ∈ [a,b[ | p } f"
49   with precedence 80
50 for @{'bigop ($b-$a) times 1 (λ${ident j}.((λ${ident j}.$p) (${ident j}+$a)))
51   (λ${ident j}.((λ${ident j}.$f)(${ident j}+$a)))}.
52
53 (* instances of associative and commutative operations *)
54
55 definition plusA ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) 
56    (λa,b,c.sym_eq ??? (associative_plus a b c)).
57    
58 definition plusAC ≝ mk_ACop nat 0 plusA commutative_plus.
59
60 definition timesA ≝ mk_Aop nat 1 times 
61    (λa.sym_eq ??? (plus_n_O a)) (λn.sym_eq ??? (times_n_1 n)) 
62    (λa,b,c.sym_eq ??? (associative_times a b c)).
63    
64 definition timesAC ≝ mk_ACop nat 1 timesA commutative_times.
65
66 definition natD ≝ mk_Dop nat 0 plusAC times (λn.(sym_eq ??? (times_n_O n))) 
67    distributive_times_plus.
68    
69 (********************************************************)
70
71 theorem sigma_const: ∀n:nat. ∑_{i<n} 1 = n.
72 #n elim n // #n1 >bigop_Strue //
73 qed.
74
75 (* monotonicity; these roperty should be expressed at a more
76 genral level *)
77
78 theorem le_sigma: 
79 ∀n:nat. ∀p1,p2:nat → bool. ∀g1,g2:nat → nat.
80 (∀i. i < n → p1 i = true → p2 i = true ) → 
81 (∀i. i < n → p1 i = true → g1 i ≤ g2 i ) → 
82  ∑_{i < n | p1 i} (g1 i) ≤ ∑_{i < n | p2 i} (g2 i).
83 #n #p1 #p2 #g1 #g2 elim n 
84   [#_ #_ @le_n
85   |#n1 #Hind #H1 #H2 
86    lapply (Hind ??)
87      [#j #ltin1 #Hgj @(H2 … Hgj) @le_S //
88      |#j #ltin1 #Hp1j @(H1 … Hp1j) @le_S //
89      ] -Hind #Hind
90    cases (true_or_false (p2 n1)) #Hp2
91     [>bigop_Strue in ⊢ (??%); [2:@Hp2] 
92      cases (true_or_false (p1 n1)) #Hp1
93       [>bigop_Strue [2:@Hp1] @(le_plus … Hind) @H2 // 
94       |>bigop_Sfalse [2:@Hp1] @le_plus_a // 
95       ]
96     |cut (p1 n1 = false) 
97       [cases (true_or_false (p1 n1)) #Hp1
98         [>(H1 … (le_n ?) Hp1) in Hp2; #H destruct (H) | //]
99       ] #Hp1
100      >bigop_Sfalse [2:@Hp1] >bigop_Sfalse [2:@Hp2] //
101     ]
102   ]
103 qed.
104
105 theorem lt_sigma_p: 
106 ∀n:nat. ∀p1,p2:nat → bool. ∀g1,g2:nat → nat.
107 (∀i. i < n → p1 i = true → p2 i = true) →
108 (∀i. i < n → p1 i = true → g1 i ≤ g2 i ) →
109 (∃i. i < n ∧ ((p1 i = true) ∧ (g1 i < g2 i)
110               ∨ (p1 i = false ∧ (p2 i = true) ∧ (0 < g2 i)))) →
111   ∑_{i < n | p1 i} (g1 i) < ∑_{i < n | p2 i} (g2 i).
112 #n #p1 #p2 #g1 #g2 #H1 #H2 * #k * #ltk * 
113   [* #p1k #gk 
114    lapply (H1 k ltk p1k) #p2k
115    >(bigop_diff p1 ?? plusAC … ltk p1k)
116    >(bigop_diff p2 ?? plusAC … ltk p2k) whd 
117    cut (∀a,b. S a + b = S(a +b)) [//] #Hplus <Hplus @le_plus
118     [@gk
119     |@le_sigma
120       [#i #ltin #H @true_to_andb_true 
121         [@(andb_true_l … H) | @(H1 i ltin) @(andb_true_r … H)]
122       |#i #ltin #H @(H2 i ltin) @(andb_true_r … H)
123       ]
124     ]
125   |* * #p1k #p2k #posg2
126    >(bigop_diff p2 ?? plusAC … ltk p2k) whd 
127    cut (∀a. S 0 + a = S a) [//] #H0 <(H0 (bigop n ?????)) @le_plus
128     [@posg2   
129     |@le_sigma
130       [#i #ltin #H @true_to_andb_true 
131         [cases (true_or_false (eqb k i)) #Hc >Hc
132           [normalize <H <p1k >(eqb_true_to_eq … Hc) //|//] 
133         |@(H1 i ltin) @H]
134       |#i #ltin #H @(H2 i ltin) @H
135       ]
136     ]
137 qed.
138  
139 theorem le_pi: 
140 ∀n.∀p:nat → bool.∀g1,g2:nat → nat. 
141   (∀i.i<n → p i = true → g1 i ≤ g2 i ) → 
142   ∏_{i < n | p i} (g1 i) ≤ ∏_{i < n | p i} (g2 i).
143 #n #p #g1 #g2 elim n 
144   [#_ @le_n
145   |#n1 #Hind #Hle cases (true_or_false (p n1)) #Hcase
146     [ >bigop_Strue // >bigop_Strue // @le_times
147       [@Hle // |@Hind #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]]
148     |>bigop_Sfalse // >bigop_Sfalse // @Hind
149      #i #lti #Hpi @Hle [@lt_to_le @le_S_S @lti|@Hpi]
150     ]
151   ]
152 qed.
153
154 theorem exp_sigma: ∀n,a,p. 
155   ∏_{i < n | p i} a = exp a (∑_{i < n | p i} 1).
156 #n #a #p elim n // #n1 cases (true_or_false (p n1)) #Hcase
157   [>bigop_Strue // >bigop_Strue // |>bigop_Sfalse // >bigop_Sfalse //] 
158 qed.
159
160 theorem times_pi: ∀n,p,f,g. 
161   ∏_{i<n|p i}(f i*g i) = ∏_{i<n|p i}(f i) * ∏_{i<n|p i}(g i). 
162 #n #p #f #g elim n // #n1 cases (true_or_false (p n1)) #Hcase #Hind
163   [>bigop_Strue // >bigop_Strue // >bigop_Strue //
164   |>bigop_Sfalse // >bigop_Sfalse // >bigop_Sfalse //
165   ]
166 qed.
167
168 theorem pi_1: ∀n,p. 
169   ∏_{i < n | p i} 1 = 1.
170 #n #p elim n // #n1 #Hind cases (true_or_false (p n1)) #Hc 
171   [>bigop_Strue >Hind // |>bigop_Sfalse // ]
172 qed.
173
174 theorem exp_pi: ∀n,m,p,f. 
175   ∏_{i < n | p i}(exp (f i) m) = exp (∏_{i < n | p i}(f i)) m.
176 #n #m #p #f elim m
177   [@pi_1
178   |#m1 #Hind >times_pi >Hind %
179   ]
180 qed.
181
182 theorem exp_sigma_l: ∀n,a,p,f. 
183   ∏_{i < n | p i} (exp a (f i)) = exp a (∑_{i < n | p i}(f i)).
184 #n #a #p #f elim n // #i #Hind cases (true_or_false (p i)) #Hc
185   [>bigop_Strue [>bigop_Strue [>Hind >exp_plus_times // |//] |//]
186   |>bigop_Sfalse [>bigop_Sfalse [@Hind|//] | //]
187   ]
188 qed.