From: Wilmer Ricciotti 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