renamed generic_sigma_p.ma to generic_iter_p.ma

[helm.git] / helm / software / matita / library / nat / primes.ma

diff --git a/helm/software/matita/library/nat/primes.ma b/helm/software/matita/library/nat/primes.ma
index c5fe7bd298990a596e523bbc8282cd85f8e244ef..a95b2e88fddda2344f0fafc448593de57404d470 100644 (file)
--- a/helm/software/matita/library/nat/primes.ma
+++ b/helm/software/matita/library/nat/primes.ma
@@ -193,7 +193,7 @@ qed.
 (* boolean divides *)
 definition divides_b : nat \to nat \to bool \def
 \lambda n,m :nat. (eqb (m \mod n) O).
-  
+
 theorem divides_b_to_Prop :
 \forall n,m:nat. O < n \to
 match divides_b n m with
@@ -205,7 +205,7 @@ intro.simplify.apply mod_O_to_divides.assumption.assumption.
 intro.simplify.unfold Not.intro.apply H1.apply divides_to_mod_O.assumption.assumption.
 qed.
 
-theorem divides_b_true_to_divides :
+theorem divides_b_true_to_divides1:
 \forall n,m:nat. O < n \to
 (divides_b n m = true ) \to n \divides m.
 intros.
@@ -217,7 +217,21 @@ rewrite < H1.apply divides_b_to_Prop.
 assumption.
 qed.
 
-theorem divides_b_false_to_not_divides :
+theorem divides_b_true_to_divides:
+\forall n,m:nat. divides_b n m = true \to n \divides m.
+intros 2.apply (nat_case n)
+  [apply (nat_case m)
+    [intro.apply divides_n_n
+    |simplify.intros.apply False_ind.
+     apply not_eq_true_false.apply sym_eq.assumption
+    ]
+  |intros.
+   apply divides_b_true_to_divides1
+    [apply lt_O_S|assumption]
+  ]
+qed.
+
+theorem divides_b_false_to_not_divides1:
 \forall n,m:nat. O < n \to
 (divides_b n m = false ) \to n \ndivides m.
 intros.
@@ -229,6 +243,22 @@ rewrite < H1.apply divides_b_to_Prop.
 assumption.
 qed.
 
+theorem divides_b_false_to_not_divides:
+\forall n,m:nat. divides_b n m = false \to n \ndivides m.
+intros 2.apply (nat_case n)
+  [apply (nat_case m)
+    [simplify.unfold Not.intros.
+     apply not_eq_true_false.assumption
+    |unfold Not.intros.elim H1.
+     apply (not_eq_O_S m1).apply sym_eq.
+     assumption
+    ]
+  |intros.
+   apply divides_b_false_to_not_divides1
+    [apply lt_O_S|assumption]
+  ]
+qed.
+
 theorem decidable_divides: \forall n,m:nat.O < n \to
 decidable (n \divides m).
 intros.unfold decidable.
@@ -263,6 +293,21 @@ absurd (n \divides m).assumption.assumption.
 reflexivity.
 qed.
 
+theorem divides_b_true_to_lt_O: \forall n,m. O < n \to divides_b m n = true \to O < m.
+intros.
+elim (le_to_or_lt_eq ? ? (le_O_n m))
+  [assumption
+  |apply False_ind.
+   elim H1.
+   rewrite < H2 in H1.
+   simplify in H1.
+   apply (lt_to_not_eq O n H).
+   apply sym_eq.
+   apply eqb_true_to_eq.
+   assumption
+  ]
+qed.
+
 (* divides and pi *)
 theorem divides_f_pi_f : \forall f:nat \to nat.\forall n,m,i:nat. 
 m \le i \to i \le n+m \to f i \divides pi n f m.
@@ -323,10 +368,8 @@ theorem not_divides_S_fact: \forall n,i:nat.
 (S O) < i \to i \le n \to i \ndivides S n!.
 intros.
 apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.
 unfold divides_b.
-rewrite > mod_S_fact.simplify.reflexivity.
-assumption.assumption.
+rewrite > mod_S_fact[simplify.reflexivity|assumption|assumption].
 qed.
 
 (* prime *)
@@ -342,6 +385,10 @@ theorem not_prime_SO: \lnot (prime (S O)).
 unfold Not.unfold prime.intro.elim H.apply (not_le_Sn_n (S O) H1).
 qed.
 
+theorem prime_to_lt_O: \forall p. prime p \to O < p.
+intros.elim H.apply lt_to_le.assumption.
+qed.
+
 (* smallest factor *)
 definition smallest_factor : nat \to nat \def
 \lambda n:nat. 
@@ -350,18 +397,18 @@ match n with
 | (S p) \Rightarrow 
   match p with
   [ O \Rightarrow (S O)
-  | (S q) \Rightarrow min_aux q (S(S q)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
+  | (S q) \Rightarrow min_aux q (S (S O)) (\lambda m.(eqb ((S(S q)) \mod m) O))]].
 
-(* it works ! 
-theorem example1 : smallest_prime_factor (S(S(S O))) = (S(S(S O))).
+(* it works !
+theorem example1 : smallest_factor (S(S(S O))) = (S(S(S O))).
 normalize.reflexivity.
 qed.
 
-theorem example2: smallest_prime_factor (S(S(S(S O)))) = (S(S O)).
+theorem example2: smallest_factor (S(S(S(S O)))) = (S(S O)).
 normalize.reflexivity.
 qed.
 
-theorem example3 : smallest_prime_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
+theorem example3 : smallest_factor (S(S(S(S(S(S(S O))))))) = (S(S(S(S(S(S(S O))))))).
 simplify.reflexivity.
 qed. *)
 
@@ -372,7 +419,7 @@ apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
 intros.
 change with 
-(S O < min_aux m1 (S(S m1)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
+(S O < min_aux m1 (S (S O)) (\lambda m.(eqb ((S(S m1)) \mod m) O))).
 apply (lt_to_le_to_lt ? (S (S O))).
 apply (le_n (S(S O))).
 cut ((S(S O)) = (S(S m1)) - m1).
@@ -401,17 +448,19 @@ intro.apply (nat_case m).intro. simplify.
 apply (witness ? ? (S O)). simplify.reflexivity.
 intros.
 apply divides_b_true_to_divides.
-apply (lt_O_smallest_factor ? H).
 change with 
-(eqb ((S(S m1)) \mod (min_aux m1 (S(S m1)) 
+(eqb ((S(S m1)) \mod (min_aux m1 (S (S O)) 
   (\lambda m.(eqb ((S(S m1)) \mod m) O)))) O = true).
 apply f_min_aux_true.
 apply (ex_intro nat ? (S(S m1))).
 split.split.
-apply le_minus_m.apply le_n.
-rewrite > mod_n_n.reflexivity.
-apply (trans_lt ? (S O)).apply (le_n (S O)).unfold lt.
-apply le_S_S.apply le_S_S.apply le_O_n.
+apply (le_S_S_to_le (S (S O)) (S (S m1)) ?).
+apply (minus_le_O_to_le (S (S (S O))) (S (S (S m1))) ?).
+apply (le_n O).
+rewrite < sym_plus. simplify. apply le_n.
+apply (eq_to_eqb_true (mod (S (S m1)) (S (S m1))) O ?).
+apply (mod_n_n (S (S m1)) ?).
+apply (H).
 qed.
   
 theorem le_smallest_factor_n : 
@@ -431,14 +480,10 @@ apply (nat_case n).intro.apply False_ind.apply (not_le_Sn_O (S O) H).
 intro.apply (nat_case m).intro. apply False_ind.apply (not_le_Sn_n (S O) H).
 intros.
 apply divides_b_false_to_not_divides.
-apply (trans_lt O (S O)).apply (le_n (S O)).assumption.unfold divides_b.
 apply (lt_min_aux_to_false 
-(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S(S m1)) m1 i).
-cut ((S(S O)) = (S(S m1)-m1)).
-rewrite < Hcut.exact H1.
-apply sym_eq. apply plus_to_minus.
-rewrite < sym_plus.simplify.reflexivity.
-exact H2.
+(\lambda i:nat.eqb ((S(S m1)) \mod i) O) (S (S O)) m1 i).
+assumption.
+assumption.
 qed.
 
 theorem prime_smallest_factor_n :