]> matita.cs.unibo.it Git - helm.git/commitdiff
Towards chebyshev.
authorAndrea Asperti <andrea.asperti@unibo.it>
Mon, 19 Nov 2007 11:55:54 +0000 (11:55 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Mon, 19 Nov 2007 11:55:54 +0000 (11:55 +0000)
17 files changed:
helm/software/matita/library/nat/chebyshev.ma [new file with mode: 0644]
helm/software/matita/library/nat/compare.ma
helm/software/matita/library/nat/div_and_mod.ma
helm/software/matita/library/nat/euler_theorem.ma
helm/software/matita/library/nat/exp.ma
helm/software/matita/library/nat/factorial2.ma [new file with mode: 0644]
helm/software/matita/library/nat/factorization.ma
helm/software/matita/library/nat/gcd.ma
helm/software/matita/library/nat/generic_iter_p.ma
helm/software/matita/library/nat/le_arith.ma
helm/software/matita/library/nat/log.ma [new file with mode: 0644]
helm/software/matita/library/nat/lt_arith.ma
helm/software/matita/library/nat/minimization.ma
helm/software/matita/library/nat/ord.ma
helm/software/matita/library/nat/orders.ma
helm/software/matita/library/nat/pi_p.ma [new file with mode: 0644]
helm/software/matita/library/nat/primes.ma

diff --git a/helm/software/matita/library/nat/chebyshev.ma b/helm/software/matita/library/nat/chebyshev.ma
new file mode 100644 (file)
index 0000000..f980d44
--- /dev/null
@@ -0,0 +1,1680 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/chebishev".
+
+include "nat/log.ma".
+include "nat/pi_p.ma".
+include "nat/factorization.ma".
+include "nat/factorial2.ma".
+
+definition prim: nat \to nat \def
+\lambda n. sigma_p (S n) primeb (\lambda p.(S O)).
+
+definition A: nat \to nat \def
+\lambda n. pi_p (S n) primeb (\lambda p.exp p (log p n)).
+
+theorem le_Al1: \forall n.
+A n \le pi_p (S n) primeb (\lambda p.n).
+intro.unfold A.
+cases n
+  [simplify.apply le_n
+  |apply le_pi_p.
+   intros.
+   apply le_exp_log.
+   apply lt_O_S
+  ]
+qed.
+
+theorem le_Al: \forall n.
+A n \le exp n (prim n).
+intro.unfold prim.
+rewrite < exp_sigma_p.
+apply le_Al1.
+qed.
+
+theorem leA_r2: \forall n.
+exp n (prim n) \le A n * A n.
+intro.unfold prim.
+elim (le_to_or_lt_eq ? ? (le_O_n n))
+  [rewrite < (exp_sigma_p (S n) n primeb).
+   unfold A.
+   rewrite < times_pi_p.
+   apply le_pi_p.
+   intros.
+   rewrite < exp_plus_times.
+   apply (trans_le ? (exp i (S(log i n))))
+    [apply lt_to_le.
+     apply lt_exp_log.
+     apply prime_to_lt_SO.
+     apply primeb_true_to_prime.
+     assumption
+    |apply le_exp
+      [apply prime_to_lt_O.
+       apply primeb_true_to_prime.
+       assumption
+      |rewrite > plus_n_O.
+       simplify.
+       rewrite > plus_n_Sm.
+       apply le_plus_r.
+       apply lt_O_log
+        [assumption
+        |apply le_S_S_to_le.
+         apply H1
+        ]
+      ]
+    ]
+  |rewrite < H. apply le_n
+  ]
+qed.
+
+definition A': nat \to nat \def
+\lambda n. pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p n) (\lambda i.true) (\lambda i.p))).
+
+theorem eq_A_A': \forall n.A n = A' n.
+intro.unfold A.unfold A'.
+apply eq_pi_p
+  [intros.reflexivity
+  |intros.
+   apply (trans_eq ? ? (exp x (sigma_p (log x n) (λi:nat.true) (λi:nat.(S O)))))
+    [apply eq_f.apply sym_eq.apply sigma_p_true
+    |apply sym_eq.apply exp_sigma_p
+    ]
+  ]
+qed.
+
+theorem eq_pi_p_primeb_divides_b: \forall n,m.
+pi_p n (\lambda p.primeb p \land divides_b p m) (\lambda p.exp p (ord m p))
+= pi_p n primeb (\lambda p.exp p (ord m p)).
+intro.
+elim n
+  [reflexivity
+  |apply (bool_elim ? (primeb n1));intro
+    [rewrite > true_to_pi_p_Sn in ⊢ (? ? ? %)
+      [apply (bool_elim ? (divides_b n1 m));intro
+        [rewrite > true_to_pi_p_Sn
+          [apply eq_f.
+           apply H
+          |apply true_to_true_to_andb_true;assumption
+          ]
+        |rewrite > false_to_pi_p_Sn
+          [rewrite > not_divides_to_ord_O
+            [simplify in ⊢ (? ? ? (? % ?)).
+             rewrite > sym_times.
+             rewrite < times_n_SO.
+             apply H
+            |apply primeb_true_to_prime.assumption
+            |apply divides_b_false_to_not_divides.
+             assumption
+            ]
+          |rewrite > H1.rewrite > H2.reflexivity
+          ]
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_pi_p_Sn
+      [rewrite > false_to_pi_p_Sn
+        [apply H
+        |assumption
+        ]
+      |rewrite > H1.reflexivity
+      ]
+    ]
+  ]
+qed.
+    
+theorem lt_max_to_pi_p_primeb: \forall q,m. O < m \to max m (\lambda i.primeb i \land divides_b i m) < q \to
+m = pi_p q (\lambda i.primeb i \land divides_b i m) (\lambda p.exp p (ord m p)).
+intro.elim q
+  [apply False_ind.
+   apply (not_le_Sn_O ? H1)
+  |apply (bool_elim ? (primeb n∧divides_b n m));intro
+    [rewrite > true_to_pi_p_Sn
+      [rewrite > (exp_ord n m) in ⊢ (? ? % ?)
+        [apply eq_f.
+         rewrite > (H (ord_rem m n))
+          [apply eq_pi_p1
+            [intros.
+             apply (bool_elim ? (primeb x));intro
+              [simplify.
+               apply (bool_elim ? (divides_b x (ord_rem m n)));intro
+                [apply sym_eq.
+                 apply divides_to_divides_b_true
+                  [apply prime_to_lt_O.
+                   apply primeb_true_to_prime.
+                   assumption
+                  |apply (trans_divides ? (ord_rem m n))
+                    [apply divides_b_true_to_divides.
+                     assumption
+                    |apply divides_ord_rem
+                      [apply (trans_lt ? x)
+                        [apply prime_to_lt_SO.
+                         apply primeb_true_to_prime.
+                         assumption
+                        |assumption
+                        ]
+                      |assumption
+                      ]
+                    ]
+                  ]
+                |apply sym_eq.
+                 apply not_divides_to_divides_b_false
+                  [apply prime_to_lt_O.
+                   apply primeb_true_to_prime.
+                   assumption
+                  |apply ord_O_to_not_divides
+                    [assumption
+                    |apply primeb_true_to_prime.
+                     assumption
+                    |rewrite < (ord_ord_rem n)
+                      [apply not_divides_to_ord_O
+                        [apply primeb_true_to_prime.
+                         assumption
+                        |apply divides_b_false_to_not_divides.
+                         assumption
+                        ]
+                      |assumption
+                      |apply primeb_true_to_prime.
+                       apply (andb_true_true ? ? H3)
+                      |apply primeb_true_to_prime.
+                       assumption
+                      |assumption
+                      ]
+                    ]
+                  ]
+                ]
+              |reflexivity
+              ]
+            |intros.
+             apply eq_f.
+             apply ord_ord_rem
+              [assumption
+              |apply primeb_true_to_prime.
+               apply (andb_true_true ? ? H3)
+              |apply primeb_true_to_prime.
+               apply (andb_true_true ? ? H5)
+              |assumption
+              ]
+            ]
+          |apply lt_O_ord_rem
+            [apply prime_to_lt_SO.
+             apply primeb_true_to_prime.
+             apply (andb_true_true ? ? H3)
+            |assumption
+            ]
+          |apply not_eq_to_le_to_lt
+            [elim (exists_max_forall_false (λi:nat.primeb i∧divides_b i (ord_rem m n)) (ord_rem m n))
+              [elim H4.
+               intro.rewrite > H7 in H6.simplify in H6.
+               apply (not_divides_ord_rem m n)
+                [assumption
+                |apply prime_to_lt_SO.
+                 apply primeb_true_to_prime.
+                 apply (andb_true_true ? ? H3)
+                |apply divides_b_true_to_divides.
+                 apply (andb_true_true_r ? ? H6)
+                ]
+              |elim H4.rewrite > H6.
+               apply lt_to_not_eq.
+               apply prime_to_lt_O.
+               apply primeb_true_to_prime.
+               apply (andb_true_true ? ? H3)
+              ]
+            |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i (ord_rem m n))))
+              [apply le_to_le_max.
+               apply divides_to_le
+                [assumption
+                |apply divides_ord_rem
+                  [apply prime_to_lt_SO.
+                   apply primeb_true_to_prime.
+                   apply (andb_true_true ? ? H3)
+                  |assumption
+                  ]
+                ]
+              |apply (trans_le ? (max m (λi:nat.primeb i∧divides_b i m)))
+                [apply le_max_f_max_g.
+                 intros.
+                 apply (bool_elim ? (primeb i));intro
+                  [simplify.
+                   apply divides_to_divides_b_true
+                    [apply prime_to_lt_O.
+                     apply primeb_true_to_prime.
+                     assumption
+                    |apply (trans_divides ? (ord_rem m n))
+                      [apply divides_b_true_to_divides.
+                       apply (andb_true_true_r ? ? H5)
+                      |apply divides_ord_rem
+                        [apply prime_to_lt_SO.
+                         apply primeb_true_to_prime.
+                         apply (andb_true_true ? ? H3)
+                        |assumption
+                        ]
+                      ]
+                    ]
+                  |rewrite > H6 in H5.
+                   assumption
+                  ]
+                |apply le_S_S_to_le.
+                 assumption
+                ]
+              ]
+            ]
+          ]
+        |apply prime_to_lt_SO.
+         apply primeb_true_to_prime.
+         apply (andb_true_true ? ? H3)
+        |assumption
+        ]
+      |assumption
+      ]
+    |elim (le_to_or_lt_eq ? ? H1)
+      [rewrite > false_to_pi_p_Sn
+        [apply H
+          [assumption
+          |apply false_to_lt_max
+            [apply (lt_to_le_to_lt ? (max m (λi:nat.primeb i∧divides_b i m)))
+              [apply lt_to_le.
+               apply lt_SO_max_prime.
+               assumption
+              |apply le_S_S_to_le.
+               assumption
+              ]
+            |assumption
+            |apply le_S_S_to_le.
+             assumption
+            ]
+          ]
+        |assumption
+        ]
+      |rewrite < H4.
+       rewrite < (pi_p_false (λp:nat.p\sup(ord (S O) p)) (S n) ) in ⊢ (? ? % ?).
+       apply eq_pi_p
+        [intros.
+         apply (bool_elim ? (primeb x));intro
+          [apply sym_eq.
+           change with (divides_b x (S O) =false).
+           apply not_divides_to_divides_b_false
+            [apply prime_to_lt_O.
+             apply primeb_true_to_prime.
+             assumption
+            |intro.
+             apply (le_to_not_lt x (S O))
+              [apply divides_to_le
+                [apply lt_O_S.assumption
+                |assumption
+                ]
+              |elim (primeb_true_to_prime ? H6).
+               assumption
+              ]
+            ]
+          |reflexivity
+          ]
+        |intros.reflexivity
+        ]
+      ]
+    ]
+  ]
+qed.
+    
+theorem pi_p_primeb_divides_b: \forall n. O < n \to 
+n = pi_p (S n) (\lambda i.primeb i \land divides_b i n) (\lambda p.exp p (ord n p)).
+intros.
+apply lt_max_to_pi_p_primeb
+  [assumption
+  |apply le_S_S.
+   apply le_max_n
+  ]
+qed.
+
+theorem pi_p_primeb: \forall n. O < n \to 
+n = pi_p (S n) primeb (\lambda p.exp p (ord n p)).
+intros.
+rewrite < eq_pi_p_primeb_divides_b.
+apply pi_p_primeb_divides_b.
+assumption.
+qed.
+
+theorem le_ord_log: \forall n,p. O < n \to S O < p \to
+ord n p \le log p n.
+intros.
+rewrite > (exp_ord p) in ⊢ (? ? (? ? %))
+  [rewrite > log_exp
+    [apply le_plus_n_r
+    |assumption
+    |apply lt_O_ord_rem;assumption
+    ]
+  |assumption
+  |assumption
+  ]
+qed.
+
+theorem sigma_p_divides_b:
+\forall m,n,p. O < n \to prime p \to \lnot divides p n \to
+m = sigma_p m (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
+intro.elim m
+  [reflexivity
+  |simplify in ⊢ (? ? ? (? % ? ?)).
+   rewrite > true_to_sigma_p_Sn
+    [rewrite > sym_plus.rewrite < plus_n_SO.
+     apply eq_f.
+     rewrite > (H n1 p H1 H2 H3) in ⊢ (? ? % ?).
+     apply eq_sigma_p1
+      [intros.
+       apply (bool_elim ? (divides_b (p\sup(S x)) (p\sup n*n1)));intro
+        [apply sym_eq.
+         apply divides_to_divides_b_true
+          [apply lt_O_exp.
+           apply prime_to_lt_O.
+           assumption
+          |apply (witness ? ? ((exp p (n - x))*n1)).
+           rewrite < assoc_times.
+           rewrite < exp_plus_times.
+           apply eq_f2
+            [apply eq_f.simplify.
+             apply eq_f.
+             rewrite > sym_plus.
+             apply plus_minus_m_m.
+             apply lt_to_le.assumption
+            |reflexivity
+            ]
+          ]
+        |apply sym_eq.
+         apply False_ind.
+         apply (divides_b_false_to_not_divides ? ? H5).
+         apply (witness ? ? ((exp p (n - S x))*n1)).
+         rewrite < assoc_times.
+         rewrite < exp_plus_times.
+         apply eq_f2
+          [apply eq_f.
+           rewrite > sym_plus.
+           apply plus_minus_m_m.
+           assumption
+          |reflexivity
+          ]
+        ]
+      |intros.reflexivity
+      ]
+    |apply divides_to_divides_b_true
+      [apply lt_O_exp.
+       apply prime_to_lt_O.assumption
+      |apply (witness ? ? n1).reflexivity
+      ]
+    ]
+  ]
+qed.
+  
+theorem sigma_p_divides_b1:
+\forall m,n,p,k. O < n \to prime p \to \lnot divides p n \to m \le k \to
+m = sigma_p k (λi:nat.divides_b (p\sup (S i)) ((exp p m)*n)) (λx:nat.S O).
+intros.
+lapply (prime_to_lt_SO ? H1) as H4.
+lapply (prime_to_lt_O ? H1) as H5.
+rewrite > (false_to_eq_sigma_p m k)
+  [apply sigma_p_divides_b;assumption
+  |assumption
+  |intros.
+   apply not_divides_to_divides_b_false
+    [apply lt_O_exp.assumption
+    |intro.apply (le_to_not_lt ? ? H6).
+     unfold lt.
+     rewrite < (ord_exp p)
+      [rewrite > (plus_n_O m).
+       rewrite < (not_divides_to_ord_O ? ? H1 H2).
+       rewrite < (ord_exp p ? H4) in ⊢ (? ? (? % ?)).
+       rewrite < ord_times
+        [apply divides_to_le_ord
+          [apply lt_O_exp.assumption
+          |rewrite > (times_n_O O).
+           apply lt_times
+            [apply lt_O_exp.assumption
+            |assumption
+            ]
+          |assumption
+          |assumption
+          ]
+        |apply lt_O_exp.assumption
+        |assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem eq_ord_sigma_p:
+\forall n,m,x. O < n \to prime x \to 
+exp x m \le n \to n < exp x (S m) \to
+ord n x=sigma_p m (λi:nat.divides_b (x\sup (S i)) n) (λx:nat.S O).
+intros.
+lapply (prime_to_lt_SO ? H1).
+rewrite > (exp_ord x n) in ⊢ (? ? ? (? ? (λi:?.? ? %) ?))
+  [apply sigma_p_divides_b1
+    [apply lt_O_ord_rem;assumption
+    |assumption
+    |apply not_divides_ord_rem;assumption
+    |apply lt_S_to_le.
+     apply (le_to_lt_to_lt ? (log x n))
+      [apply le_ord_log;assumption
+      |apply (lt_exp_to_lt x)
+        [assumption
+        |apply (le_to_lt_to_lt ? n ? ? H3).
+         apply le_exp_log.
+         assumption
+        ]
+      ]
+    ]
+  |assumption
+  |assumption
+  ]
+qed.
+    
+theorem pi_p_primeb1: \forall n. O < n \to 
+n = pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p n) 
+    (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))).
+intros.
+rewrite > (pi_p_primeb n H) in ⊢ (? ? % ?).
+apply eq_pi_p1
+  [intros.reflexivity
+  |intros.
+   rewrite > exp_sigma_p.
+   apply eq_f.
+   apply eq_ord_sigma_p
+    [assumption
+    |apply primeb_true_to_prime.
+     assumption
+    |apply le_exp_log.assumption
+    |apply lt_exp_log.
+     apply prime_to_lt_SO.
+     apply primeb_true_to_prime.
+     assumption
+    ]
+  ]
+qed.
+
+theorem eq_fact_pi_p:\forall n. fact n = 
+pi_p (S n) (\lambda i.leb (S O) i) (\lambda i.i).
+intro.elim n
+  [reflexivity
+  |change with ((S n1)*n1! = pi_p (S (S n1)) (λi:nat.leb (S O) i) (λi:nat.i)).
+   rewrite > true_to_pi_p_Sn
+    [apply eq_f.assumption
+    |reflexivity
+    ]
+  ]
+qed.
+   
+theorem eq_sigma_p_div: \forall n,q.O < q \to
+sigma_p (S n) (λm:nat.leb (S O) m∧divides_b q m) (λx:nat.S O)
+=n/q.
+intros.
+apply (div_mod_spec_to_eq n q ? (n \mod q) ? (n \mod q))
+  [apply div_mod_spec_intro
+    [apply lt_mod_m_m.assumption
+    |elim n
+      [simplify.elim q;reflexivity
+      |elim (or_div_mod1 n1 q)
+        [elim H2.clear H2.
+         rewrite > divides_to_mod_O
+          [rewrite < plus_n_O.
+           rewrite > true_to_sigma_p_Sn
+            [rewrite > H4 in ⊢ (? ? % ?).
+             apply eq_f2
+              [rewrite < sym_plus.
+               rewrite < plus_n_SO.
+               apply eq_f.
+               apply (div_mod_spec_to_eq n1 q (div n1 q) (mod n1 q) ? (mod n1 q))
+                [apply div_mod_spec_div_mod.
+                 assumption
+                |apply div_mod_spec_intro
+                  [apply lt_mod_m_m.assumption
+                  |assumption
+                  ]
+                ]
+              |reflexivity
+              ]
+            |apply true_to_true_to_andb_true
+              [reflexivity
+              |apply divides_to_divides_b_true;assumption
+              ]
+            ]
+          |assumption
+          |assumption
+          ]
+        |elim H2.clear H2.
+         rewrite > false_to_sigma_p_Sn
+          [rewrite > mod_S
+            [rewrite < plus_n_Sm.
+             apply eq_f.
+             assumption
+            |assumption
+            |elim (le_to_or_lt_eq (S (mod n1 q)) q)
+              [assumption
+              |apply False_ind.
+               apply H3.
+               apply (witness ? ? (S(div n1 q))).
+               rewrite < times_n_Sm.
+               rewrite < sym_plus.
+               rewrite < H2 in ⊢ (? ? ? (? ? %)).
+               rewrite > sym_times.
+               assumption
+              |apply lt_mod_m_m.
+               assumption
+              ]
+            ]
+          |rewrite > not_divides_to_divides_b_false
+            [rewrite < andb_sym in ⊢ (? ? % ?).reflexivity
+            |assumption
+            |assumption
+            ]
+          ]
+        |assumption
+        ]
+      ]
+    ]
+  |apply div_mod_spec_div_mod.
+   assumption
+  ]
+qed.              
+
+theorem fact_pi_p: \forall n. fact n =
+pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p n) 
+    (\lambda i.true) (\lambda i.(exp p (n /(exp p (S i))))))).
+intros.
+rewrite > eq_fact_pi_p.
+apply (trans_eq ? ? 
+  (pi_p (S n) (λi:nat.leb (S O) i) 
+   (λn.pi_p (S n) primeb 
+    (\lambda p.(pi_p (log p n) 
+     (\lambda i.divides_b (exp p (S i)) n) (\lambda i.p))))))
+  [apply eq_pi_p1;intros
+    [reflexivity
+    |apply pi_p_primeb1.
+     apply leb_true_to_le.assumption
+    ]
+  |apply (trans_eq ? ? 
+    (pi_p (S n) (λi:nat.leb (S O) i)
+     (λn:nat
+      .pi_p (S n) (\lambda p.primeb p\land leb p n)
+       (λp:nat.pi_p (log p n) (λi:nat.divides_b ((p)\sup(S i)) n) (λi:nat.p)))))
+    [apply eq_pi_p1
+      [intros.reflexivity
+      |intros.apply eq_pi_p1
+        [intros.elim (primeb x1)
+          [simplify.apply sym_eq.
+           apply le_to_leb_true.
+           apply le_S_S_to_le.
+           assumption
+          |reflexivity
+          ]
+        |intros.reflexivity
+        ]
+      ]
+    |apply (trans_eq ? ? 
+      (pi_p (S n) (λi:nat.leb (S O) i)
+       (λm:nat
+        .pi_p (S n) (λp:nat.primeb p∧leb p m)
+         (λp:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))))
+      [apply eq_pi_p1
+        [intros.reflexivity
+        |intros.
+         apply sym_eq.
+         apply false_to_eq_pi_p
+          [assumption
+          |intros.rewrite > lt_to_leb_false
+            [elim primeb;reflexivity|assumption]
+          ]
+        ]
+      |(* make a general theorem *)
+       apply (trans_eq ? ? 
+        (pi_p (S n) primeb
+         (λp:nat
+          .pi_p (S n) (λm.leb p m)
+           (λm:nat.pi_p (log p m) (λi:nat.divides_b ((p)\sup(S i)) m) (λi:nat.p)))
+        ))
+        [apply pi_p_pi_p1.
+         intros.
+         apply (bool_elim ? (primeb y \land leb y x));intros
+          [rewrite > (le_to_leb_true (S O) x)
+            [reflexivity
+            |apply (trans_le ? y)
+              [apply prime_to_lt_O.
+               apply primeb_true_to_prime.
+               apply (andb_true_true ? ? H2)
+              |apply leb_true_to_le.
+               apply (andb_true_true_r ? ? H2)
+              ]
+            ]
+          |elim (leb (S O) x);reflexivity
+          ]
+        |apply eq_pi_p1
+          [intros.reflexivity
+          |intros.
+           apply (trans_eq ? ? 
+            (pi_p (S n) (λm:nat.leb x m)
+             (λm:nat.pi_p (log x n) (λi:nat.divides_b (x\sup(S i)) m) (λi:nat.x))))
+            [apply eq_pi_p1
+              [intros.reflexivity
+              |intros.
+               apply sym_eq.
+               apply false_to_eq_pi_p
+                [apply le_log
+                  [apply prime_to_lt_SO.
+                   apply primeb_true_to_prime.
+                   assumption
+                  |apply (lt_to_le_to_lt ? x)
+                    [apply prime_to_lt_O.
+                     apply primeb_true_to_prime.
+                     assumption
+                    |apply leb_true_to_le.
+                     assumption
+                    ]
+                  |apply le_S_S_to_le.
+                   assumption
+                  ]
+                |intros.
+                 apply not_divides_to_divides_b_false
+                  [apply lt_O_exp.
+                   apply prime_to_lt_O.
+                   apply primeb_true_to_prime.
+                   assumption
+                  |intro.
+                   apply (lt_to_not_le x1 (exp x (S i)))
+                    [apply (lt_to_le_to_lt ? (exp x (S(log x x1))))
+                      [apply lt_exp_log.
+                       apply prime_to_lt_SO.
+                       apply primeb_true_to_prime.
+                       assumption
+                      |apply le_exp
+                        [apply prime_to_lt_O.
+                         apply primeb_true_to_prime.
+                         assumption
+                        |apply le_S_S.
+                         assumption
+                        ]
+                      ]
+                    |apply divides_to_le
+                      [apply (lt_to_le_to_lt ? x)
+                        [apply prime_to_lt_O.
+                         apply primeb_true_to_prime.
+                         assumption
+                        |apply leb_true_to_le.
+                         assumption
+                        ]
+                      |assumption
+                      ]
+                    ]
+                  ]
+                ]
+              ]
+            |apply 
+             (trans_eq ? ? 
+              (pi_p (log x n) (λi:nat.true)
+               (λi:nat.pi_p (S n) (λm:nat.leb x m \land divides_b (x\sup(S i)) m) (λm:nat.x))))
+              [apply (pi_p_pi_p1 (\lambda m,i.x)).
+               intros.
+               reflexivity
+              |apply eq_pi_p1
+                [intros.reflexivity
+                |intros.
+                 rewrite > exp_sigma_p.
+                 apply eq_f.
+                 apply (trans_eq ? ? 
+                  (sigma_p (S n) (λm:nat.leb (S O) m∧divides_b (x\sup(S x1)) m) (λx:nat.S O)))
+                  [apply eq_sigma_p1
+                    [intros.
+                     apply (bool_elim ? (divides_b (x\sup(S x1)) x2));intro
+                      [apply (bool_elim ? (leb x x2));intro
+                        [rewrite > le_to_leb_true
+                          [reflexivity
+                          |apply (trans_le ? x)
+                            [apply prime_to_lt_O.
+                             apply primeb_true_to_prime.
+                             assumption
+                            |apply leb_true_to_le.
+                             assumption
+                            ]
+                          ]
+                        |rewrite > lt_to_leb_false
+                          [reflexivity
+                          |apply not_le_to_lt.intro.
+                           apply (leb_false_to_not_le ? ? H6).
+                           apply (trans_le ? (exp x (S x1)))
+                            [rewrite > times_n_SO in ⊢ (? % ?).
+                             change with (exp x (S O) \le exp x (S x1)).
+                             apply le_exp
+                              [apply prime_to_lt_O.
+                               apply primeb_true_to_prime.
+                               assumption
+                              |apply le_S_S.apply le_O_n.
+                              ]
+                            |apply divides_to_le
+                              [assumption
+                              |apply divides_b_true_to_divides.
+                               assumption
+                              ]
+                            ]
+                          ]
+                        ]
+                      |rewrite < andb_sym.
+                       rewrite < andb_sym in ⊢ (? ? ? %).
+                       reflexivity
+                      ]
+                    |intros.reflexivity
+                    ]
+                  |apply eq_sigma_p_div.
+                   apply lt_O_exp.
+                   apply prime_to_lt_O.
+                   apply primeb_true_to_prime.
+                   assumption
+                  ]
+                ]
+              ]
+            ]
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+(* odd n is just mod n (S(S O)) 
+let rec odd n \def
+  match n with 
+  [ O \Rightarrow O
+  | S m \Rightarrow (S O) - odd m 
+  ].
+
+theorem le_odd_SO: \forall n. odd n \le S O.
+intro.elim n
+  [apply le_O_n
+  |simplify.cases (odd n1)
+    [simplify.apply le_n.
+    |apply le_O_n
+    ]
+  ]
+qed.
+
+theorem SSO_odd: \forall n. n = (n/(S(S O)))*(S(S O)) + odd n.
+intro.elim n
+  [apply (lt_O_n_elim ? H).
+   intro.simplify.reflexivity
+  |
+*)
+
+theorem fact_pi_p2: \forall n. fact ((S(S O))*n) =
+pi_p (S ((S(S O))*n)) primeb 
+  (\lambda p.(pi_p (log p ((S(S O))*n)) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))*(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O)))))))).
+intros.rewrite > fact_pi_p.
+apply eq_pi_p1
+  [intros.reflexivity
+  |intros.apply eq_pi_p
+    [intros.reflexivity
+    |intros.
+     rewrite < exp_plus_times.
+     apply eq_f.
+     rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+     apply SSO_mod.
+     apply lt_O_exp.
+     apply prime_to_lt_O.
+     apply primeb_true_to_prime.
+     assumption
+    ]
+  ]
+qed.
+
+theorem fact_pi_p3: \forall n. fact ((S(S O))*n) =
+pi_p (S ((S(S O))*n)) primeb 
+  (\lambda p.(pi_p (log p ((S(S O))*n)) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))*
+pi_p (S ((S(S O))*n)) primeb 
+  (\lambda p.(pi_p (log p ((S(S O))*n))   
+    (\lambda i.true) (\lambda i.(exp p (mod ((S(S O))*n /(exp p (S i))) (S(S O))))))).
+intros.
+rewrite < times_pi_p.
+rewrite > fact_pi_p2.
+apply eq_pi_p;intros 
+  [reflexivity
+  |apply times_pi_p
+  ]
+qed.
+
+theorem pi_p_primeb4: \forall n. S O < n \to
+pi_p (S ((S(S O))*n)) primeb 
+  (\lambda p.(pi_p (log p ((S(S O))*n)) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
+= 
+pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p (S(S O)*n)) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+intros.
+apply or_false_eq_SO_to_eq_pi_p
+  [apply le_S_S.
+   apply le_times_n.
+   apply lt_O_S
+  |intros.
+   right.
+   rewrite > log_i_SSOn
+    [change with (i\sup((S(S O))*(n/i\sup(S O)))*(S O) = S O).
+     rewrite < times_n_SO.
+     rewrite > eq_div_O
+      [reflexivity
+      |simplify.rewrite < times_n_SO.assumption
+      ]
+    |assumption
+    |assumption
+    |apply le_S_S_to_le.assumption
+    ]
+  ]
+qed.
+   
+theorem pi_p_primeb5: \forall n. S O < n \to
+pi_p (S ((S(S O))*n)) primeb 
+  (\lambda p.(pi_p (log p ((S(S O))*n)) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i))))))))
+= 
+pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p n) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+intros.
+rewrite > (pi_p_primeb4 ? H).
+apply eq_pi_p1;intros
+  [reflexivity
+  |apply or_false_eq_SO_to_eq_pi_p
+    [apply le_log
+      [apply prime_to_lt_SO.
+       apply primeb_true_to_prime.
+       assumption
+      |apply lt_to_le.assumption
+      |apply le_times_n.
+       apply lt_O_S
+      ]
+    |intros.right.
+     rewrite > eq_div_O
+      [simplify.reflexivity
+      |apply (lt_to_le_to_lt ? (exp x (S(log x n))))
+        [apply lt_exp_log.
+         apply prime_to_lt_SO.
+         apply primeb_true_to_prime.
+         assumption
+        |apply le_exp
+          [apply prime_to_lt_O.
+           apply primeb_true_to_prime.
+           assumption
+          |apply le_S_S.
+           assumption
+          ]
+        ]
+      ]
+    ]
+  ]
+qed.
+
+theorem exp_fact_SSO: \forall n.
+exp (fact n) (S(S O))
+= 
+pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p n) 
+    (\lambda i.true) (\lambda i.(exp p ((S(S O))*(n /(exp p (S i)))))))).
+intros.
+rewrite > fact_pi_p.
+rewrite < exp_pi_p.
+apply eq_pi_p;intros
+  [reflexivity
+  |apply sym_eq.
+   apply exp_times_pi_p
+  ]
+qed.
+
+definition B \def
+\lambda n.
+pi_p (S n) primeb 
+  (\lambda p.(pi_p (log p n)   
+    (\lambda i.true) (\lambda i.(exp p (mod (n /(exp p (S i))) (S(S O))))))).
+
+theorem eq_fact_B:\forall n.S O < n \to
+fact ((S(S O))*n) = exp (fact n) (S(S O)) * B((S(S O))*n).
+intros. unfold B.
+rewrite > fact_pi_p3.
+apply eq_f2
+  [apply sym_eq.
+   rewrite > pi_p_primeb5
+    [apply exp_fact_SSO
+    |assumption
+    ]
+  |reflexivity
+  ]
+qed.
+
+theorem le_B_A: \forall n. B n \le A n.
+intro.unfold B.
+rewrite > eq_A_A'.
+unfold A'.
+apply le_pi_p.intros.
+apply le_pi_p.intros.
+rewrite > exp_n_SO in ⊢ (? ? %).
+apply le_exp
+  [apply prime_to_lt_O.
+   apply primeb_true_to_prime.
+   assumption
+  |apply le_S_S_to_le.
+   apply lt_mod_m_m.
+   apply lt_O_S
+  ]
+qed.
+
+theorem le_fact_A:\forall n.S O < n \to
+fact ((S(S O))*n) \le exp (fact n) (S(S O)) * A ((S(S O))*n).
+intros.
+rewrite > eq_fact_B
+  [apply le_times_r.
+   apply le_B_A
+  |assumption
+  ]
+qed.
+
+theorem le_B_exp: \forall n.S O < n \to
+B ((S(S O))*n) \le exp (S(S O)) ((S(S O))*n).
+intros.
+apply (le_times_to_le (exp (fact n) (S(S O))))
+  [apply lt_O_exp.
+   apply lt_O_fact
+  |rewrite < eq_fact_B
+    [rewrite < sym_times in ⊢ (? ? %).
+     rewrite > exp_SSO.
+     rewrite < assoc_times.
+     apply fact1
+    |assumption
+    ]
+  ]
+qed.
+
+theorem le_A_SSO_A: \forall n.
+A((S(S O))*n) \le 
+ pi_p (S ((S(S O))*n)) primeb (λp:nat.p)*A n.
+unfold A.intros.
+cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
+  [rewrite > Hcut.
+   rewrite < times_pi_p.
+   apply le_pi_p.intros.
+   lapply (prime_to_lt_SO ? (primeb_true_to_prime ? H1)) as H2.
+   change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
+   apply le_exp
+    [apply lt_to_le.assumption
+    |apply (trans_le ? (log i (i*n)))
+      [apply le_log
+        [assumption
+        |apply not_le_to_lt.intro.
+         apply (lt_to_not_le ? ? H).  
+         apply (trans_le ? (S O)) 
+          [apply le_S_S.assumption
+          |apply lt_to_le.assumption
+          ] 
+        |apply le_times_l.
+         assumption
+        ]
+      |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
+       rewrite > log_exp
+        [apply le_n
+        |assumption
+        |apply not_le_to_lt.intro.
+         apply (lt_to_not_le ? ? H). 
+         apply (le_n_O_elim ? H3).
+         apply lt_to_le.
+         assumption
+        ] 
+      ]
+    ]
+  |apply sym_eq.
+   apply or_false_eq_SO_to_eq_pi_p
+    [apply le_S_S.
+     apply le_times_n.
+     apply lt_O_S
+    |intros.right.
+     change with (exp i (log i n) = (exp i O)).
+     apply eq_f.
+     apply antisymmetric_le
+      [cut (O < n)
+        [apply le_S_S_to_le.
+         apply (lt_exp_to_lt i)
+          [apply (le_to_lt_to_lt ? n);assumption
+          |apply (le_to_lt_to_lt ? n)
+            [apply le_exp_log.
+             assumption
+            |rewrite < exp_n_SO.
+             assumption
+            ]
+          ]
+        |apply not_le_to_lt.intro.
+         apply (lt_to_not_le ? ? H1).
+         generalize in match H.
+         apply (le_n_O_elim ? H2).
+         intro.assumption
+        ]
+      |apply le_O_n
+      ]
+    ]
+  ]
+qed.
+    
+(* so far so good 
+
+theorem le_A_BA: \forall n. 
+A((S(S O))*n) \le B((S(S O))*n)*A n.
+(*
+  [simplify.reflexivity
+  |rewrite > times_SSO.
+   rewrite > times_SSO.
+   unfold A.
+apply (trans_le ? ((pi_p (S ((S(S O))*n)) primeb (λp:nat.p))*A n))
+  [apply le_A_SSO_A
+  |apply le_times_l.
+   unfold B.
+   apply le_pi_p.intros.
+*)
+intro.unfold A.unfold B.
+cut (pi_p (S n) primeb (λp:nat.(exp p (log p n))) = pi_p (S ((S(S O))*n)) primeb (λp:nat.(p)\sup(log p n)))
+  [rewrite > Hcut.
+   rewrite < times_pi_p.
+   apply le_pi_p.intros.
+   apply le_trans i.
+   
+
+   change with (i\sup(log i ((S(S O))*n))≤i\sup(S(log i n))).
+   apply le_exp
+    [apply prime_to_lt_O.
+     apply primeb_true_to_prime.
+     assumption
+    |apply (trans_le ? (log i (i*n)))
+      [apply le_log
+        [apply prime_to_lt_SO.
+         apply primeb_true_to_prime.
+         assumption
+        |apply not_le_to_lt.intro.
+         apply (lt_to_not_le ? ? H).  
+         apply (trans_le ? (S O)) 
+          [apply le_S_S.assumption
+          |apply prime_to_lt_O.
+           apply primeb_true_to_prime.
+           assumption 
+          ] 
+        |apply le_times_l.
+         apply prime_to_lt_SO.
+         apply primeb_true_to_prime.
+         assumption
+        ]
+      |rewrite > exp_n_SO in ⊢ (? (? ? (? % ?)) ?).
+       rewrite > log_exp
+        [apply le_n
+        |apply prime_to_lt_SO.
+         apply primeb_true_to_prime.
+         assumption
+        |apply not_le_to_lt.intro.
+         apply (lt_to_not_le ? ? H). 
+         apply (le_n_O_elim ? H2).
+         apply prime_to_lt_O.
+         apply primeb_true_to_prime.
+         assumption
+        ] 
+      ]
+    ]
+  |apply sym_eq.
+   apply or_false_eq_SO_to_eq_pi_p
+    [apply le_S_S.
+     apply le_times_n.
+     apply lt_O_S
+    |intros.right.
+     change with (exp i (log i n) = (exp i O)).
+     apply eq_f.
+     apply antisymmetric_le
+      [cut (O < n)
+        [apply le_S_S_to_le.
+         apply (lt_exp_to_lt i)
+          [apply (le_to_lt_to_lt ? n);assumption
+          |apply (le_to_lt_to_lt ? n)
+            [apply le_exp_log.
+             assumption
+            |rewrite < exp_n_SO.
+             assumption
+            ]
+          ]
+        |apply not_le_to_lt.intro.
+         apply (lt_to_not_le ? ? H1).
+         generalize in match H.
+         apply (le_n_O_elim ? H2).
+         intro.assumption
+        ]
+      |apply le_O_n
+      ]
+    ]
+  ]
+qed.
+
+
+unfold A.unfold B.
+rewrite > eq_A_A'.rewrite > eq_A_A'.
+unfold A'.unfold B.
+
+(* da spostare *)
+theorem times_exp: \forall n,m,p.exp n p * exp m p = exp (n*m) p.
+intros.elim p
+  [reflexivity
+  |simplify.autobatch
+  ]
+qed.
+
+theorem le_exp_log: \forall p,n. O < n \to
+exp p (
+log n) \le n.
+intros.
+apply leb_true_to_le.
+unfold log.
+apply (f_max_true (\lambda x.leb (exp p x) n)).
+apply (ex_intro ? ? O).
+split
+  [apply le_O_n
+  |apply le_to_leb_true.simplify.assumption
+  ]
+qed.
+
+theorem lt_log_n_n: \forall n. O < n \to log n < n.
+intros.
+cut (log n \le n)
+  [elim (le_to_or_lt_eq ? ? Hcut)
+    [assumption
+    |absurd (exp (S(S O)) n \le n)
+      [rewrite < H1 in ⊢ (? (? ? %) ?).
+       apply le_exp_log.
+       assumption
+      |apply lt_to_not_le.
+       apply lt_m_exp_nm.
+       apply le_n
+      ]
+    ]
+  |unfold log.apply le_max_n
+  ]
+qed.
+
+theorem le_log_n_n: \forall n. log n \le n.
+intro.
+cases n
+  [apply le_n
+  |apply lt_to_le.
+   apply lt_log_n_n.
+   apply lt_O_S
+  ]
+qed.
+
+theorem lt_exp_log: \forall n. n < exp (S(S O)) (S (log n)).
+intro.cases n
+  [simplify.apply le_S.apply le_n
+  |apply not_le_to_lt.
+   apply leb_false_to_not_le.
+   apply (lt_max_to_false ? (S n1) (S (log (S n1))))
+    [apply le_S_S.apply le_n
+    |apply lt_log_n_n.apply lt_O_S
+    ]
+  ]
+qed.
+
+theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
+(\forall m. p < m \to f m = false)
+\to max n f \le p.
+intros.
+apply not_lt_to_le.intro.
+apply not_eq_true_false.
+rewrite < (H1 ? H2).
+apply sym_eq.
+apply f_max_true.
+assumption.
+qed.
+
+theorem log_times1: \forall n,m. O < n \to O < m \to
+log (n*m) \le S(log n+log m).
+intros.
+unfold in ⊢ (? (% ?) ?).
+apply f_false_to_le_max
+  [apply (ex_intro ? ? O).
+   split
+    [apply le_O_n
+    |apply le_to_leb_true.
+     simplify.
+     rewrite > times_n_SO.
+     apply le_times;assumption
+    ]
+  |intros.
+   apply lt_to_leb_false.
+   apply (lt_to_le_to_lt ? ((exp (S(S O)) (S(log n)))*(exp (S(S O)) (S(log m)))))
+    [apply lt_times;apply lt_exp_log
+    |rewrite < exp_plus_times.
+     apply le_exp
+      [apply lt_O_S
+      |simplify.
+       rewrite < plus_n_Sm.
+       assumption
+      ]
+    ]
+  ]
+qed.
+  
+theorem log_times: \forall n,m.log (n*m) \le S(log n+log m).
+intros.
+cases n
+  [apply le_O_n
+  |cases m
+    [rewrite < times_n_O.
+     apply le_O_n
+    |apply log_times1;apply lt_O_S
+    ]
+  ]
+qed.
+
+theorem log_exp: \forall n,m.O < m \to
+log ((exp (S(S O)) n)*m)=n+log m.
+intros.
+unfold log in ⊢ (? ? (% ?) ?).
+apply max_spec_to_max.
+unfold max_spec.
+split
+  [split
+    [elim n
+      [simplify.
+       rewrite < plus_n_O.
+       apply le_log_n_n
+      |simplify.
+       rewrite < plus_n_O.
+       rewrite > times_plus_l.
+       apply (trans_le ? (S((S(S O))\sup(n1)*m)))
+        [apply le_S_S.assumption
+        |apply (lt_O_n_elim ((S(S O))\sup(n1)*m))
+          [rewrite > (times_n_O O) in ⊢ (? % ?).
+           apply lt_times
+            [apply lt_O_exp.
+             apply lt_O_S
+            |assumption
+            ]
+          |intro.simplify.apply le_S_S.
+           apply le_plus_n
+          ]
+        ]
+      ]
+    |simplify.
+     apply le_to_leb_true.
+     rewrite > exp_plus_times.
+     apply le_times_r.
+     apply le_exp_log.
+     assumption
+    ]
+  |intros.
+   simplify.
+   apply lt_to_leb_false.
+   apply (lt_to_le_to_lt ? ((exp (S(S O)) n)*(exp (S(S O)) (S(log m)))))
+    [apply lt_times_r1
+      [apply lt_O_exp.apply lt_O_S
+      |apply lt_exp_log.
+      ]
+    |rewrite < exp_plus_times.
+     apply le_exp
+      [apply lt_O_S
+      |rewrite < plus_n_Sm.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem log_SSO: \forall n. O < n \to 
+log ((S(S O))*n) = S (log n).
+intros.
+change with (log ((exp (S(S O)) (S O))*n)=S (log n)).
+rewrite > log_exp.reflexivity.assumption.
+qed.
+
+theorem or_eq_S: \forall n.\exists m. 
+(n = (S(S O))*m) \lor (n = S((S(S O))*m)).
+intro.
+elim n
+  [apply (ex_intro ? ? O).left.apply times_n_O
+  |elim H.elim H1
+    [apply (ex_intro ? ? a).right.apply eq_f.assumption
+    |apply (ex_intro ? ? (S a)).left.
+     rewrite > H2.simplify.
+     rewrite < plus_n_O.
+     rewrite < plus_n_Sm.
+     reflexivity
+    ]
+  ]
+qed.
+
+theorem lt_O_to_or_eq_S: \forall n.O < n \to \exists m.m < n \land 
+((n = (S(S O))*m) \lor (n = S((S(S O))*m))).
+intros.  
+elim (or_eq_S n).
+elim H1
+  [apply (ex_intro ? ? a).split
+    [rewrite > H2.
+     rewrite > times_n_SO in ⊢ (? % ?).
+     rewrite > sym_times.
+     apply lt_times_l1
+      [apply (divides_to_lt_O a n ? ?)
+        [assumption
+        |apply (witness a n (S (S O))).
+         rewrite > sym_times.
+         assumption
+        ]
+      |apply le_n
+      ]
+    |left.assumption
+    ]
+  |apply (ex_intro ? ? a).split
+    [rewrite > H2.
+     apply (le_to_lt_to_lt ? ((S(S O))*a))
+      [rewrite > times_n_SO in ⊢ (? % ?).
+       rewrite > sym_times. 
+       apply le_times_l.
+       apply le_n_Sn
+      |apply le_n
+      ]
+    |right.assumption
+    ]
+  ]
+qed.
+
+theorem factS: \forall n. fact (S n) = (S n)*(fact n).
+intro.simplify.reflexivity.
+qed.
+
+theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
+intros.reflexivity.
+qed.
+
+lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
+intro.simplify.rewrite < plus_n_Sm.reflexivity.
+qed.
+
+theorem fact1: \forall n.
+fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
+intro.elim n
+  [rewrite < times_n_O.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite > factS.
+   rewrite < assoc_times.
+   rewrite > factS.
+   apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
+    [apply le_times_l.
+     rewrite > times_SSO.
+     apply le_times_r.
+     apply le_n_Sn
+    |rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > exp_S. 
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite < assoc_times.
+     rewrite < assoc_times.
+     rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > exp_S. 
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite > sym_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite > sym_times in ⊢ (? ? (? ? %)).
+     rewrite > sym_times in ⊢ (? ? %).
+     assumption
+    ]
+  ]
+qed.
+
+theorem monotonic_log: monotonic nat le log.
+unfold monotonic.intros.
+elim (le_to_or_lt_eq ? ? H) 0
+  [cases x;intro
+    [apply le_O_n
+    |apply lt_S_to_le.
+     apply (lt_exp_to_lt (S(S O)))
+      [apply le_n
+      |apply (le_to_lt_to_lt ? (S n))
+        [apply le_exp_log.
+         apply lt_O_S
+        |apply (trans_lt ? y)
+          [assumption
+          |apply lt_exp_log
+          ]
+        ]
+      ]
+    ]
+  |intro.rewrite < H1.apply le_n
+  ]
+qed.
+
+theorem lt_O_fact: \forall n. O < fact n.
+intro.elim n
+  [simplify.apply lt_O_S
+  |rewrite > factS.
+   rewrite > (times_n_O O).
+   apply lt_times
+    [apply lt_O_S
+    |assumption
+    ]
+  ]
+qed.
+
+theorem fact2: \forall n.O < n \to
+(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
+intros.elim H
+  [simplify.apply le_S.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite > factS.
+   rewrite < assoc_times.
+   rewrite > factS.
+   rewrite < times_SSO in ⊢ (? ? %).
+   apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
+    [rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > exp_S.
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     apply lt_times_r.
+     rewrite > exp_S.
+     rewrite > assoc_times.
+     rewrite > sym_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply lt_times_r.
+     rewrite > sym_times.
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     apply lt_times_r.
+     rewrite < assoc_times.
+     rewrite < assoc_times.
+     rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > sym_times in ⊢ (? ? %).
+     apply lt_times_r.
+     rewrite < assoc_times.
+     rewrite < sym_times.
+     rewrite < assoc_times.
+     assumption
+    |apply lt_times_l1
+      [rewrite > (times_n_O O) in ⊢ (? % ?).
+       apply lt_times
+        [rewrite > (times_n_O O) in ⊢ (? % ?).
+         apply lt_times
+          [apply lt_O_S
+          |apply lt_O_S
+          ]
+        |apply lt_O_fact
+        ]
+      |apply le_n
+      ]
+    ]
+  ]
+qed.
+
+theorem lt_O_log: \forall n. S O < n \to O < log n.
+intros.elim H
+  [simplify.apply lt_O_S
+  |apply (lt_to_le_to_lt ? (log n1))
+    [assumption
+    |apply monotonic_log.
+     apply le_n_Sn
+    ]
+  ]
+qed.
+
+theorem log_fact_SSSO: log (fact (S(S(S O)))) = S (S O).
+reflexivity.
+qed.
+
+lemma exp_SSO_SSO: exp (S(S O)) (S(S O)) = S(S(S(S O))).
+reflexivity.
+qed.
+(*
+theorem log_fact_SSSSO: log (fact (S(S(S(S O))))) = S(S(S(S O))).
+reflexivity.
+qed.
+*)
+theorem log_fact_SSSSSO: log (fact (S(S(S(S(S O)))))) = S(S(S(S O))).
+reflexivity.
+qed.
+
+theorem bof_bof: \forall n.(S(S(S(S O)))) < n \to 
+n \le (S(S(S(S(S(S(S(S O)))))))) \to log (fact n) < n*log n - n.
+intros.
+elim H
+  [rewrite > factS in ⊢ (? (? %) ?). 
+   rewrite > factS in ⊢ (? (? (? ? %)) ?).
+   rewrite < assoc_times in ⊢ (? (? %) ?).
+   rewrite < sym_times in ⊢ (? (? (? % ?)) ?).
+   rewrite > assoc_times in ⊢ (? (? %) ?).
+   change with (exp (S(S O)) (S(S O))) in ⊢ (? (? (? % ?)) ?).
+theorem bof: \forall n.(S(S(S(S O))))) < n \to log (fact n) < n*log n - n.
+intro.apply (nat_elim1 n).
+intros.
+elim (lt_O_to_or_eq_S m)
+  [elim H2.clear H2.
+   elim H4.clear H4.
+   rewrite > H2.
+   apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
+    [apply monotonic_log.
+     apply fact1
+    |rewrite > assoc_times in ⊢ (? (? %) ?).
+     rewrite > log_exp.
+     apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
+      [apply le_plus_r.
+       apply log_times
+      |rewrite > plus_n_Sm.
+       rewrite > log_SSO.
+       rewrite < times_n_Sm.
+       apply (le_to_lt_to_lt ? ((S(S O))*a+(log a!+(a*log a-a))))
+        [apply le_plus_r.
+         apply le_plus_r.
+         apply H.assumption
+        |apply (lt_to_le_to_lt ? ((S(S O))*a+((a*log a-a)+(a*log a-a))))
+          [apply lt_plus_r.
+           apply lt_plus_l.
+           apply H.
+           assumption.
+          |rewrite > times_SSO_n.
+           rewrite > distr_times_minus.
+           rewrite > sym_plus.
+           rewrite > plus_minus
+            [rewrite > sym_plus.
+             rewrite < assoc_times.
+             apply le_n
+            |rewrite < assoc_times.
+             rewrite > times_n_SO in ⊢ (? % ?).
+             apply le_times
+              [apply le_n
+              |apply lt_O_log.
+               apply (lt_times_n_to_lt_r (S(S O)))
+                [apply lt_O_S
+                |rewrite < times_n_SO.
+                 rewrite < H2.
+                 assumption
+                ]
+              ]
+            ]
+          ]
+          
+             .
+          ]
+        |
+           rewrite < eq_plus_minus_minus_plus.
+           
+       rewrite > assoc_plus.
+       apply lt_plus_r.
+       rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
+       change with
+        (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
+       apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
+        [apply le_S_S.
+         apply lt_plus_r.
+         apply lt_times_r.
+         apply H.
+         assumption
+        |
+        
+theorem stirling: \forall n,k.k \le n \to
+log (fact n) < n*log n - n + k*log n.
+intro.
+apply (nat_elim1 n).
+intros.
+elim (lt_O_to_or_eq_S m)
+  [elim H2.clear H2.
+   elim H4.clear H4.
+   rewrite > H2.
+   apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
+    [apply monotonic_log.
+     apply fact1
+    |rewrite > assoc_times in ⊢ (? (? %) ?).
+     rewrite > log_exp.
+     apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
+      [apply le_plus_r.
+       apply log_times
+      |rewrite < plus_n_Sm.
+       rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
+       change with
+        (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
+       apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
+        [apply le_S_S.
+         apply lt_plus_r.
+         apply lt_times_r.
+         apply H.
+         assumption
+        |
+        
+          [
+       
+       a*log a-a+k*log a
+       
index 78dc50318197c3dbc449c50d3e757e868aec527d..b002d78cccdedd6ad690ffeea67aaa0402c14288 100644 (file)
@@ -126,6 +126,23 @@ apply nat_elim2; intros; simplify
   ]
 qed.
 
+theorem leb_true_to_le:\forall n,m.
+leb n m = true \to (n \le m).
+intros 2.
+apply leb_elim
+  [intros.assumption
+  |intros.destruct H1.
+  ]
+qed.
+
+theorem leb_false_to_not_le:\forall n,m.
+leb n m = false \to \lnot (n \le m).
+intros 2.
+apply leb_elim
+  [intros.destruct H1
+  |intros.assumption
+  ]
+qed.
 (*
 theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m. 
 intros.
index f7f2883d590a8118ae6a39a8c348a75dcb2ff565..0323b18fb17849949b5ce4a49e3b33476f14fcec 100644 (file)
@@ -325,6 +325,31 @@ rewrite > (div_mod m n) in \vdash (? ? %)
   ]
 qed.
 
+theorem or_div_mod: \forall n,q. O < q \to
+((S (n \mod q)=q) \land S n = (S (div n q)) * q \lor
+((S (n \mod q)<q) \land S n= (div n q) * q + S (n\mod q))).
+intros.
+elim (le_to_or_lt_eq ? ? (lt_mod_m_m n q H))
+  [right.split
+    [assumption
+    |rewrite < plus_n_Sm.
+     apply eq_f.
+     apply div_mod.
+     assumption
+    ]
+  |left.split
+    [assumption
+    |simplify.
+     rewrite > sym_plus.
+     rewrite < H1 in ⊢ (? ? ? (? ? %)).
+     rewrite < plus_n_Sm.
+     apply eq_f.
+     apply div_mod.
+     assumption
+    ]
+  ]
+qed.
+
 (* injectivity *)
 theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
 change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
index ab7d8242e1e5752573c61e187807a4aeeecfdbab..1e5988b35de64d1a9eba560dadd53e6929e98f15 100644 (file)
@@ -55,7 +55,6 @@ intro.apply (nat_case n)
 qed.
 *)
 
-
 (*this obvious property is useful because simplify, sometimes,
   "simplifies too much", and doesn't allow to obtain this simple result.
  *)
@@ -136,7 +135,6 @@ elim (m)
 ]
 qed.
   
-
 lemma totient_card: \forall n.
 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
 intros.
index 193478c0fd6706ddc075aa2d6402051f553489e8..49efe8525504d4f431e81de36ea702f7c9d46f76 100644 (file)
@@ -40,6 +40,12 @@ theorem exp_n_SO : \forall n:nat. n = n \sup (S O).
 intro.simplify.rewrite < times_n_SO.reflexivity.
 qed.
 
+theorem exp_SSO: \forall n. exp n (S(S O)) = n*n.
+intro.simplify.
+rewrite < times_n_SO.
+reflexivity.
+qed.
+
 theorem exp_exp_times : \forall n,p,q:nat. 
 (n \sup p) \sup q = n \sup (p * q).
 intros.
@@ -164,7 +170,22 @@ apply nat_elim2;intros
   ]
 qed.
 
-
+theorem lt_exp_to_lt: 
+\forall a,n,m. S O < a \to exp a n < exp a m \to n < m.
+intros.
+elim (le_to_or_lt_eq n m)
+  [assumption
+  |apply False_ind.
+   apply (lt_to_not_eq ? ? H1).
+   rewrite < H2.
+   reflexivity
+  |apply (le_exp_to_le a)
+    [assumption
+    |apply lt_to_le.
+     assumption
+    ]
+  ]
+qed.
      
    
    
diff --git a/helm/software/matita/library/nat/factorial2.ma b/helm/software/matita/library/nat/factorial2.ma
new file mode 100644 (file)
index 0000000..4f3631c
--- /dev/null
@@ -0,0 +1,177 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/factorial2".
+
+include "nat/exp.ma".
+include "nat/factorial.ma".
+
+theorem factS: \forall n. fact (S n) = (S n)*(fact n).
+intro.simplify.reflexivity.
+qed.
+
+theorem exp_S: \forall n,m. exp m (S n) = m*exp m n.
+intros.reflexivity.
+qed.
+
+lemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
+intro.simplify.rewrite < plus_n_Sm.reflexivity.
+qed.
+
+theorem fact1: \forall n.
+fact ((S(S O))*n) \le (exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n).
+intro.elim n
+  [rewrite < times_n_O.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite > factS.
+   rewrite < assoc_times.
+   rewrite > factS.
+   apply (trans_le ? (((S(S O))*(S n1))*((S(S O))*(S n1))*(fact (((S(S O))*n1)))))
+    [apply le_times_l.
+     rewrite > times_SSO.
+     apply le_times_r.
+     apply le_n_Sn
+    |rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > exp_S. 
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite < assoc_times.
+     rewrite < assoc_times.
+     rewrite < sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > exp_S. 
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite > sym_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < assoc_times in ⊢ (? ? %).
+     rewrite < sym_times in ⊢ (? ? (? (? % ?) ?)).
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply le_times_r.
+     rewrite > sym_times in ⊢ (? ? (? ? %)).
+     rewrite > sym_times in ⊢ (? ? %).
+     assumption
+    ]
+  ]
+qed.
+
+theorem lt_O_fact: \forall n. O < fact n.
+intro.elim n
+  [simplify.apply lt_O_S
+  |rewrite > factS.
+   rewrite > (times_n_O O).
+   apply lt_times
+    [apply lt_O_S
+    |assumption
+    ]
+  ]
+qed.
+
+theorem fact2: \forall n.O < n \to
+(exp (S(S O)) ((S(S O))*n))*(fact n)*(fact n) < fact (S((S(S O))*n)).
+intros.elim H
+  [simplify.apply le_S.apply le_n
+  |rewrite > times_SSO.
+   rewrite > factS.
+   rewrite > factS.
+   rewrite < assoc_times.
+   rewrite > factS.
+   rewrite < times_SSO in ⊢ (? ? %).
+   apply (trans_lt ? (((S(S O))*S n1)*((S(S O))*S n1*(S ((S(S O))*n1))!)))
+    [rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > exp_S.
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     apply lt_times_r.
+     rewrite > exp_S.
+     rewrite > assoc_times.
+     rewrite > sym_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     rewrite > assoc_times in ⊢ (? ? %).
+     apply lt_times_r.
+     rewrite > sym_times.
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     apply lt_times_r.
+     rewrite < assoc_times.
+     rewrite < assoc_times.
+     rewrite > sym_times in ⊢ (? (? (? % ?) ?) ?).
+     rewrite > assoc_times.
+     rewrite > assoc_times.
+     rewrite > sym_times in ⊢ (? ? %).
+     apply lt_times_r.
+     rewrite < assoc_times.
+     rewrite < sym_times.
+     rewrite < assoc_times.
+     assumption
+    |apply lt_times_l1
+      [rewrite > (times_n_O O) in ⊢ (? % ?).
+       apply lt_times
+        [rewrite > (times_n_O O) in ⊢ (? % ?).
+         apply lt_times
+          [apply lt_O_S
+          |apply lt_O_S
+          ]
+        |apply lt_O_fact
+        ]
+      |apply le_n
+      ]
+    ]
+  ]
+qed.
+
+(*
+theorem stirling: \forall n,k.k \le n \to
+log (fact n) < n*log n - n + k*log n.
+intro.
+apply (nat_elim1 n).
+intros.
+elim (lt_O_to_or_eq_S m)
+  [elim H2.clear H2.
+   elim H4.clear H4.
+   rewrite > H2.
+   apply (le_to_lt_to_lt ? (log ((exp (S(S O)) ((S(S O))*a))*(fact a)*(fact a))))
+    [apply monotonic_log.
+     apply fact1
+    |rewrite > assoc_times in ⊢ (? (? %) ?).
+     rewrite > log_exp.
+     apply (le_to_lt_to_lt ? ((S(S O))*a+S(log a!+log a!)))
+      [apply le_plus_r.
+       apply log_times
+      |rewrite < plus_n_Sm.
+       rewrite > plus_n_O in ⊢ (? (? (? ? (? ? %))) ?).
+       change with
+        (S((S(S O))*a+((S(S O))*log a!)) < (S(S O))*a*log ((S(S O))*a)-(S(S O))*a+k*log ((S(S O))*a)).
+       apply (trans_lt ? (S ((S(S O))*a+(S(S O))*(a*log a-a+k*log a))))
+        [apply le_S_S.
+         apply lt_plus_r.
+         apply lt_times_r.
+         apply H.
+         assumption
+        |
+        
+          [
+       
+       a*log a-a+k*log a
+       
+*)
\ No newline at end of file
index 14696ca2891d7322622f2b7aabd2a1031fc36572..8c50d1d7db1e5612e160776b39a59e55ab21fece 100644 (file)
 set "baseuri" "cic:/matita/nat/factorization".
 
 include "nat/ord.ma".
-include "nat/gcd.ma".
-include "nat/nth_prime.ma".
 
 (* the following factorization algorithm looks for the largest prime
    factor. *)
 definition max_prime_factor \def \lambda n:nat.
 (max n (\lambda p:nat.eqb (n \mod (nth_prime p)) O)).
 
+theorem lt_SO_max_prime: \forall m. S O <  m \to 
+S O < max m (λi:nat.primeb i∧divides_b i m).
+intros.
+apply (lt_to_le_to_lt ? (smallest_factor m))
+  [apply lt_SO_smallest_factor.assumption
+  |apply f_m_to_le_max
+    [apply le_smallest_factor_n
+    |apply true_to_true_to_andb_true
+      [apply prime_to_primeb_true.
+       apply prime_smallest_factor_n.
+       assumption
+      |apply divides_to_divides_b_true
+        [apply lt_O_smallest_factor.apply lt_to_le.assumption
+        |apply divides_smallest_factor_n.
+         apply lt_to_le.assumption
+        ]
+      ]
+    ]
+  ]
+qed.
 (* max_prime_factor is indeed a factor *)
 theorem divides_max_prime_factor_n:
   \forall n:nat. (S O) < n
@@ -40,7 +58,6 @@ cut (\exists i. nth_prime i = smallest_factor n);
       | rewrite > H1;
         apply le_smallest_factor_n; ]
     | rewrite > H1;
-      (*CSC: simplify here does something nasty! *)
       change with (divides_b (smallest_factor n) n = true);
       apply divides_to_divides_b_true;
       [ apply (trans_lt ? (S O));
@@ -356,7 +373,7 @@ theorem defactorize_factorize: \forall n:nat.defactorize (factorize n) = n.
 intro.
 apply (nat_case n).reflexivity.
 intro.apply (nat_case m).reflexivity.
-intro.(*CSC: simplify here does something really nasty *)
+intro.
 change with  
 (let p \def (max (S(S m1)) (\lambda p:nat.eqb ((S(S m1)) \mod (nth_prime p)) O)) in
 defactorize (match p_ord (S(S m1)) (nth_prime p) with
@@ -377,7 +394,6 @@ simplify.
 cut ((S(S m1)) = (nth_prime p) \sup q *r).
 cut (O<r).
 rewrite > defactorize_aux_factorize_aux.
-(*CSC: simplify here does something really nasty *)
 change with (r*(nth_prime p) \sup (S (pred q)) = (S(S m1))).
 cut ((S (pred q)) = q).
 rewrite > Hcut2.
@@ -395,7 +411,6 @@ apply (divides_max_prime_factor_n (S (S m1))).
 unfold lt.apply le_S_S.apply le_S_S. apply le_O_n.
 cut ((S(S m1)) = r).
 rewrite > Hcut3 in \vdash (? (? ? %)).
-(*CSC: simplify here does something really nasty *)
 change with (nth_prime p \divides r \to False).
 intro.
 apply (p_ord_aux_to_not_mod_O (S(S m1)) (S(S m1)) (nth_prime p) q r).
@@ -472,30 +487,6 @@ apply (witness ? ? (n2* (nth_prime i) \sup n)).
 reflexivity.
 qed.
 
-theorem divides_exp_to_divides: 
-\forall p,n,m:nat. prime p \to 
-p \divides n \sup m \to p \divides n.
-intros 3.elim m.simplify in H1.
-apply (transitive_divides p (S O)).assumption.
-apply divides_SO_n.
-cut (p \divides n \lor p \divides n \sup n1).
-elim Hcut.assumption.
-apply H.assumption.assumption.
-apply divides_times_to_divides.assumption.
-exact H2.
-qed.
-
-theorem divides_exp_to_eq: 
-\forall p,q,m:nat. prime p \to prime q \to
-p \divides q \sup m \to p = q.
-intros.
-unfold prime in H1.
-elim H1.apply H4.
-apply (divides_exp_to_divides p q m).
-assumption.assumption.
-unfold prime in H.elim H.assumption.
-qed.
-
 lemma eq_p_max: \forall n,p,r:nat. O < n \to
 O < r \to
 r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to
@@ -762,7 +753,7 @@ exact H1.
 qed.
 
 theorem factorize_defactorize: 
-\forall f,g: nat_fact_all. factorize (defactorize f) = f.
+\forall f: nat_fact_all. factorize (defactorize f) = f.
 intros.
 apply injective_defactorize.
 apply defactorize_factorize.
index ded9d4843ac6cf3cb4da2b4f564568db2df2e02b..9bbce8144ff8885a7c7346bdb9b7937983bd5f7e 100644 (file)
@@ -749,6 +749,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
+(* primes and divides *)
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 n \divides p \lor n \divides q.
 intros.
@@ -802,6 +803,30 @@ cut (n \divides p \lor n \ndivides p)
   ]
 qed.
 
+theorem divides_exp_to_divides: 
+\forall p,n,m:nat. prime p \to 
+p \divides n \sup m \to p \divides n.
+intros 3.elim m.simplify in H1.
+apply (transitive_divides p (S O)).assumption.
+apply divides_SO_n.
+cut (p \divides n \lor p \divides n \sup n1).
+elim Hcut.assumption.
+apply H.assumption.assumption.
+apply divides_times_to_divides.assumption.
+exact H2.
+qed.
+
+theorem divides_exp_to_eq: 
+\forall p,q,m:nat. prime p \to prime q \to
+p \divides q \sup m \to p = q.
+intros.
+unfold prime in H1.
+elim H1.apply H4.
+apply (divides_exp_to_divides p q m).
+assumption.assumption.
+unfold prime in H.elim H.assumption.
+qed.
+
 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
 intros.
@@ -877,4 +902,5 @@ cut (n \divides p \lor n \ndivides p)
  |apply (decidable_divides n p).
   assumption.
  ]
-qed.
\ No newline at end of file
+qed.
+
index 3a9adc231262f58a9bfc5da65783cf790b4e9a89..249957f1b3bc44453e46caf4099361818b4cbbff 100644 (file)
@@ -205,6 +205,47 @@ elim H
 ]
 qed.
 
+(* a therem slightly more general than the previous one *)
+theorem or_false_eq_baseA_to_eq_iter_p_gen: \forall A:Type. \forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to A. \forall baseA:A. \forall plusA: A \to A \to A.
+(\forall a. plusA baseA a = a) \to
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = baseA)
+\to iter_p_gen m p A g baseA plusA = iter_p_gen n p A g baseA plusA.
+intros 9.
+elim H1
+[reflexivity
+|apply (bool_elim ? (p n1));intro
+  [elim (H4 n1)
+    [apply False_ind.
+     apply not_eq_true_false.
+     rewrite < H5.
+     rewrite < H6.
+     reflexivity
+    |rewrite > true_to_iter_p_gen_Sn
+      [rewrite > H6.
+       rewrite > H.
+       apply H3.intros.
+       apply H4
+        [assumption
+        |apply le_S.assumption
+        ]
+      |assumption
+      ]
+    |assumption
+    |apply le_n
+    ]
+  |rewrite > false_to_iter_p_gen_Sn
+    [apply H3.intros.
+     apply H4
+      [assumption
+      |apply le_S.assumption
+      ]
+    |assumption
+    ]
+  ]
+]
+qed.
+    
 theorem iter_p_gen2 : 
 \forall n,m:nat.
 \forall p1,p2:nat \to bool.
@@ -1631,7 +1672,82 @@ apply (trans_eq ? ?
 ]
 qed.
 
-
+theorem iter_p_gen_iter_p_gen: 
+\forall A:Type.
+\forall baseA: A.
+\forall plusA: A \to A \to A. 
+(symmetric A plusA) \to 
+(associative A plusA) \to 
+(\forall a:A.(plusA a  baseA) = a)\to
+\forall g: nat \to nat \to A.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to 
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+iter_p_gen n p11 A 
+  (\lambda x:nat.iter_p_gen m (p12 x) A (\lambda y. g x y) baseA plusA) 
+  baseA plusA =
+iter_p_gen m p21 A 
+  (\lambda y:nat.iter_p_gen n (p22 y) A  (\lambda x. g x y) baseA plusA )
+  baseA plusA.
+intros.
+apply (iter_p_gen_2_eq A baseA plusA H H1 H2 (\lambda x,y. g x y) (\lambda x,y.y) (\lambda x,y.x) (\lambda x,y.y) (\lambda x,y.x)
+       n m m n p11 p21 p12 p22)
+  [intros.split
+    [split
+      [split
+        [split
+          [split
+            [apply (andb_true_true ? (p12 j i)).
+             rewrite > H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            |apply (andb_true_true_r (p11 j)).
+             rewrite > H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            ]
+          |reflexivity
+          ]
+        |reflexivity
+        ]
+      |assumption
+      ]
+    |assumption
+    ]
+  |intros.split
+    [split
+      [split
+        [split
+          [split
+            [apply (andb_true_true ? (p22 j i)).
+             rewrite < H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            |apply (andb_true_true_r (p21 j)).
+             rewrite < H3
+              [rewrite > H6.rewrite > H7.reflexivity
+              |assumption
+              |assumption
+              ]
+            ]
+          |reflexivity
+          ]
+        |reflexivity
+        ]
+      |assumption
+      ]
+    |assumption
+    ]
+  ]
+qed.
 
 
 
index 6ad389346a8b9e2347493f1b0b3299866feb7869..f391c85a9686e77900e11bee558cd07987e3fbf8 100644 (file)
@@ -146,6 +146,18 @@ apply nat_elim2;intros
   ]
 qed.
 
+theorem le_S_times_SSO: \forall n,m.O < m \to
+n \le m \to S n \le (S(S O))*m.
+intros.
+simplify.
+rewrite > plus_n_O.
+simplify.rewrite > plus_n_Sm.
+apply le_plus
+  [assumption
+  |rewrite < plus_n_O.
+   assumption
+  ]
+qed.
 (*0 and times *)
 theorem O_lt_const_to_le_times_const:  \forall a,c:nat.
 O \lt c \to a \le a*c.
diff --git a/helm/software/matita/library/nat/log.ma b/helm/software/matita/library/nat/log.ma
new file mode 100644 (file)
index 0000000..53b1245
--- /dev/null
@@ -0,0 +1,274 @@
+(**************************************************************************)
+(*       ___                                                               *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        Matita is distributed under the terms of the          *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/log".
+
+include "datatypes/constructors.ma".
+include "nat/minimization.ma".
+include "nat/relevant_equations.ma".
+include "nat/primes.ma".
+
+definition log \def \lambda p,n.
+max n (\lambda x.leb (exp p x) n).
+
+theorem le_exp_log: \forall p,n. O < n \to
+exp p (log p n) \le n.
+intros.
+apply leb_true_to_le.
+unfold log.
+apply (f_max_true (\lambda x.leb (exp p x) n)).
+apply (ex_intro ? ? O).
+split
+  [apply le_O_n
+  |apply le_to_leb_true.simplify.assumption
+  ]
+qed.
+
+theorem log_SO: \forall n. S O < n \to log n (S O) = O.
+intros.
+apply sym_eq.apply le_n_O_to_eq.
+apply (le_exp_to_le n)
+  [assumption
+  |simplify in ⊢ (? ? %).
+   apply le_exp_log.
+   apply le_n
+  ]
+qed.
+
+theorem lt_log_n_n: \forall p, n. S O < p \to O < n \to log p n < n.
+intros.
+cut (log p n \le n)
+  [elim (le_to_or_lt_eq ? ? Hcut)
+    [assumption
+    |absurd (exp p n \le n)
+      [rewrite < H2 in ⊢ (? (? ? %) ?).
+       apply le_exp_log.
+       assumption
+      |apply lt_to_not_le.
+       apply lt_m_exp_nm.
+       assumption
+      ]
+    ]
+  |unfold log.apply le_max_n
+  ]
+qed.
+
+theorem lt_O_log: \forall p,n. O < n \to p \le n \to O < log p n.
+intros.
+unfold log.
+apply not_lt_to_le.
+intro.
+apply (leb_false_to_not_le ? ? ? H1).
+rewrite > (exp_n_SO p).
+apply (lt_max_to_false ? ? ? H2).
+assumption.
+qed.
+
+theorem le_log_n_n: \forall p,n. S O < p \to log p n \le n.
+intros.
+cases n
+  [apply le_n
+  |apply lt_to_le.
+   apply lt_log_n_n
+    [assumption|apply lt_O_S]
+  ]
+qed.
+
+theorem lt_exp_log: \forall p,n. S O < p \to n < exp p (S (log p n)).
+intros.cases n
+  [simplify.rewrite < times_n_SO.apply lt_to_le.assumption
+  |apply not_le_to_lt.
+   apply leb_false_to_not_le.
+   apply (lt_max_to_false ? (S n1) (S (log p (S n1))))
+    [apply le_S_S.apply le_n
+    |apply lt_log_n_n
+      [assumption|apply lt_O_S]
+    ]
+  ]
+qed.
+
+theorem log_times1: \forall p,n,m. S O < p \to O < n \to O < m \to
+log p (n*m) \le S(log p n+log p m).
+intros.
+unfold in ⊢ (? (% ? ?) ?).
+apply f_false_to_le_max
+  [apply (ex_intro ? ? O).
+   split
+    [apply le_O_n
+    |apply le_to_leb_true.
+     simplify.
+     rewrite > times_n_SO.
+     apply le_times;assumption
+    ]
+  |intros.
+   apply lt_to_leb_false.
+   apply (lt_to_le_to_lt ? ((exp p (S(log p n)))*(exp p (S(log p m)))))
+    [apply lt_times;apply lt_exp_log;assumption
+    |rewrite < exp_plus_times.
+     apply le_exp
+      [apply lt_to_le.assumption
+      |simplify.
+       rewrite < plus_n_Sm.
+       assumption
+      ]
+    ]
+  ]
+qed.
+  
+theorem log_times: \forall p,n,m.S O < p \to log p (n*m) \le S(log p n+log p m).
+intros.
+cases n
+  [apply le_O_n
+  |cases m
+    [rewrite < times_n_O.
+     apply le_O_n
+    |apply log_times1
+      [assumption
+      |apply lt_O_S
+      |apply lt_O_S
+      ]
+    ]
+  ]
+qed.
+
+theorem log_exp: \forall p,n,m.S O < p \to O < m \to
+log p ((exp p n)*m)=n+log p m.
+intros.
+unfold log in ⊢ (? ? (% ? ?) ?).
+apply max_spec_to_max.
+unfold max_spec.
+split
+  [split
+    [elim n
+      [simplify.
+       rewrite < plus_n_O.
+       apply le_log_n_n.
+       assumption
+      |simplify.
+       rewrite > assoc_times.
+       apply (trans_le ? ((S(S O))*(p\sup n1*m)))
+        [apply le_S_times_SSO
+          [rewrite > (times_n_O O) in ⊢ (? % ?).
+           apply lt_times
+            [apply lt_O_exp.
+             apply lt_to_le.
+             assumption
+            |assumption
+            ]
+          |assumption
+          ]
+        |apply le_times
+          [assumption
+          |apply le_n
+          ]
+        ]
+      ]
+    |simplify.
+     apply le_to_leb_true.
+     rewrite > exp_plus_times.
+     apply le_times_r.
+     apply le_exp_log.
+     assumption
+    ]
+  |intros.
+   simplify.
+   apply lt_to_leb_false.
+   apply (lt_to_le_to_lt ? ((exp p n)*(exp p (S(log p m)))))
+    [apply lt_times_r1
+      [apply lt_O_exp.apply lt_to_le.assumption
+      |apply lt_exp_log.assumption
+      ]
+    |rewrite < exp_plus_times.
+     apply le_exp
+      [apply lt_to_le.assumption
+      |rewrite < plus_n_Sm.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem le_log: \forall p,n,m. S O < p \to O < n \to n \le m \to 
+log p n \le log p m.
+intros.
+apply le_S_S_to_le.
+apply (lt_exp_to_lt p)
+  [assumption
+  |apply (le_to_lt_to_lt ? n)
+    [apply le_exp_log.
+     assumption
+    |apply (le_to_lt_to_lt ? m)
+      [assumption
+      |apply lt_exp_log.
+       assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem log_n_n: \forall n. S O < n \to log n n = S O.
+intros.
+rewrite > exp_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > times_n_SO in ⊢ (? ? (? ? %) ?).
+rewrite > log_exp
+  [rewrite > log_SO
+    [reflexivity
+    |assumption
+    ]
+  |assumption
+  |apply le_n
+  ]
+qed.
+
+theorem log_i_SSOn: \forall n,i. S O < n \to n < i \to i \le ((S(S O))*n) \to
+log i ((S(S O))*n) = S O.
+intros.
+apply antisymmetric_le
+  [apply not_lt_to_le.intro.
+   apply (lt_to_not_le ((S(S O)) * n) (exp i (S(S O))))
+    [rewrite > exp_SSO.
+     apply lt_times
+      [apply (le_to_lt_to_lt ? n);assumption
+      |assumption
+      ]
+    |apply (trans_le ? (exp i (log i ((S(S O))*n))))
+      [apply le_exp
+        [apply (ltn_to_ltO ? ? H1)
+        |assumption
+        ]
+      |apply le_exp_log.
+       rewrite > (times_n_O O) in ⊢ (? % ?).
+       apply lt_times
+        [apply lt_O_S
+        |apply lt_to_le.assumption
+        ]
+      ]
+    ]
+  |apply (trans_le ? (log i i))
+    [rewrite < (log_n_n i) in ⊢ (? % ?)
+      [apply le_log
+        [apply (trans_lt ? n);assumption
+        |apply (ltn_to_ltO ? ? H1)
+        |apply le_n
+        ]
+      |apply (trans_lt ? n);assumption
+      ]
+    |apply le_log
+      [apply (trans_lt ? n);assumption
+      |apply (ltn_to_ltO ? ? H1)
+      |assumption
+      ]
+    ]
+  ]
+qed.
index a568ca408be94412a0203a82abf170709edfaa05..623f30295922c7d6ff5fe5d23369b960f5e7c2dc 100644 (file)
@@ -239,6 +239,27 @@ apply (nat_case n)
   ]
 qed.
 
+theorem le_times_to_le_div: \forall a,b,c:nat.
+O \lt b \to (b*c) \le a \to c \le (a /b).
+intros.
+apply lt_S_to_le.
+apply (lt_times_n_to_lt b)
+  [assumption
+  |rewrite > sym_times.
+   apply (le_to_lt_to_lt ? a)
+    [assumption
+    |simplify.
+     rewrite > sym_plus.
+     rewrite > (div_mod a b) in ⊢ (? % ?)
+      [apply lt_plus_r.
+       apply lt_mod_m_m.
+       assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
 theorem nat_compare_times_l : \forall n,p,q:nat. 
 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
 intros.apply nat_compare_elim.intro.
@@ -320,7 +341,81 @@ apply (trans_lt ? (S O)).
 unfold lt. apply le_n.assumption.
 qed.
 
+theorem eq_div_div_div_times: \forall n,m,q. O < n \to O < m \to
+q/n/m = q/(n*m).
+intros.
+apply (div_mod_spec_to_eq q (n*m) ? (q\mod n+n*(q/n\mod m)) ? (mod q (n*m)))
+  [apply div_mod_spec_intro
+    [apply (lt_to_le_to_lt ? (n*(S (q/n\mod m))))
+      [rewrite < times_n_Sm.
+       apply lt_plus_l.
+       apply lt_mod_m_m.
+       assumption
+      |apply le_times_r.
+       apply lt_mod_m_m.
+       assumption
+      ]
+    |rewrite > sym_times in ⊢ (? ? ? (? (? ? %) ?)).
+     rewrite < assoc_times.
+     rewrite > (eq_times_div_minus_mod ? ? H1).
+     rewrite > sym_times.
+     rewrite > distributive_times_minus.
+     rewrite > sym_times.
+     rewrite > (eq_times_div_minus_mod ? ? H).
+     rewrite < sym_plus in ⊢ (? ? ? (? ? %)).
+     rewrite < assoc_plus.
+     rewrite < plus_minus_m_m
+      [rewrite < plus_minus_m_m
+        [reflexivity
+        |apply (eq_plus_to_le ? ? ((q/n)*n)).
+         rewrite < sym_plus.
+         apply div_mod.
+         assumption
+        ]
+      |apply (trans_le ? (n*(q/n)))
+        [apply le_times_r.
+         apply (eq_plus_to_le ? ? ((q/n)/m*m)).
+         rewrite < sym_plus.
+         apply div_mod.
+         assumption
+        |rewrite > sym_times.
+         rewrite > eq_times_div_minus_mod
+          [apply le_n
+          |assumption
+          ]
+        ]
+      ]
+    ]
+  |apply div_mod_spec_div_mod.
+   rewrite > (times_n_O O).
+   apply lt_times;assumption
+  ]
+qed.
+
+theorem eq_div_div_div_div: \forall n,m,q. O < n \to O < m \to
+q/n/m = q/m/n.
+intros.
+apply (trans_eq ? ? (q/(n*m)))
+  [apply eq_div_div_div_times;assumption
+  |rewrite > sym_times.
+   apply sym_eq.
+   apply eq_div_div_div_times;assumption
+  ]
+qed.
 
+theorem SSO_mod: \forall n,m. O < m \to (S(S O))*n/m = (n/m)*(S(S O)) + mod ((S(S O))*n/m) (S(S O)).
+intros.
+rewrite < (lt_O_to_div_times n (S(S O))) in ⊢ (? ? ? (? (? (? % ?) ?) ?))
+  [rewrite > eq_div_div_div_div
+    [rewrite > sym_times in ⊢ (? ? ? (? (? (? (? % ?) ?) ?) ?)).
+     apply div_mod.
+     apply lt_O_S
+    |apply lt_O_S
+    |assumption
+    ]
+  |apply lt_O_S
+  ]
+qed.
 (* Forall a,b : N. 0 < b \to b * (a/b) <= a < b * (a/b +1) *)
 (* The theorem is shown in two different parts: *)
 
index 8b4b83c2fbc7d910fc9c3d91dbd4dc130e713c30..22d5030ddb37a12d032f66b489cd87aa7bc01780 100644 (file)
@@ -72,6 +72,76 @@ intro.simplify.rewrite < H3.
 rewrite > H2.simplify.apply le_n.
 qed.
 
+theorem max_f_g: \forall f,g,n. (\forall i. i \le n \to f i = g i) \to
+max n f = max n g.
+intros 3.
+elim n
+  [simplify.
+   rewrite > (H O)
+    [reflexivity
+    |apply le_n
+    ]
+  |simplify.
+   rewrite > H
+    [rewrite > H1
+      [reflexivity
+      |apply le_n
+      ]
+    |intros.
+     apply H1.
+     apply le_S.
+     assumption
+    ]
+  ]
+qed.
+
+theorem le_max_f_max_g: \forall f,g,n. (\forall i. i \le n \to f i = true \to g i =true) \to
+max n f \le max n g.
+intros 3.
+elim n
+  [simplify.
+   elim (f O);apply le_O_n
+  |simplify.
+   apply (bool_elim ? (f (S n1)));intro
+    [rewrite > (H1 (S n1) ? H2)
+      [apply le_n
+      |apply le_n
+      ]
+    |cases (g(S n1))
+      [simplify.
+       apply le_S.
+       apply le_max_n
+      |simplify.
+       apply H.
+       intros.
+       apply H1
+        [apply le_S.assumption
+        |assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+
+
+theorem max_O : \forall f:nat \to bool. \forall n:nat.
+(\forall i:nat. le i n \to f i = false) \to max n f = O.
+intros 2.elim n
+  [simplify.rewrite > H
+    [reflexivity
+    |apply le_O_n
+    ]
+  |simplify.rewrite > H1
+    [simplify.apply H.
+     intros.
+     apply H1.
+     apply le_S.
+     assumption
+    |apply le_n
+    ]
+  ]
+qed.
+
 theorem f_max_true : \forall f:nat \to bool. \forall n:nat.
 (\exists i:nat. le i n \land f i = true) \to f (max n f) = true. 
 intros 2.
@@ -95,6 +165,73 @@ rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
 reflexivity.
 qed.
 
+theorem exists_forall_le:\forall f,n. 
+(\exists i. i \le n \land f i = true) \lor
+(\forall i. i \le n \to f i = false).
+intros.
+elim n
+  [apply (bool_elim ? (f O));intro
+    [left.apply (ex_intro ? ? O).
+     split[apply le_n|assumption]
+    |right.intros.
+     apply (le_n_O_elim ? H1).
+     assumption
+    ]
+  |elim H
+    [elim H1.elim H2.
+     left.apply (ex_intro ? ? a).
+     split[apply le_S.assumption|assumption]
+    |apply (bool_elim ? (f (S n1)));intro
+      [left.apply (ex_intro ? ? (S n1)).
+       split[apply le_n|assumption]
+      |right.intros.
+       elim (le_to_or_lt_eq ? ? H3)
+        [apply H1.
+         apply le_S_S_to_le.
+         apply H4
+        |rewrite > H4.
+         assumption
+        ]
+      ]
+    ]
+  ]
+qed.
+     
+theorem exists_max_forall_false:\forall f,n. 
+((\exists i. i \le n \land f i = true) \land (f (max n f) = true))\lor
+((\forall i. i \le n \to f i = false) \land (max n f) = O).
+intros.
+elim (exists_forall_le f n)
+  [left.split
+    [assumption
+    |apply f_max_true.assumption
+    ]
+  |right.split
+    [assumption
+    |apply max_O.assumption
+    ]
+  ]
+qed.
+
+theorem false_to_lt_max: \forall f,n,m.O < n \to
+f n = false \to max m f \le n \to max m f < n.
+intros.
+elim (le_to_or_lt_eq ? ? H2)
+  [assumption
+  |elim (exists_max_forall_false f m)
+    [elim H4.
+     apply False_ind.
+     apply not_eq_true_false.
+     rewrite < H6.
+     rewrite > H3.
+     assumption
+    |elim H4.
+     rewrite > H6.
+     assumption
+    ]
+  ]
+qed.
+
 theorem lt_max_to_false : \forall f:nat \to bool. 
 \forall n,m:nat. (max n f) < m \to m \leq n \to f m = false.
 intros 2.
@@ -114,6 +251,18 @@ apply le_S_S_to_le.assumption.
 intro.rewrite > H7.assumption.
 qed.
 
+theorem f_false_to_le_max: \forall f,n,p. (∃i:nat.i≤n∧f i=true) \to
+(\forall m. p < m \to f m = false)
+\to max n f \le p.
+intros.
+apply not_lt_to_le.intro.
+apply not_eq_true_false.
+rewrite < (H1 ? H2).
+apply sym_eq.
+apply f_max_true.
+assumption.
+qed.
+
 definition max_spec \def \lambda f:nat \to bool.\lambda n,m: nat.
 m \le n \land (f m)=true \land (\forall i. m < i \to i \le n \to (f i = false)).
 
index 340e33a865fb809d8beb35e632f4e129fa2bd0dc..335550d0d6366f02d172c1f3aa6171d3ef6d171a 100644 (file)
@@ -17,6 +17,7 @@ set "baseuri" "cic:/matita/nat/ord".
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
 include "nat/nth_prime.ma".
+include "nat/gcd.ma". (* for some properties of divides *)
 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
 
 let rec p_ord_aux p n m \def
@@ -429,7 +430,165 @@ elim (le_to_or_lt_eq O (ord_rem n p))
   ]
 qed.
 
-(* p_ord_inv is the inverse of ord *)
+(* properties of ord e ord_rem *)
+
+theorem ord_times: \forall p,m,n.O<m \to O<n \to prime p \to
+ord (m*n) p = ord m p+ord n p.
+intros.unfold ord.
+rewrite > (p_ord_times ? ? ? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p))
+  [reflexivity
+  |assumption
+  |assumption
+  |assumption
+  |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+  |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+  ]
+qed.
+
+theorem ord_exp: \forall p,m.S O < p \to
+ord (exp p m) p = m.
+intros.
+unfold ord.
+rewrite > (p_ord_exp1 p (exp p m) m (S O))
+  [reflexivity
+  |apply lt_to_le.assumption
+  |intro.apply (lt_to_not_le ? ? H).
+   apply divides_to_le
+    [apply lt_O_S
+    |assumption
+    ]
+  |apply times_n_SO
+  ]
+qed.
+
+theorem not_divides_to_ord_O: 
+\forall p,m. prime p \to \lnot (divides p m) \to
+ord m p = O.
+intros.unfold ord.
+rewrite > (p_ord_exp1 p m O m)
+  [reflexivity
+  |apply prime_to_lt_O.assumption
+  |assumption
+  |simplify.apply plus_n_O
+  ]
+qed.
+
+theorem ord_O_to_not_divides: 
+\forall p,m. O < m \to prime p \to ord m p = O \to 
+\lnot (divides p m).
+intros.
+lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
+  [elim Hletin.
+   rewrite > H4.
+   rewrite > H2.
+   rewrite > sym_times.
+   rewrite < times_n_SO.
+   assumption
+  |apply prime_to_lt_SO.assumption
+  |assumption
+  |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+  ]
+qed.
+
+theorem divides_to_not_ord_O: 
+\forall p,m. O < m \to prime p \to divides p m \to
+\lnot(ord m p = O).
+intros.intro.
+apply (ord_O_to_not_divides ? ? H H1 H3).
+assumption.
+qed.
+
+theorem not_ord_O_to_divides: 
+\forall p,m. O < m \to prime p \to \lnot (ord m p = O) \to 
+divides p m.
+intros.
+rewrite > (exp_ord p) in ⊢ (? ? %)
+  [apply (trans_divides ? (exp p (ord m p)))
+    [generalize in match H2.
+     cases (ord m p);intro
+      [apply False_ind.apply H3.reflexivity
+      |simplify.autobatch
+      ]
+    |autobatch
+    ]
+  |apply prime_to_lt_SO.
+   assumption
+  |assumption
+  ]
+qed.
+
+theorem not_divides_ord_rem: \forall m,p.O< m \to S O < p \to
+\lnot (divides p (ord_rem m p)).
+intros.
+elim (p_ord_to_exp1 p m (ord m p) (ord_rem m p))
+  [assumption
+  |assumption
+  |assumption
+  |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
+  ]
+qed.
+
+theorem ord_ord_rem: \forall p,q,m. O < m \to 
+prime p \to prime q \to
+q < p \to ord (ord_rem m p) q = ord m q.
+intros.
+rewrite > (exp_ord p) in ⊢ (? ? ? (? % ?))
+  [rewrite > ord_times
+    [rewrite > not_divides_to_ord_O in ⊢ (? ? ? (? % ?))
+      [reflexivity
+      |assumption
+      |intro.
+       apply (lt_to_not_eq ? ? H3).
+       apply (divides_exp_to_eq ? ? ? H2 H1 H4)
+      ]
+    |apply lt_O_exp.
+     apply (ltn_to_ltO ? ? H3)
+    |apply lt_O_ord_rem
+      [elim H1.assumption
+      |assumption
+      
+      ]
+    |assumption
+    ]
+  |elim H1.assumption
+  |assumption
+  ]
+qed.
+
+theorem lt_ord_rem: \forall n,m. prime n \to O < m \to
+divides n m \to ord_rem m n < m.
+intros.
+elim (le_to_or_lt_eq (ord_rem m n) m)
+  [assumption
+  |apply False_ind.
+   apply (ord_O_to_not_divides ? ? H1 H ? H2).
+   apply (inj_exp_r n)
+    [apply prime_to_lt_SO.assumption
+    |apply (inj_times_l1 m)
+      [assumption
+      |rewrite > sym_times in ⊢ (? ? ? %).
+       rewrite < times_n_SO.
+       rewrite < H3 in ⊢ (? ? (? ? %) ?).
+       apply sym_eq.
+       apply exp_ord
+        [apply prime_to_lt_SO.assumption
+        |assumption
+        ]
+      ]
+    ]
+  |apply divides_to_le
+    [assumption
+    |apply divides_ord_rem
+      [apply prime_to_lt_SO.assumption
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+(* p_ord_inv is used to encode the pair ord and rem into 
+   a single natural number. *)
 definition p_ord_inv \def
 \lambda p,m,x.
   match p_ord x p with
index caecbe0632eb8bfd2219275403c012e000831743..799f8bf7c47b74c65575431e78d2f0b8f9662b9e 100644 (file)
@@ -325,6 +325,16 @@ intros.apply (le_to_lt_to_lt O n).
 apply le_O_n.assumption.
 qed.
 
+theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
+(S O) \lt n \to O \lt (pred n).
+intros.
+apply (ltn_to_ltO (pred (S O)) (pred n) ?).
+ apply (lt_pred (S O) n);
+ [ apply (lt_O_S O) 
+ | assumption
+ ]
+qed.
+
 theorem lt_O_n_elim: \forall n:nat. lt O n \to 
 \forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
 intro.elim n.apply False_ind.exact (not_le_Sn_O O H).
diff --git a/helm/software/matita/library/nat/pi_p.ma b/helm/software/matita/library/nat/pi_p.ma
new file mode 100644 (file)
index 0000000..e649f5f
--- /dev/null
@@ -0,0 +1,395 @@
+(**************************************************************************)
+(*       ___                                                             *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/nat/pi_p".
+
+include "nat/primes.ma".
+(* include "nat/ord.ma". *)
+include "nat/generic_iter_p.ma".
+(* include "nat/count.ma". necessary just to use bool_to_nat and bool_to_nat_andb*)
+include "nat/iteration2.ma".
+
+(* pi_p on nautral numbers is a specialization of iter_p_gen *)
+definition pi_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
+\lambda n, p, g. (iter_p_gen n p nat g (S O) times).
+
+theorem true_to_pi_p_Sn: 
+\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
+p n = true \to pi_p (S n) p g = (g n)*(pi_p n p g).
+intros.
+unfold pi_p.
+apply true_to_iter_p_gen_Sn.
+assumption.
+qed.
+   
+theorem false_to_pi_p_Sn: 
+\forall n:nat. \forall p:nat \to bool. \forall g:nat \to nat.
+p n = false \to pi_p (S n) p g = pi_p n p g.
+intros.
+unfold pi_p.
+apply false_to_iter_p_gen_Sn.
+assumption.
+qed.  
+
+theorem eq_pi_p: \forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to nat.\forall n.
+(\forall x.  x < n \to p1 x = p2 x) \to
+(\forall x.  x < n \to g1 x = g2 x) \to
+pi_p n p1 g1 = pi_p n p2 g2.
+intros.
+unfold pi_p.
+apply eq_iter_p_gen;
+assumption.
+qed.
+
+theorem eq_pi_p1: \forall p1,p2:nat \to bool.
+\forall g1,g2: nat \to nat.\forall n.
+(\forall x.  x < n \to p1 x = p2 x) \to
+(\forall x.  x < n \to p1 x = true \to g1 x = g2 x) \to
+pi_p n p1 g1 = pi_p n p2 g2.
+intros.
+unfold pi_p.
+apply eq_iter_p_gen1;
+assumption.
+qed.
+
+theorem pi_p_false: 
+\forall g: nat \to nat.\forall n.pi_p n (\lambda x.false) g = S O.
+intros.
+unfold pi_p.
+apply iter_p_gen_false.
+qed.
+
+theorem pi_p_times: \forall n,k:nat.\forall p:nat \to bool.
+\forall g: nat \to nat.
+pi_p (k+n) p g 
+= pi_p k (\lambda x.p (x+n)) (\lambda x.g (x+n)) * pi_p n p g.
+intros.
+unfold pi_p.
+apply (iter_p_gen_plusA nat n k p g (S O) times)
+[ apply sym_times.
+| intros.
+  apply sym_eq.
+  apply times_n_SO
+| apply associative_times
+]
+qed.
+
+theorem false_to_eq_pi_p: \forall n,m:nat.n \le m \to
+\forall p:nat \to bool.
+\forall g: nat \to nat. (\forall i:nat. n \le i \to i < m \to
+p i = false) \to pi_p m p g = pi_p n p g.
+intros.
+unfold pi_p.
+apply (false_to_eq_iter_p_gen);
+assumption.
+qed.
+
+theorem or_false_eq_SO_to_eq_pi_p: 
+\forall n,m:nat.\forall p:nat \to bool.
+\forall g: nat \to nat.
+n \le m \to (\forall i:nat. n \le i \to i < m \to p i = false \lor g i = S O)
+\to pi_p m p g = pi_p n p g.
+intros.
+unfold pi_p.
+apply or_false_eq_baseA_to_eq_iter_p_gen
+  [intros.simplify.rewrite < plus_n_O.reflexivity
+  |assumption
+  |assumption
+  ]
+qed.
+
+theorem pi_p2 : 
+\forall n,m:nat.
+\forall p1,p2:nat \to bool.
+\forall g: nat \to nat \to nat.
+pi_p (n*m) 
+  (\lambda x.andb (p1 (div x m)) (p2 (mod x m))) 
+  (\lambda x.g (div x m) (mod x m)) =
+pi_p n p1 
+  (\lambda x.pi_p m p2 (g x)).
+intros.
+unfold pi_p.
+apply (iter_p_gen2 n m p1 p2 nat g (S O) times)
+[ apply sym_times
+| apply associative_times
+| intros.
+  apply sym_eq.
+  apply times_n_SO
+]
+qed.
+
+theorem pi_p2' : 
+\forall n,m:nat.
+\forall p1:nat \to bool.
+\forall p2:nat \to nat \to bool.
+\forall g: nat \to nat \to nat.
+pi_p (n*m) 
+  (\lambda x.andb (p1 (div x m)) (p2 (div x m) (mod x  m))) 
+  (\lambda x.g (div x m) (mod x m)) =
+pi_p n p1 
+  (\lambda x.pi_p m (p2 x) (g x)).
+intros.
+unfold pi_p.
+apply (iter_p_gen2' n m p1 p2 nat g (S O) times)
+[ apply sym_times
+| apply associative_times
+| intros.
+  apply sym_eq.
+  apply times_n_SO
+]
+qed.
+
+lemma pi_p_gi: \forall g: nat \to nat.
+\forall n,i.\forall p:nat \to bool.i < n \to p i = true \to 
+pi_p n p g = g i * pi_p n (\lambda x. andb (p x) (notb (eqb x i))) g.
+intros.
+unfold pi_p.
+apply (iter_p_gen_gi)
+[ apply sym_times
+| apply associative_times
+| intros.
+  apply sym_eq.
+  apply times_n_SO
+| assumption
+| assumption
+]
+qed.
+
+theorem eq_pi_p_gh: 
+\forall g,h,h1: nat \to nat.\forall n,n1.
+\forall p1,p2:nat \to bool.
+(\forall i. i < n \to p1 i = true \to p2 (h i) = true) \to
+(\forall i. i < n \to p1 i = true \to h1 (h i) = i) \to 
+(\forall i. i < n \to p1 i = true \to h i < n1) \to 
+(\forall j. j < n1 \to p2 j = true \to p1 (h1 j) = true) \to
+(\forall j. j < n1 \to p2 j = true \to h (h1 j) = j) \to 
+(\forall j. j < n1 \to p2 j = true \to h1 j < n) \to 
+pi_p n p1 (\lambda x.g(h x)) = pi_p n1 p2 g.
+intros.
+unfold pi_p.
+apply (eq_iter_p_gen_gh nat (S O) times ? ? ? g h h1 n n1 p1 p2)
+[ apply sym_times
+| apply associative_times
+| intros.
+  apply sym_eq.
+  apply times_n_SO
+| assumption
+| assumption
+| assumption
+| assumption
+| assumption
+| assumption
+]
+qed.
+
+(* monotonicity *)
+theorem le_pi_p: 
+\forall n:nat. \forall p:nat \to bool. \forall g1,g2:nat \to nat.
+(\forall i. i < n \to p i = true \to g1 i \le g2 i ) \to 
+pi_p n p g1 \le pi_p n p g2.
+intros.
+generalize in match H.
+elim n
+  [apply le_n.
+  |apply (bool_elim ? (p n1));intros
+    [rewrite > true_to_pi_p_Sn
+      [rewrite > true_to_pi_p_Sn in ⊢ (? ? %)
+        [apply le_times
+          [apply H2[apply le_n|assumption]
+          |apply H1.
+           intros.
+           apply H2[apply le_S.assumption|assumption]
+          ]
+        |assumption
+        ]
+      |assumption
+      ]
+    |rewrite > false_to_pi_p_Sn
+      [rewrite > false_to_pi_p_Sn in ⊢ (? ? %)
+        [apply H1.
+         intros.
+         apply H2[apply le_S.assumption|assumption]
+        |assumption
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+     
+theorem exp_sigma_p: \forall n,a,p. 
+pi_p n p (\lambda x.a) = (exp a (sigma_p n p (\lambda x.S O))).
+intros.
+elim n
+  [reflexivity
+  |apply (bool_elim ? (p n1))
+    [intro.
+     rewrite > true_to_pi_p_Sn
+      [rewrite > true_to_sigma_p_Sn
+        [simplify.
+         rewrite > H.
+         reflexivity.
+        |assumption
+        ]
+      |assumption
+      ]
+    |intro.
+     rewrite > false_to_pi_p_Sn
+      [rewrite > false_to_sigma_p_Sn
+        [simplify.assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem times_pi_p: \forall n,p,f,g. 
+pi_p n p (\lambda x.f x*g x) = pi_p n p f * pi_p n p  g. 
+intros.
+elim n
+  [simplify.reflexivity
+  |apply (bool_elim ? (p n1))
+    [intro.
+     rewrite > true_to_pi_p_Sn
+      [rewrite > true_to_pi_p_Sn
+        [rewrite > true_to_pi_p_Sn
+          [rewrite > H.autobatch
+          |assumption
+          ]
+        |assumption
+        ]
+      |assumption
+      ]
+    |intro.
+     rewrite > false_to_pi_p_Sn
+      [rewrite > false_to_pi_p_Sn
+        [rewrite > false_to_pi_p_Sn;assumption
+        |assumption
+        ]
+      |assumption
+      ]
+    ]
+  ]
+qed.
+
+theorem pi_p_SO: \forall n,p. 
+pi_p n p (\lambda i.S O) = S O.
+intros.elim n
+  [reflexivity
+  |simplify.elim (p n1)
+    [simplify.rewrite < plus_n_O.assumption
+    |simplify.assumption
+    ]
+  ]
+qed.
+
+theorem exp_pi_p: \forall n,m,p,f. 
+pi_p n p (\lambda x.exp (f x) m) = exp (pi_p n p f) m.
+intros.
+elim m
+  [simplify.apply pi_p_SO
+  |simplify.
+   rewrite > times_pi_p.
+   rewrite < H.
+   reflexivity
+  ]
+qed.
+
+theorem exp_times_pi_p: \forall n,m,k,p,f. 
+pi_p n p (\lambda x.exp k (m*(f x))) = 
+exp (pi_p n p (\lambda x.exp k (f x))) m.
+intros.
+apply (trans_eq ? ? (pi_p n p (\lambda x.(exp (exp k (f x)) m))))
+  [apply eq_pi_p;intros
+    [reflexivity
+    |apply sym_eq.rewrite > sym_times.
+     apply exp_exp_times
+    ]
+  |apply exp_pi_p
+  ]
+qed.
+
+
+theorem pi_p_knm:
+\forall g: nat \to nat.
+\forall h2:nat \to nat \to nat.
+\forall h11,h12:nat \to nat. 
+\forall k,n,m.
+\forall p1,p21:nat \to bool.
+\forall p22:nat \to nat \to bool.
+(\forall x. x < k \to p1 x = true \to 
+p21 (h11 x) = true \land p22 (h11 x) (h12 x) = true
+\land h2 (h11 x) (h12 x) = x 
+\land (h11 x) < n \land (h12 x) < m) \to
+(\forall i,j. i < n \to j < m \to p21 i = true \to p22 i j = true \to 
+p1 (h2 i j) = true \land 
+h11 (h2 i j) = i \land h12 (h2 i j) = j
+\land h2 i j < k) \to
+pi_p k p1 g =
+pi_p n p21 (\lambda x:nat.pi_p m (p22 x) (\lambda y. g (h2 x y))).
+intros.
+unfold pi_p.unfold pi_p.
+apply (iter_p_gen_knm nat (S O) times sym_times assoc_times ? ? ? h11 h12)
+  [intros.apply sym_eq.apply times_n_SO.
+  |assumption
+  |assumption
+  ]
+qed.
+
+theorem pi_p_pi_p: 
+\forall g: nat \to nat \to nat.
+\forall h11,h12,h21,h22: nat \to nat \to nat. 
+\forall n1,m1,n2,m2.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall i,j. i < n2 \to j < m2 \to p21 i = true \to p22 i j = true \to 
+p11 (h11 i j) = true \land p12 (h11 i j) (h12 i j) = true
+\land h21 (h11 i j) (h12 i j) = i \land h22 (h11 i j) (h12 i j) = j
+\land h11 i j < n1 \land h12 i j < m1) \to
+(\forall i,j. i < n1 \to j < m1 \to p11 i = true \to p12 i j = true \to 
+p21 (h21 i j) = true \land p22 (h21 i j) (h22 i j) = true
+\land h11 (h21 i j) (h22 i j) = i \land h12 (h21 i j) (h22 i j) = j
+\land (h21 i j) < n2 \land (h22 i j) < m2) \to
+pi_p n1 p11 
+     (\lambda x:nat .pi_p m1 (p12 x) (\lambda y. g x y)) =
+pi_p n2 p21 
+    (\lambda x:nat .pi_p m2 (p22 x)  (\lambda y. g (h11 x y) (h12 x y))).
+intros.
+unfold pi_p.unfold pi_p.
+apply (iter_p_gen_2_eq ? ? ? sym_times assoc_times ? ? ? ? h21 h22)
+  [intros.apply sym_eq.apply times_n_SO.
+  |assumption
+  |assumption
+  ]
+qed.
+
+theorem pi_p_pi_p1: 
+\forall g: nat \to nat \to nat.
+\forall n,m.
+\forall p11,p21:nat \to bool.
+\forall p12,p22:nat \to nat \to bool.
+(\forall x,y. x < n \to y < m \to 
+ (p11 x \land p12 x y) = (p21 y \land p22 y x)) \to
+pi_p n p11 (\lambda x:nat.pi_p m (p12 x) (\lambda y. g x y)) =
+pi_p m p21 (\lambda y:nat.pi_p n (p22 y) (\lambda x. g x y)).
+intros.
+unfold pi_p.unfold pi_p.
+apply (iter_p_gen_iter_p_gen ? ? ? sym_times assoc_times)
+  [intros.apply sym_eq.apply times_n_SO.
+  |assumption
+  ]
+qed.
\ No newline at end of file
index 6885a98474089bee8c3c83336afcde7fd3228356..ec7118980e1a82a53609a14bd76c0371e6a83585 100644 (file)
@@ -190,8 +190,33 @@ rewrite > H2.rewrite < H3.
 simplify.exact (not_le_Sn_n O).
 qed.
 
-
-(*divides and div*)
+(*a variant of or_div_mod *)
+theorem or_div_mod1: \forall n,q. O < q \to
+(divides q (S n)) \land S n = (S (div n q)) * q \lor
+(\lnot (divides q (S n)) \land S n= (div n q) * q + S (n\mod q)).
+intros.elim (or_div_mod n q H);elim H1
+  [left.split
+    [apply (witness ? ? (S (n/q))).
+     rewrite > sym_times.assumption
+    |assumption
+    ]
+  |right.split
+    [intro.
+     apply (not_eq_O_S (n \mod q)).
+     (* come faccio a fare unfold nelleipotesi ? *)
+     cut ((S n) \mod q = O)
+      [rewrite < Hcut.
+       apply (div_mod_spec_to_eq2 (S n) q (div (S n) q) (mod (S n) q) (div n q) (S (mod n q)))
+        [apply div_mod_spec_div_mod.
+         assumption
+        |apply div_mod_spec_intro;assumption
+        ]
+      |apply divides_to_mod_O;assumption
+      ]
+    |assumption
+    ]
+  ]
+qed.
 
 theorem divides_to_div: \forall n,m.divides n m \to m/n*n = m.
 intro.
@@ -490,6 +515,11 @@ theorem prime_to_lt_O: \forall p. prime p \to O < p.
 intros.elim H.apply lt_to_le.assumption.
 qed.
 
+theorem prime_to_lt_SO: \forall p. prime p \to S O < p.
+intros.elim H.
+assumption.
+qed.
+
 (* smallest factor *)
 definition smallest_factor : nat \to nat \def
 \lambda n:nat.