X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fbinomial.ma;h=c3834c8d847b8d001f48ef19217b9d121e1a2944;hb=b08fbe87149ae7c2e14dfd7485dbf50d6e7dbfe6;hp=414b71a15585a32a99aad910857013ace38725f0;hpb=53452958508001e7af3090695b619fe92135fb9e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma
index 414b71a15..c3834c8d8 100644
--- a/matita/matita/lib/arithmetics/binomial.ma
+++ b/matita/matita/lib/arithmetics/binomial.ma
@@ -9,8 +9,8 @@
      \ /      
       V_______________________________________________________________ *)
 
-include "arithmetics/bigops.ma".
 include "arithmetics/primes.ma".
+include "arithmetics/sigma_pi.ma".
 
 (* binomial coefficient *)
 definition bc ≝ λn,k. n!/(k!*(n-k)!).
@@ -23,14 +23,14 @@ theorem bc_n_n: ∀n. bc n n = 1.
 qed.
 
 theorem bc_n_O: ∀n. bc n O = 1.
-#n >bceq <minus_n_O /2/
+#n >bceq <minus_n_O /2 by injective_plus_r/
 qed.
 
 theorem fact_minus: ∀n,k. k < n → 
-  (n-k)*(n - S k)! = (n - k)!.
+  (n - S k)!*(n-k) = (n - k)!.
 #n #k (cases n)
   [#ltO @False_ind /2/
-  |#l #ltl >minus_Sn_m [>commutative_times //|@le_S_S_to_le //]
+  |#l #ltl >(minus_Sn_m k) [// |@le_S_S_to_le //]
   ]
 qed.
 
@@ -38,208 +38,156 @@ theorem bc2 : ∀n.
 ∀k. k ≤n → k!*(n-k)! ∣ n!.
 #n (elim n) 
   [#k #lek0 <(le_n_O_to_eq ? lek0) //
-  |#m #Hind #k generalize in match H1;cases k
-     [intro;simplify in ⊢ (? (? ? (? %)) ?);simplify in ⊢ (? (? % ?) ?);
-      rewrite > sym_times;rewrite < times_n_SO;apply reflexive_divides
-     |intro;elim (decidable_eq_nat n2 n1)
-        [rewrite > H3;rewrite < minus_n_n;
-         rewrite > times_n_SO in ⊢ (? ? %);apply reflexive_divides
-        |lapply (H n2)
-           [lapply (H (n1 - (S n2)))
-              [change in ⊢ (? ? %) with ((S n1)*n1!);
-               rewrite > (plus_minus_m_m n1 n2) in ⊢ (? ? (? (? %) ?))
-                 [rewrite > sym_plus;
-                  change in ⊢ (? ? (? % ?)) with ((S n2) + (n1 - n2));
-                  rewrite > sym_times in \vdash (? ? %);
-                  rewrite > distr_times_plus in ⊢ (? ? %);
-                  simplify in ⊢ (? (? ? (? %)) ?);
-                  apply divides_plus
-                    [rewrite > sym_times;
-                     change in ⊢ (? (? ? %) ?) with ((S n2)*n2!);
-                     rewrite > sym_times in ⊢ (? (? ? %) ?);
-                     rewrite < assoc_times;
-                     apply divides_times
-                       [rewrite > sym_times;assumption
-                       |apply reflexive_divides]
-                    |rewrite < fact_minus in ⊢ (? (? ? %) ?)
-                       [rewrite > sym_times in ⊢ (? (? ? %) ?);
-                        rewrite < assoc_times;
-                        apply divides_times
-                          [rewrite < eq_plus_minus_minus_minus in Hletin1;
-                             [rewrite > sym_times;rewrite < minus_n_n in Hletin1;
-                              rewrite < plus_n_O in Hletin1;assumption
-                             |lapply (le_S_S_to_le ? ? H2);
-                              elim (le_to_or_lt_eq ? ? Hletin2);
-                                [assumption
-                                |elim (H3 H4)]
-                             |constructor 1]
-                          |apply reflexive_divides]
-                       |lapply (le_S_S_to_le ? ? H2);
-                        elim (le_to_or_lt_eq ? ? Hletin2);
-                          [assumption
-                          |elim (H3 H4)]]]
-                 |apply le_S_S_to_le;assumption]
-              |apply le_minus_m;apply le_S_S_to_le;assumption]
-           |apply le_S_S_to_le;assumption]]]]
-qed.                      
-    
-theorem bc1: \forall n.\forall k. k < n \to bc (S n) (S k) = (bc n k) + (bc n (S k)). 
-intros.unfold bc.
-rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
-  [rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)). 
-   rewrite < assoc_times in ⊢ (? ? ? (? (? ? %) ?)).
-   rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (n - k)) in ⊢ (? ? ? (? ? %))
-    [rewrite > assoc_times in ⊢ (? ? ? (? ? (? ? %))).
-     rewrite > sym_times in ⊢ (? ? ? (? ? (? ? (? ? %)))).
-     rewrite > fact_minus
-      [rewrite < eq_div_plus
-        [rewrite < distr_times_plus.
-         simplify in ⊢ (? ? ? (? (? ? %) ?)).
-         rewrite > sym_plus in ⊢ (? ? ? (? (? ? (? %)) ?)).
-         rewrite < plus_minus_m_m
-          [rewrite > sym_times in ⊢ (? ? ? (? % ?)).
-           reflexivity
-          |apply lt_to_le.
-           assumption
-          ]
-        |rewrite > (times_n_O O).
-         apply lt_times;apply lt_O_fact
-        |change in ⊢ (? (? % ?) ?) with ((S k)*k!);
-         rewrite < sym_times in ⊢ (? ? %);
-         rewrite > assoc_times;apply divides_times
-           [apply reflexive_divides
-           |apply bc2;apply le_S_S_to_le;constructor 2;assumption]
-        |rewrite < fact_minus
-           [rewrite > sym_times in ⊢ (? (? ? %) ?);rewrite < assoc_times;
-            apply divides_times
-              [apply bc2;assumption
-              |apply reflexive_divides]
-           |assumption]]
-     |assumption]
-  |apply lt_to_lt_O_minus;assumption
-  |rewrite > (times_n_O O).
-   apply lt_times;apply lt_O_fact]
-|apply lt_O_S
-|rewrite > (times_n_O O).
- apply lt_times;apply lt_O_fact]
-qed.
-
-theorem lt_O_bc: \forall n,m. m \le n \to O < bc n m.
-intro.elim n
-  [apply (le_n_O_elim ? H).
-   simplify.apply le_n
-  |elim (le_to_or_lt_eq ? ? H1)
-    [generalize in match H2.cases m;intro
-      [rewrite > bc_n_O.apply le_n
-      |rewrite > bc1
-        [apply (trans_le ? (bc n1 n2))
-          [apply H.apply le_S_S_to_le.apply lt_to_le.assumption
-          |apply le_plus_n_r
-          ]
-        |apply le_S_S_to_le.assumption
-        ]
+  |#m #Hind #k (cases k) normalize //
+     #c #lec cases (le_to_or_lt_eq … (le_S_S_to_le …lec))
+    [#ltcm 
+     cut (m-(m-(S c)) = S c) [@plus_to_minus @plus_minus_m_m //] #eqSc     
+     lapply (Hind c (le_S_S_to_le … lec)) #Hc
+     lapply (Hind (m - (S c)) ?) [@le_plus_to_minus //] >eqSc #Hmc
+     >(plus_minus_m_m m c) in ⊢ (??(??(?%))); [|@le_S_S_to_le //]
+     >commutative_plus >(distributive_times_plus ? (S c))
+     @divides_plus
+      [>associative_times >(commutative_times (S c))
+       <associative_times @divides_times //
+      |<(fact_minus …ltcm) in ⊢ (?(??%)?);
+       <associative_times @divides_times //
+       >commutative_times @Hmc
       ]
-    |rewrite > H2.
-     rewrite > bc_n_n.
-     apply le_n
+    |#eqcm >eqcm <minus_n_n <times_n_1 // 
     ]
   ]
 qed.
-
-theorem exp_plus_sigma_p:\forall a,b,n.
-exp (a+b) n = sigma_p (S n) (\lambda k.true) 
-  (\lambda k.(bc n k)*(exp a (n-k))*(exp b k)).
-intros.elim n
-  [simplify.reflexivity
-  |simplify in ⊢ (? ? % ?).
-   rewrite > true_to_sigma_p_Sn
-    [rewrite > H;rewrite > sym_times in ⊢ (? ? % ?);
-     rewrite > distr_times_plus in ⊢ (? ? % ?);
-     rewrite < minus_n_n in ⊢ (? ? ? (? (? (? ? (? ? %)) ?) ?));
-     rewrite > sym_times in ⊢ (? ? (? % ?) ?);
-     rewrite > sym_times in ⊢ (? ? (? ? %) ?);
-     rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? % ?) ?);
-     rewrite > distributive_times_plus_sigma_p in ⊢ (? ? (? ? %) ?);
-     rewrite > true_to_sigma_p_Sn in ⊢ (? ? (? ? %) ?)
-       [rewrite < assoc_plus;rewrite < sym_plus in ⊢ (? ? (? % ?) ?);
-        rewrite > assoc_plus;
-        apply eq_f2
-          [rewrite > sym_times;rewrite > assoc_times;autobatch paramodulation
-          |rewrite > (sigma_p_gi ? ? O);
-            [rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in ⊢ (? ? (? (? ? %) ?) ?)
-               [rewrite > (sigma_p_gi ? ? O) in ⊢ (? ? ? %);
-                  [rewrite > assoc_plus;apply eq_f2
-                     [autobatch paramodulation; 
-                     |rewrite < sigma_p_plus_1;
-                      rewrite < (eq_sigma_p_gh ? S pred n1 (S n1) (λx:nat.true)) in \vdash (? ? ? %);
-                        [apply eq_sigma_p
-                           [intros;reflexivity
-                           |intros;rewrite > sym_times;rewrite > assoc_times;
-                            rewrite > sym_times in ⊢ (? ? (? (? ? %) ?) ?);
-                            rewrite > assoc_times;rewrite < assoc_times in ⊢ (? ? (? (? ? %) ?) ?);
-                            rewrite > sym_times in ⊢ (? ? (? (? ? (? % ?)) ?) ?);
-                            change in ⊢ (? ? (? (? ? (? % ?)) ?) ?) with (exp a (S (n1 - S x)));
-                            rewrite < (minus_Sn_m ? ? H1);rewrite > minus_S_S;
-                            rewrite > sym_times in \vdash (? ? (? ? %) ?);
-                            rewrite > assoc_times; 
-                            rewrite > sym_times in ⊢ (? ? (? ? (? ? %)) ?);
-                            change in \vdash (? ? (? ? (? ? %)) ?) with (exp b (S x));
-                            rewrite > assoc_times in \vdash (? ? (? ? %) ?);
-                            rewrite > sym_times in \vdash (? ? (? % ?) ?);
-                            rewrite > sym_times in \vdash (? ? (? ? %) ?);
-                            rewrite > assoc_times in \vdash (? ? ? %);
-                            rewrite > sym_times in \vdash (? ? ? %);
-                            rewrite < distr_times_plus;
-                            rewrite > sym_plus;rewrite < bc1;
-                              [reflexivity|assumption]]
-                        |intros;simplify;reflexivity
-                        |intros;simplify;reflexivity
-                        |intros;apply le_S_S;assumption
-                        |intros;reflexivity
-                        |intros 2;elim j
-                            [simplify in H2;destruct H2
-                            |simplify;reflexivity]
-                        |intro;elim j
-                            [simplify in H2;destruct H2
-                            |simplify;apply le_S_S_to_le;assumption]]]
-                  |apply le_S_S;apply le_O_n
-                  |reflexivity]
-               |intros;simplify;reflexivity
-               |intros;simplify;reflexivity
-               |intros;apply le_S_S;assumption
-               |intros;reflexivity
-               |intros 2;elim j
-                  [simplify in H2;destruct H2
-                  |simplify;reflexivity]
-               |intro;elim j
-                  [simplify in H2;destruct H2
-                  |simplify;apply le_S_S_to_le;assumption]]
-            |apply le_S_S;apply le_O_n
-            |reflexivity]]
-      |reflexivity]
-   |reflexivity]]
+           
+theorem bc1: ∀n.∀k. k < n → 
+  bc (S n) (S k) = (bc n k) + (bc n (S k)).
+#n #k #ltkn > bceq >(bceq n) >(bceq n (S k))
+>(div_times_times ?? (S k)) in ⊢ (???(?%?));
+  [|>(times_n_O 0) @lt_times // | //]
+>associative_times in ⊢ (???(?(??%)?));
+>commutative_times in ⊢ (???(?(??(??%))?));
+<associative_times in ⊢ (???(?(??%)?));
+>(div_times_times ?? (n - k)) in ⊢ (???(??%)) ; 
+  [|>(times_n_O 0) @lt_times // 
+   |@(le_plus_to_le_r k ??) <plus_minus_m_m /2 by lt_to_le/]
+>associative_times in ⊢ (???(??(??%)));
+>fact_minus // <plus_div 
+  [<distributive_times_plus
+   >commutative_plus in ⊢ (???%); <plus_n_Sm <plus_minus_m_m [|/2 by lt_to_le/] @refl
+  |<fact_minus // <associative_times @divides_times // @(bc2 n (S k)) //
+  |>associative_times >(commutative_times (S k))
+   <associative_times @divides_times // @bc2 /2 by lt_to_le/
+  |>(times_n_O 0) @lt_times [@(le_1_fact (S k)) | //]
+  ]
 qed.
 
-theorem exp_S_sigma_p:\forall a,n.
-exp (S a) n = sigma_p (S n) (\lambda k.true) (\lambda k.(bc n k)*(exp a (n-k))).
-intros.
-rewrite > plus_n_SO.
-rewrite > exp_plus_sigma_p.
-apply eq_sigma_p;intros
-  [reflexivity
-  |rewrite < exp_SO_n.
-   rewrite < times_n_SO.
-   reflexivity
+theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m.
+#n (elim n) 
+  [#m #lemO @(le_n_O_elim ? lemO) //
+  |-n #n #Hind #m (cases m) //
+   #m #lemn cases(le_to_or_lt_eq … (le_S_S_to_le …lemn)) //
+   #ltmn >bc1 // >(plus_O_n 0) @lt_plus @Hind /2/
   ]
-qed.
+qed. 
 
-theorem exp_Sn_SSO: \forall n. exp (S n) 2 = S((exp n 2) + 2*n).
-intros.simplify.
-rewrite < times_n_SO.
-rewrite < plus_n_O.
-rewrite < sym_times.simplify.
-rewrite < assoc_plus.
-rewrite < sym_plus.
-reflexivity.
+theorem binomial_law:∀a,b,n.
+  (a+b)^n = ∑_{k < S n}((bc n k)*(a^(n-k))*(b^k)).
+#a #b #n (elim n) //
+-n #n #Hind normalize in ⊢ (??%?); >commutative_times
+>bigop_Strue // >Hind >distributive_times_plus_r
+<(minus_n_n (S n)) (* <commutative_times <(commutative_times b) *)
+(* da capire *)
+>(bigop_distr ??? 0 (mk_Dop ℕ O plusAC times (λn0:ℕ.sym_eq ℕ O (n0*O) (times_n_O n0))
+    distributive_times_plus) ? a) 
+>(bigop_distr ???? (mk_Dop ℕ O plusAC times (λn0:ℕ.sym_eq ℕ O (n0*O) (times_n_O n0))
+    distributive_times_plus) ? b)
+>bigop_Strue in ⊢ (??(??%)?); // <associative_plus 
+<commutative_plus in ⊢ (??(? % ?) ?); >associative_plus @eq_f2
+  [<minus_n_n >bc_n_n >bc_n_n normalize //
+  |>bigop_0 >associative_plus >commutative_plus in ⊢ (??(??%)?);
+   <associative_plus >(bigop_0 n ?? plusA) @eq_f2 
+    [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus >Hplus 
+     >(bigop_op n ??? plusAC) @same_bigop //
+     #i #ltin #_ <associative_times >(commutative_times b)
+     >(associative_times ?? b) <Hplus <(distributive_times_plus_r (b^(S i)))
+     @eq_f2 // <associative_times >(commutative_times a) 
+     >associative_times cut(∀n.a*a^n = a^(S n)) [#n @commutative_times] #H
+     >H <minus_Sn_m // <(distributive_times_plus_r (a^(n-i)))
+     @eq_f2 // @sym_eq >commutative_plus @bc1 //
+    |>bc_n_O >bc_n_O normalize // 
+    ]
+  ]
+qed.
+     
+theorem exp_S_sigma_p:∀a,n.
+  (S a)^n = ∑_{k < S n}((bc n k)*a^(n-k)).
+#a #n cut (S a = a + 1) // #H >H
+>binomial_law @same_bigop //
 qed.
 
+(************ mid value *************)
+lemma eqb_sym: ∀a,b. eqb a b = eqb b a.
+#a #b cases (true_or_false (eqb a b)) #Hab
+  [>(eqb_true_to_eq … Hab) // 
+  |>Hab @sym_eq @not_eq_to_eqb_false 
+   @(not_to_not … (eqb_false_to_not_eq … Hab)) //
+  ] 
+qed-.
+
+definition M ≝ λm.bc (S(2*m)) m.
+
+lemma Mdef : ∀m. M m = bc (S(2*m)) m. 
+// qed.
+
+theorem lt_M: ∀m. O < m → M m < exp 2 (2*m).
+#m #posm  @(lt_times_n_to_lt_l 2)
+cut (∀a,b. a^(S b) = a^b*a) [//] #expS <expS  
+cut (2 = 1+1) [//] #H2 >H2 in ⊢ (??(?%?));
+>binomial_law 
+@(le_to_lt_to_lt ? 
+  (∑_{k < S (S (2*m)) | orb (eqb k m) (eqb k (S m))}
+         (bc (S (2*m)) k*1^(S (2*m)-k)*1^k)))
+  [>(bigop_diff ??? plusAC … m)
+    [>(bigop_diff ??? plusAC … (S m))
+      [<(pad_bigop1 … (S(S(2*m))) 0)
+        [cut (∀a,b. plus a b = plusAC a b) [//] #Hplus <Hplus <Hplus
+         whd in ⊢ (? ? (? ? (? ? %)));
+         cut (∀a. 2*a = a + a) [//] #H2a >commutative_times >H2a
+         <exp_1_n <exp_1_n <exp_1_n <exp_1_n
+         <times_n_1 <times_n_1 <times_n_1 <times_n_1 
+         @le_plus
+          [@le_n
+          |>Mdef <plus_n_O >bceq >bceq 
+           cut (∀a,b.S a - (S b) = a -b) [//] #Hminus >Hminus 
+           normalize in ⊢ (??(??(??(?(?%?))))); <plus_n_O <minus_plus_m_m
+           <commutative_times in ⊢ (??(??%)); 
+           cut (S (2*m)-m = S m) 
+            [>H2a >plus_n_Sm >commutative_plus <minus_plus_m_m //] 
+           #Hcut >Hcut //
+          ]
+        |#i #_ #_ >(eqb_sym i m) >(eqb_sym i (S m))
+         cases (eqb m i) cases (eqb (S m) i) //
+        |@le_O_n
+        ]
+      |>(eqb_sym (S m) m) >(eq_to_eqb_true ? ? (refl ? (S m)))
+       >(not_eq_to_eqb_false m (S m)) 
+        [// |@(not_to_not … (not_eq_n_Sn m)) //]
+      |@le_S_S @le_S_S // 
+      ]
+    |>(eq_to_eqb_true ?? (refl ? m)) //
+    |@le_S @le_S_S //
+    ]
+  |@lt_sigma_p
+    [//
+    |#i #lti #Hi @le_n
+    |%{0} %
+      [@lt_O_S
+      |%2 % 
+        [% // >(not_eq_to_eqb_false 0 (S m)) //
+         >(not_eq_to_eqb_false 0 m) // @lt_to_not_eq //
+        |>bc_n_O <exp_1_n <exp_1_n @le_n
+        ]
+      ]
+    ]
+  ]
+qed.
+