More restructuring in moebius.ma

diff --git a/matita/library/Z/moebius.ma b/matita/library/Z/moebius.ma
index d2c3765c3880b473f3217de64481187fc6a2efb8..1eb35852155109194babd46f20c0992e24516182 100644 (file)
--- a/matita/library/Z/moebius.ma
+++ b/matita/library/Z/moebius.ma
@@ -62,33 +62,6 @@ simplify.reflexivity.
 qed.
 *)
 
-theorem not_divides_to_p_ord_O: \forall n,i.
-Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = 
-pair nat nat O n.
-intros.
-apply p_ord_exp1
-  [apply lt_O_nth_prime_n
-  |assumption
-  |autobatch
-  ]
-qed.
-
-theorem p_ord_O_to_not_divides: \forall n,i,r.
-O < n \to
-p_ord n (nth_prime i) = pair nat nat O r 
-\to Not (divides (nth_prime i) n).
-intros.
-lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
-  [apply lt_SO_nth_prime_n
-  |assumption
-  |elim Hletin.
-   simplify in H3.
-   rewrite > H3.
-   rewrite < plus_n_O.
-   assumption
-  ]
-qed.
-
 theorem not_divides_to_eq_moebius_aux: \forall n,p,p1.p \le p1 \to
 (\forall i. p \le i \to i \le p1 \to Not (divides (nth_prime i) n))
 \to moebius_aux p n = moebius_aux p1 n.
@@ -143,39 +116,6 @@ elim p
   ]
 qed.
 
-theorem p_ord_to_not_eq_O : \forall n,p,q,r.
-  (S O) < n \to
-  p_ord n (nth_prime p) = pair nat nat q r \to
-  Not (r=O).
-intros.
-unfold.intro.
-cut (O < n)
-  [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
-    [apply lt_SO_nth_prime_n.
-    |assumption
-    |elim Hletin.
-     apply (lt_to_not_eq ? ? Hcut).
-     rewrite > H4.
-     rewrite > H2.
-     apply times_n_O
-    ]
-  |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
-  ]
-qed.
-
-theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
-  (S O) < n \to
-  p = max_prime_factor n \to
-  p_ord n (nth_prime p) \neq pair nat nat O r.
-intros.unfold Not.intro.
-apply (p_ord_O_to_not_divides ? ? ? ? H2)
-  [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
-  |rewrite > H1.
-   apply divides_max_prime_factor_n.
-   assumption
-  ]
-qed.
-
 theorem p_ord_SO_SO_to_moebius : \forall n,p.
   (S O) < n \to
   p = max_prime_factor n \to
@@ -260,115 +200,6 @@ rewrite > H2.simplify.
 reflexivity.
 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
-p = max_prime_factor (r*(nth_prime p)\sup n).
-intros.
-apply sym_eq.
-unfold max_prime_factor.
-apply max_spec_to_max.
-split
-  [split
-    [rewrite > times_n_SO in \vdash (? % ?).
-     rewrite > sym_times.
-     apply le_times
-      [assumption
-      |apply lt_to_le.
-       apply (lt_to_le_to_lt ? (nth_prime p))
-        [apply lt_n_nth_prime_n
-        |rewrite > exp_n_SO in \vdash (? % ?).
-         apply le_exp
-          [apply lt_O_nth_prime_n
-          |assumption
-          ]
-        ]
-      ]
-    |apply eq_to_eqb_true.
-     apply divides_to_mod_O
-      [apply lt_O_nth_prime_n
-      |apply (lt_O_n_elim ? H).
-       intro.
-       apply (witness ? ? (r*(nth_prime p \sup m))).
-       rewrite < assoc_times.
-       rewrite < sym_times in \vdash (? ? ? (? % ?)).
-       rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
-       rewrite > assoc_times.
-       rewrite < exp_plus_times.
-       reflexivity
-      ]
-    ]
-  |intros.  
-   apply not_eq_to_eqb_false.
-   unfold Not.intro.
-   lapply (mod_O_to_divides ? ? ? H5)
-    [apply lt_O_nth_prime_n
-    |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
-      [elim H2
-        [rewrite > H6 in Hletin.
-         simplify in Hletin.
-         rewrite < plus_n_O in Hletin.
-         apply Hcut.assumption
-        |elim (divides_times_to_divides ? ? ? ? Hletin)
-          [apply (lt_to_not_le ? ? H3).
-           apply lt_to_le. 
-           apply (le_to_lt_to_lt ? ? ? ? H6).
-           apply f_m_to_le_max
-            [apply (trans_le ? (nth_prime i))
-              [apply lt_to_le.
-               apply lt_n_nth_prime_n
-              |apply divides_to_le[assumption|assumption]
-              ]
-            |apply eq_to_eqb_true.
-             apply divides_to_mod_O
-              [apply lt_O_nth_prime_n|assumption]
-            ]
-          |apply prime_nth_prime
-          |apply Hcut.assumption
-          ]
-        ]
-      |unfold Not.intro.
-       apply (lt_to_not_eq ? ? H3).
-       apply sym_eq.
-       elim (prime_nth_prime p).
-       apply injective_nth_prime.
-       apply H8
-        [apply (divides_exp_to_divides ? ? ? ? H6).
-         apply prime_nth_prime.
-        |apply lt_SO_nth_prime_n
-        ]
-      ]
-    ]
-  ]
-qed.
-
-lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
-O < n \to n=S O \lor max_prime_factor n < p \to 
-(nth_prime p \ndivides n).
-intros.unfold Not.intro.
-elim H1
-  [rewrite > H3 in H2.
-   apply (le_to_not_lt (nth_prime p) (S O))
-    [apply divides_to_le[apply le_n|assumption]
-    |apply lt_SO_nth_prime_n
-    ]
-  |apply (not_le_Sn_n p).
-   change with (p < p).
-   apply (le_to_lt_to_lt ? ? ? ? H3).
-   unfold max_prime_factor.
-   apply  f_m_to_le_max
-    [apply (trans_le ? (nth_prime p))
-      [apply lt_to_le.
-       apply lt_n_nth_prime_n
-      |apply divides_to_le;assumption
-      ]
-    |apply eq_to_eqb_true.
-     apply divides_to_mod_O
-      [apply lt_O_nth_prime_n|assumption]
-    ]
-  ]
-qed.
-
 theorem moebius_exp: \forall p,q,r:nat. O < r \to
 r = (S O) \lor (max_prime_factor r) < p \to
 (* r = (S O) \lor (max r (\lambda p:nat.eqb (r \mod (nth_prime p)) O)) < p \to *)

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 0bd8e247836bb10a679b9f648f0603a1a5a899dc..14696ca2891d7322622f2b7aabd2a1031fc36572 100644 (file)
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -101,6 +101,19 @@ elim (le_to_or_lt_eq ? ? H)
   ]
 qed.
 
+theorem max_prime_factor_to_not_p_ord_O : \forall n,p,r.
+  (S O) < n \to
+  p = max_prime_factor n \to
+  p_ord n (nth_prime p) \neq pair nat nat O r.
+intros.unfold Not.intro.
+apply (p_ord_O_to_not_divides ? ? ? ? H2)
+  [apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+  |rewrite > H1.
+   apply divides_max_prime_factor_n.
+   assumption
+  ]
+qed.
+
 theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to
 p = max_prime_factor n \to 
 (pair nat nat q r) = p_ord n (nth_prime p) \to
@@ -164,6 +177,33 @@ assumption.apply sym_eq.assumption.assumption.assumption.
 apply (le_to_or_lt_eq ? p H1).
 qed.
 
+lemma lt_max_prime_factor_to_not_divides: \forall n,p:nat.
+O < n \to n=S O \lor max_prime_factor n < p \to 
+(nth_prime p \ndivides n).
+intros.unfold Not.intro.
+elim H1
+  [rewrite > H3 in H2.
+   apply (le_to_not_lt (nth_prime p) (S O))
+    [apply divides_to_le[apply le_n|assumption]
+    |apply lt_SO_nth_prime_n
+    ]
+  |apply (not_le_Sn_n p).
+   change with (p < p).
+   apply (le_to_lt_to_lt ? ? ? ? H3).
+   unfold max_prime_factor.
+   apply  f_m_to_le_max
+    [apply (trans_le ? (nth_prime p))
+      [apply lt_to_le.
+       apply lt_n_nth_prime_n
+      |apply divides_to_le;assumption
+      ]
+    |apply eq_to_eqb_true.
+     apply divides_to_mod_O
+      [apply lt_O_nth_prime_n|assumption]
+    ]
+  ]
+qed.
+
 (* datatypes and functions *)
 
 inductive nat_fact : Set \def
@@ -456,6 +496,88 @@ 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
+p = max_prime_factor (r*(nth_prime p)\sup n).
+intros.
+apply sym_eq.
+unfold max_prime_factor.
+apply max_spec_to_max.
+split
+  [split
+    [rewrite > times_n_SO in \vdash (? % ?).
+     rewrite > sym_times.
+     apply le_times
+      [assumption
+      |apply lt_to_le.
+       apply (lt_to_le_to_lt ? (nth_prime p))
+        [apply lt_n_nth_prime_n
+        |rewrite > exp_n_SO in \vdash (? % ?).
+         apply le_exp
+          [apply lt_O_nth_prime_n
+          |assumption
+          ]
+        ]
+      ]
+    |apply eq_to_eqb_true.
+     apply divides_to_mod_O
+      [apply lt_O_nth_prime_n
+      |apply (lt_O_n_elim ? H).
+       intro.
+       apply (witness ? ? (r*(nth_prime p \sup m))).
+       rewrite < assoc_times.
+       rewrite < sym_times in \vdash (? ? ? (? % ?)).
+       rewrite > exp_n_SO in \vdash (? ? ? (? (? ? %) ?)).
+       rewrite > assoc_times.
+       rewrite < exp_plus_times.
+       reflexivity
+      ]
+    ]
+  |intros.  
+   apply not_eq_to_eqb_false.
+   unfold Not.intro.
+   lapply (mod_O_to_divides ? ? ? H5)
+    [apply lt_O_nth_prime_n
+    |cut (Not (divides (nth_prime i) ((nth_prime p)\sup n)))
+      [elim H2
+        [rewrite > H6 in Hletin.
+         simplify in Hletin.
+         rewrite < plus_n_O in Hletin.
+         apply Hcut.assumption
+        |elim (divides_times_to_divides ? ? ? ? Hletin)
+          [apply (lt_to_not_le ? ? H3).
+           apply lt_to_le. 
+           apply (le_to_lt_to_lt ? ? ? ? H6).
+           apply f_m_to_le_max
+            [apply (trans_le ? (nth_prime i))
+              [apply lt_to_le.
+               apply lt_n_nth_prime_n
+              |apply divides_to_le[assumption|assumption]
+              ]
+            |apply eq_to_eqb_true.
+             apply divides_to_mod_O
+              [apply lt_O_nth_prime_n|assumption]
+            ]
+          |apply prime_nth_prime
+          |apply Hcut.assumption
+          ]
+        ]
+      |unfold Not.intro.
+       apply (lt_to_not_eq ? ? H3).
+       apply sym_eq.
+       elim (prime_nth_prime p).
+       apply injective_nth_prime.
+       apply H8
+        [apply (divides_exp_to_divides ? ? ? ? H6).
+         apply prime_nth_prime.
+        |apply lt_SO_nth_prime_n
+        ]
+      ]
+    ]
+  ]
+qed.
+
 theorem  not_divides_defactorize_aux: \forall f:nat_fact. \forall i,j:nat.
 i < j \to nth_prime i \ndivides defactorize_aux f j.
 intro.elim f.

diff --git a/matita/library/nat/ord.ma b/matita/library/nat/ord.ma
index 4fd2fd2828bdd75616596a093d6f063339bd004c..5895b3bcddbebcf22f5388cd8b4483027d137012 100644 (file)
--- a/matita/library/nat/ord.ma
+++ b/matita/library/nat/ord.ma
@@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/nat/ord".
 
 include "datatypes/constructors.ma".
 include "nat/exp.ma".
-include "nat/gcd.ma".
+include "nat/nth_prime.ma".
 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
 
 let rec p_ord_aux p n m \def
@@ -240,6 +240,7 @@ rewrite < times_n_SO.
 apply exp_n_SO.
 qed.
 
+(* p_ord and divides *)
 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat. 
 O < n \to O < m \to prime p 
 \to divides n m \to p_ord n p = pair ? ? a b \to
@@ -313,7 +314,55 @@ cut (S O < p)
     ]
   |elim H2.assumption
   ]
-qed.     
+qed.    
+
+(* p_ord and primes *)
+theorem not_divides_to_p_ord_O: \forall n,i.
+Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) = 
+pair nat nat O n.
+intros.
+apply p_ord_exp1
+  [apply lt_O_nth_prime_n
+  |assumption
+  |autobatch
+  ]
+qed.
+
+theorem p_ord_O_to_not_divides: \forall n,i,r.
+O < n \to
+p_ord n (nth_prime i) = pair nat nat O r 
+\to Not (divides (nth_prime i) n).
+intros.
+lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+  [apply lt_SO_nth_prime_n
+  |assumption
+  |elim Hletin.
+   simplify in H3.
+   rewrite > H3.
+   rewrite < plus_n_O.
+   assumption
+  ]
+qed.
+
+theorem p_ord_to_not_eq_O : \forall n,p,q,r.
+  (S O) < n \to
+  p_ord n (nth_prime p) = pair nat nat q r \to
+  Not (r=O).
+intros.
+unfold.intro.
+cut (O < n)
+  [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
+    [apply lt_SO_nth_prime_n.
+    |assumption
+    |elim Hletin.
+     apply (lt_to_not_eq ? ? Hcut).
+     rewrite > H4.
+     rewrite > H2.
+     apply times_n_O
+    ]
+  |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
+  ]
+qed.
 
 definition ord :nat \to nat \to nat \def
 \lambda n,p. fst ? ? (p_ord n p).