From 2983f88c7fedc8973e1104322fa884fb6b3cfb30 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 16 Nov 2011 17:50:21 +0000 Subject: [PATCH] Non working parts of the library commented out. --- matita/matita/lib/arithmetics/bigops.ma | 2 +- matita/matita/lib/arithmetics/binomial.ma | 3 ++- matita/matita/lib/arithmetics/nth_prime.ma | 3 ++- matita/matita/lib/arithmetics/sigma_pi.ma | 3 ++- 4 files changed, 7 insertions(+), 4 deletions(-) diff --git a/matita/matita/lib/arithmetics/bigops.ma b/matita/matita/lib/arithmetics/bigops.ma index 6bcd62a65..d6b462b10 100644 --- a/matita/matita/lib/arithmetics/bigops.ma +++ b/matita/matita/lib/arithmetics/bigops.ma @@ -174,7 +174,7 @@ theorem bigop_prod: ∀k1,k2,p1,p2,B.∀nil.∀op:Aop B nil.∀f: nat →nat → [>bigop_Strue // >Hind >bigop_sum @same_bigop #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ #eqi [|#H] (>eqi in ⊢ (???%)) - >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ + >div_plus_times /2/ >Hp1 >(mod_plus_times …) /2/ normalize // |>bigop_Sfalse // >Hind >(pad_bigop (S n*k2)) // @same_bigop #i #lti @leb_elim // #lei cut (i = n*k2+(i-n*k2)) /2/ #eqi >eqi in ⊢ (???%) >div_plus_times /2/ diff --git a/matita/matita/lib/arithmetics/binomial.ma b/matita/matita/lib/arithmetics/binomial.ma index 9397f7b4d..c31e15d11 100644 --- a/matita/matita/lib/arithmetics/binomial.ma +++ b/matita/matita/lib/arithmetics/binomial.ma @@ -89,6 +89,7 @@ theorem lt_O_bc: ∀n,m. m ≤ n → O < bc n m. ] qed. +(* 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) // @@ -130,4 +131,4 @@ rewrite < assoc_plus. rewrite < sym_plus. reflexivity. qed. *) - +*) \ No newline at end of file diff --git a/matita/matita/lib/arithmetics/nth_prime.ma b/matita/matita/lib/arithmetics/nth_prime.ma index 7b7c70bfe..c973d0b12 100644 --- a/matita/matita/lib/arithmetics/nth_prime.ma +++ b/matita/matita/lib/arithmetics/nth_prime.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +(* To be ported include "nat/primes.ma". include "nat/lt_arith.ma". @@ -198,4 +199,4 @@ apply le_to_or_lt_eq.assumption. apply ex_m_le_n_nth_prime_m. simplify.unfold prime in H.elim H.assumption. qed. - +*) \ No newline at end of file diff --git a/matita/matita/lib/arithmetics/sigma_pi.ma b/matita/matita/lib/arithmetics/sigma_pi.ma index d92d525b7..94b3794b3 100644 --- a/matita/matita/lib/arithmetics/sigma_pi.ma +++ b/matita/matita/lib/arithmetics/sigma_pi.ma @@ -9,6 +9,7 @@ \ / V_______________________________________________________________ *) +(* To be ported include "arithmetics/bigops.ma". definition natAop ≝ mk_Aop nat 0 plus (λa.refl ? a) (λn.sym_eq ??? (plus_n_O n)) @@ -744,4 +745,4 @@ apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y |assumption ] ] -qed. *) \ No newline at end of file +qed. *)*) \ No newline at end of file -- 2.39.2