progress.

diff --git a/helm/software/matita/library/nat/binomial.ma b/helm/software/matita/library/nat/binomial.ma
index 9505761488e3dd9568d51036ff877471c21215de..1a341032032b95c317863801601446727cbd983a 100644 (file)
--- a/helm/software/matita/library/nat/binomial.ma
+++ b/helm/software/matita/library/nat/binomial.ma
@@ -141,6 +141,28 @@ rewrite > (lt_to_lt_to_eq_div_div_times_times ? ? (S k)) in ⊢ (? ? ? (? % ?))
  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
+        ]
+      ]
+    |rewrite > H2.
+     rewrite > bc_n_n.
+     apply le_n
+    ]
+  ]
+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)).

diff --git a/helm/software/matita/library/nat/chebyshev_teta.ma b/helm/software/matita/library/nat/chebyshev_teta.ma
index bb0f4e83890fedea76358b20ec35e035072b5c33..bdec363910b2fe1a099607cb67183468fd4a4abb 100644 (file)
--- a/helm/software/matita/library/nat/chebyshev_teta.ma
+++ b/helm/software/matita/library/nat/chebyshev_teta.ma
@@ -22,7 +22,24 @@ include "nat/pi_p.ma".
 definition teta: nat \to nat \def
 \lambda n. pi_p (S n) primeb (\lambda p.p).
 
-definition M \def \lambda m.bc (2*m+1) m.
+theorem lt_O_teta: \forall n. O < teta n.
+intros.elim n
+  [apply le_n
+  |unfold teta.apply (bool_elim ? (primeb (S n1)));intro 
+    [rewrite > true_to_pi_p_Sn
+      [rewrite > (times_n_O O).
+       apply lt_times
+        [apply lt_O_S
+        |assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_pi_p_Sn;assumption
+    ]
+  ]
+qed.
+
+definition M \def \lambda m.bc (S(2*m)) m.
 
 theorem lt_M: \forall m. O < m \to M m < exp 2 (2*m).
 intros.
@@ -43,8 +60,8 @@ apply (lt_times_to_lt 2)
            rewrite < times_n_SO.rewrite < times_n_SO.
            rewrite < times_n_SO.rewrite < times_n_SO.
            apply le_plus
-            [unfold M.rewrite < plus_n_SO.apply le_n
-            |apply le_plus_l.unfold M.rewrite < plus_n_SO.
+            [unfold M.apply le_n
+            |apply le_plus_l.unfold M.
              change in \vdash (? ? %) with (fact (S(2*m))/(fact (S m)*(fact ((2*m)-m)))).
              simplify in \vdash (? ? (? ? (? ? (? (? % ?))))).
              rewrite < plus_n_O.rewrite < minus_plus_m_m.
@@ -95,10 +112,291 @@ apply (lt_times_to_lt 2)
           ]
         ]
       |intros.rewrite > sym_times in \vdash (? ? ? %).
-       
+       rewrite < times_n_SO.
+       reflexivity
+      ]
+    ]
+  ]
+qed.
       
-         
-             simplify in \vdash (? ? %).
+theorem divides_fact_to_divides: \forall p,n. prime p \to divides p n! \to 
+\exists m.O < m \land m \le n \land divides p m.  
+intros 3.elim n
+  [apply False_ind.elim H.
+   apply (lt_to_not_le ? ? H2).
+   apply divides_to_le[apply le_n|assumption]
+  |rewrite > factS in H2.
+   elim (divides_times_to_divides ? ? ? H H2)
+    [apply (ex_intro ? ? (S n1)).split
+      [split
+        [apply lt_O_S
+        |apply le_n
+        ]
+      |assumption
+      ]
+    |elim (H1 H3).elim H4.elim H5.
+     apply (ex_intro ? ? a).split
+      [split
+        [assumption
+        |apply le_S.assumption
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+      
+theorem divides_fact_to_le: \forall p,n. prime p \to divides p n! \to 
+p \le n.  
+intros.
+elim (divides_fact_to_divides p n H H1).
+elim H2.elim H3.
+apply (trans_le ? a)
+  [apply divides_to_le;assumption
+  |assumption
+  ]
+qed.
+     
+theorem prime_to_divides_M: \forall m,p. prime p \to S m < p \to p \le S(2*m) \to
+divides p (M m).      
+intros.unfold M.
+elim (bc2 (S(2*m)) m)
+  [unfold bc.rewrite > H3.
+   rewrite > sym_times.
+   rewrite > lt_O_to_div_times
+    [elim (divides_times_to_divides p (m!*(S (2*m)-m)!) n2)
+      [apply False_ind.
+       elim (divides_times_to_divides p (m!) (S (2*m)-m)!)
+        [apply (lt_to_not_le ? ? (lt_to_le ? ? H1)).
+         apply divides_fact_to_le;assumption
+        |apply (lt_to_not_le ? ? H1).
+         apply divides_fact_to_le
+          [assumption
+          |cut (S m = S(2*m)-m)
+            [rewrite > Hcut.assumption
+            |simplify in ⊢ (? ? ? (? (? %) ?)).
+             rewrite < plus_n_O.
+             change in ⊢ (? ? ? (? % ?)) with (S m + m).
+             apply minus_plus_m_m
+            ]
+          ]
+        |assumption
+        |assumption
+        ]
+      |assumption
+      |assumption
+      |rewrite < H3.
+       apply divides_fact
+        [apply prime_to_lt_O.assumption
+        |assumption
+        ]
+      ]
+    |rewrite > (times_n_O O).
+     apply lt_times;apply lt_O_fact
+    ]
+  |simplify in ⊢ (? ? (? %)).
+   rewrite < plus_n_O.
+   change in ⊢ (? ? %) with (S m + m).
+   apply le_plus_n
+  ]
+qed.
              
+theorem divides_pi_p_M1: \forall m.\forall i. i \le (S(S(2*m))) \to 
+divides (pi_p i (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m).
+intros 2.
+elim i
+  [simplify.apply (witness ? ? (M m)).rewrite > sym_times.apply times_n_SO
+  |apply (bool_elim ? (leb (S (S m)) n \land primeb n));intro
+    [rewrite > true_to_pi_p_Sn
+      [apply divides_to_divides_times
+        [apply primeb_true_to_prime.
+         apply (andb_true_true_r ? ? H2).
+        |cut (\forall p.prime p \to n \le p \to ¬p∣pi_p n (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p))
+          [apply Hcut
+            [apply primeb_true_to_prime.
+             apply (andb_true_true_r ? ? H2)
+            |apply le_n
+            ]
+          |intros 2.
+           elim n
+            [simplify.intro.elim H3.apply (lt_to_not_le ? ? H6).
+             apply divides_to_le
+              [apply le_n
+              |assumption
+              ]
+            |apply (bool_elim ? (leb (S (S m)) n1∧primeb n1));intro
+              [rewrite > true_to_pi_p_Sn
+                [intro.elim (divides_times_to_divides ? ? ? H3 H7)
+                  [apply (le_to_not_lt ? ? H5).
+                   apply le_S_S.
+                   apply divides_to_le
+                    [apply prime_to_lt_O.
+                     apply primeb_true_to_prime.
+                     apply (andb_true_true_r ? ? H6)
+                    |assumption
+                    ]
+                  |apply H4
+                    [apply lt_to_le.assumption
+                    |assumption
+                    ]
+                  ]
+                |assumption
+                ]
+              |rewrite > false_to_pi_p_Sn
+                [apply H4.
+                 apply lt_to_le.assumption
+                |assumption
+                ]
+              ]
+            ]
+          ]
+        |apply prime_to_divides_M
+          [apply primeb_true_to_prime.
+           apply (andb_true_true_r ? ? H2)
+          |apply leb_true_to_le.
+           apply (andb_true_true ? ? H2)
+          |apply le_S_S_to_le.assumption
+          ]
+        |apply H.
+         apply lt_to_le.
+         assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_pi_p_Sn
+      [apply H.
+       apply lt_to_le.
+       assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
 
+theorem divides_pi_p_M:\forall m.
+divides (pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p)) (M m).
+intros. 
+apply divides_pi_p_M1.
+apply le_n.
+qed.  
 
+theorem teta_pi_p_teta: \forall m. teta (S (2*m))
+=pi_p (S (S (2*m))) (λp:nat.leb (S (S m)) p∧primeb p) (λp:nat.p)*teta (S m).
+intro.unfold teta.
+rewrite > (eq_pi_p1 ? (\lambda p.leb p (S m) \land primeb p) ? (\lambda p.p) (S(S m)))
+  [rewrite < (false_to_eq_pi_p (S(S m)) (S(S(2*m))))
+    [generalize in match (S(S(2*m))).intro.
+     elim n
+      [simplify.reflexivity
+      |apply (bool_elim ? (primeb n1));intro
+        [rewrite > true_to_pi_p_Sn
+          [apply (bool_elim ? (leb n1 (S m))); intro
+            [rewrite > false_to_pi_p_Sn
+              [rewrite > true_to_pi_p_Sn
+                [rewrite < assoc_times.
+                 rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+                 rewrite > assoc_times.
+                 apply eq_f.
+                 assumption
+                |apply true_to_true_to_andb_true;assumption
+                ]
+              |rewrite > lt_to_leb_false
+                [reflexivity
+                |apply le_S_S.
+                 apply leb_true_to_le.
+                 assumption
+                ]
+              ]
+            |rewrite > true_to_pi_p_Sn
+              [rewrite > false_to_pi_p_Sn
+                [rewrite > assoc_times.
+                 apply eq_f.
+                 assumption
+                |rewrite > H2.reflexivity
+                ]
+              |rewrite > H1.
+               rewrite > le_to_leb_true
+                [reflexivity
+                |apply not_le_to_lt.
+                 apply leb_false_to_not_le.
+                 assumption
+                ]
+              ]
+            ]
+          |assumption 
+          ]
+        |rewrite > false_to_pi_p_Sn
+          [rewrite > false_to_pi_p_Sn
+            [rewrite > false_to_pi_p_Sn
+              [assumption
+              |rewrite > H1.
+               rewrite > andb_sym.
+               reflexivity
+              ]
+            |rewrite > H1.
+             rewrite > andb_sym.
+             reflexivity
+            ]
+          |assumption
+          ]
+        ]
+      ]
+    |apply le_S_S.apply le_S_S.
+     apply le_times_n.
+     apply le_n_Sn
+    |intros.
+     rewrite > lt_to_leb_false
+      [reflexivity
+      |assumption
+      ]
+    ]
+  |intros.
+   rewrite > le_to_leb_true
+    [reflexivity
+    |apply le_S_S_to_le.
+     assumption
+    ]
+  |intros.reflexivity
+  ]
+qed.                  
+
+theorem div_teta_teta: \forall m. 
+teta (S(2*m))/teta (S m) = pi_p (S(S(2*m))) (\lambda p.leb (S(S m)) p \land primeb p)(\lambda p.p).
+intros.apply (div_mod_spec_to_eq ? ? ? ? ? O (div_mod_spec_div_mod ? ? ? ))
+  [apply lt_O_teta
+  |apply div_mod_spec_intro
+    [apply lt_O_teta
+    |rewrite < plus_n_O.
+     apply teta_pi_p_teta
+    ]
+  ]
+qed.
+                     
+theorem le_teta_M_teta: \forall m. 
+teta (S(2*m)) \le (M m)*teta (S m).  
+intro.
+rewrite > teta_pi_p_teta. 
+apply le_times_l.
+apply divides_to_le
+  [unfold M.apply lt_O_bc.apply lt_to_le.
+   apply le_S_S.apply le_times_n.
+   apply le_n_Sn
+  |apply divides_pi_p_M
+  ]
+qed.
+
+theorem lt_O_to_le_teta_M_teta: \forall m. O < m\to
+teta (S(2*m)) < exp 2 (2*m)*teta (S m). 
+intros. 
+apply (le_to_lt_to_lt ? (M m*teta (S m)))
+  [apply le_teta_M_teta
+  |apply lt_times_l1
+    [apply lt_O_teta
+    |apply lt_M.
+     assumption
+    ]
+  ]
+qed.
+
+  
+             

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index 9bbce8144ff8885a7c7346bdb9b7937983bd5f7e..0baa86e3c28b43cfcddd5a8e0aa8f8a69af35685 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -101,7 +101,6 @@ qed.
 theorem divides_gcd_nm: \forall n,m.
 gcd n m \divides m \land gcd n m \divides n.
 intros.
-(*CSC: simplify simplifies too much because of a redex in gcd *)
 change with
 (match leb n m with
   [ true \Rightarrow 
@@ -594,7 +593,6 @@ intro.apply (nat_case n)
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
-(*CSC: bug here: unfold symmetric does not work *)
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
 intros.
@@ -904,3 +902,35 @@ cut (n \divides p \lor n \ndivides p)
  ]
 qed.
 
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+  [elim H.apply False_ind.
+   apply H2.apply sym_eq.apply H8
+    [assumption
+    |apply prime_to_lt_SO.assumption
+    ]
+  |elim H6.
+   apply (witness ? ? n1).
+   rewrite > assoc_times.
+   rewrite < H7.assumption
+  ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p  \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+  [apply False_ind.apply H1.assumption
+  |elim H5.
+   apply (witness ? ? n1).
+   rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+   rewrite > assoc_times.
+   rewrite < H6.assumption
+  ]
+qed.
\ No newline at end of file