More restructuring in moebius.ma

[helm.git] / matita / library / nat / factorization.ma

diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma
index 85351c06d47ac9b63e5d4a94964d7d6e56f97a9c..14696ca2891d7322622f2b7aabd2a1031fc36572 100644 (file)
--- a/matita/library/nat/factorization.ma
+++ b/matita/library/nat/factorization.ma
@@ -27,10 +27,10 @@ definition max_prime_factor \def \lambda n:nat.
 theorem divides_max_prime_factor_n:
   \forall n:nat. (S O) < n
   \to nth_prime (max_prime_factor n) \divides n.
-intros; apply divides_b_true_to_divides;
-[ apply lt_O_nth_prime_n;
-| apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
-  cut (\exists i. nth_prime i = smallest_factor n);
+intros.
+apply divides_b_true_to_divides.
+apply (f_max_true  (\lambda p:nat.eqb (n \mod (nth_prime p)) O) n);
+cut (\exists i. nth_prime i = smallest_factor n);
   [ elim Hcut.
     apply (ex_intro nat ? a);
     split;
@@ -46,17 +46,17 @@ intros; apply divides_b_true_to_divides;
       [ apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | apply lt_SO_smallest_factor; assumption; ]
-      | letin x \def le.auto new.
+      | letin x \def le.autobatch new.
          (*       
        apply divides_smallest_factor_n;
         apply (trans_lt ? (S O));
         [ unfold lt; apply le_n;
         | assumption; ] *) ] ]
-  | auto. 
+  | autobatch. 
     (* 
     apply prime_to_nth_prime;
     apply prime_smallest_factor_n;
-    assumption; *) ] ]
+    assumption; *) ] 
 qed.
 
 theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to 
@@ -70,8 +70,8 @@ apply divides_to_divides_b_true.
 cut (prime (nth_prime (max_prime_factor n))).
 apply lt_O_nth_prime_n.apply prime_nth_prime.
 cut (nth_prime (max_prime_factor n) \divides n).
-auto.
-auto.
+autobatch.
+autobatch.
 (*
   [ apply (transitive_divides ? n);
     [ apply divides_max_prime_factor_n.
@@ -90,6 +90,30 @@ auto.
 *)  
 qed.
 
+theorem divides_to_max_prime_factor1 : \forall n,m. O < n \to O < m \to n \divides m \to 
+max_prime_factor n \le max_prime_factor m.
+intros 3.
+elim (le_to_or_lt_eq ? ? H)
+  [apply divides_to_max_prime_factor
+    [assumption|assumption|assumption]
+  |rewrite < H1.
+   simplify.apply le_O_n.
+  ]
+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
@@ -105,7 +129,7 @@ apply divides_max_prime_factor_n.
 assumption.unfold Not.
 intro.
 cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
-  [unfold Not in Hcut1.auto new.
+  [unfold Not in Hcut1.autobatch new.
     (*
     apply Hcut1.apply divides_to_mod_O;
     [ apply lt_O_nth_prime_n.
@@ -114,7 +138,7 @@ cut (r \mod (nth_prime (max_prime_factor n)) \neq O);
     *)
   |letin z \def le.
    cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n)));
-   [2: rewrite < H1.assumption.|letin x \def le.auto width = 4 new]
+   [2: rewrite < H1.assumption.|letin x \def le.autobatch width = 4 depth = 2]
    (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *)
   ].
 (*
@@ -153,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
@@ -388,7 +439,6 @@ apply (not_eq_O_S (S m1)).
 rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity.
 apply le_to_or_lt_eq.apply le_O_n.
 (* prova del cut *)
-goal 20.
 apply (p_ord_aux_to_exp (S(S m1))).
 apply lt_O_nth_prime_n.
 assumption.
@@ -446,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.