From: Wilmer Ricciotti <ricciott@cs.unibo.it>
Date: Sun, 9 Dec 2007 23:28:01 +0000 (+0000)
Subject: Added summation formula for the power of a binomial.
X-Git-Tag: make_still_working~5717
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=892992b24f5476c2b4eed13f64e04854ef919020;p=helm.git

Added summation formula for the power of a binomial.
---

diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma
index e1b955fa8..4434f769b 100644
--- a/helm/software/matita/library/nat/binomial.ma
+++ b/helm/software/matita/library/nat/binomial.ma
@@ -51,10 +51,56 @@ intros 2.cases n
   ]
 qed.
 
-theorem bc1: \forall n.
-(\forall i. i < n \to divides (i!*(n-i)!) n!) \to
-\forall k. k < n \to 
-bc (S n) (S k) = (bc n k) + (bc n (S k)). 
+theorem bc2 : \forall n.
+\forall k. k \leq n \to divides (k!*(n-k)!) n!.
+intro;elim n
+  [rewrite < (le_n_O_to_eq ? H);apply reflexive_divides
+  |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 ⊢ (? ? ? (? (? ? %) ?)). 
@@ -75,9 +121,26 @@ rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
           ]
         |rewrite > (times_n_O O).
          apply lt_times;apply lt_O_fact
-        |apply H.
-    
-    
+        |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 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)).
@@ -85,4 +148,69 @@ intros.elim n
   [simplify.reflexivity
   |simplify in ⊢ (? ? % ?).
    rewrite > true_to_sigma_p_Sn
-    [rewrite <
\ No newline at end of file
+    [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]]
+qed.
\ No newline at end of file