renamed generic_sigma_p.ma to generic_iter_p.ma

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

diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma
index b4f575a404c15982b04cac19db20c7f3428d6fc5..a86986a81f743efd78b0dd004e38653c0788d601 100644 (file)
--- a/helm/software/matita/library/nat/totient.ma
+++ b/helm/software/matita/library/nat/totient.ma
@@ -14,62 +14,81 @@
 
 set "baseuri" "cic:/matita/nat/totient".
 
-include "nat/count.ma".
 include "nat/chinese_reminder.ma".
+include "nat/iteration2.ma".
 
+(*a new definition of totient, which uses sigma_p instead of sigma *)
+(*there's a little difference between this definition and the classic one:
+  the classic definition of totient is:
+   
+    phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
+   (so this definition considers the values i=1,2,...,n)
+  
+  sigma_p doesn't work on the value n (but the first value it works on is (pred n))
+  but works also on 0. That's not a problem, in fact
+   - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. 
+   - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. 
+   
+ *)
 definition totient : nat \to nat \def
-\lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
-
-theorem totient3: totient (S(S(S O))) = (S(S O)).
-reflexivity.
-qed.
-
-theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
-reflexivity.
-qed.
+\lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
 
+                                        
 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
 totient (n*m) = (totient n)*(totient m).
-intro.
-apply (nat_case n)
-  [intros.simplify.reflexivity
-  |intros 2.apply (nat_case m1)
-    [rewrite < sym_times.
-     rewrite < (sym_times (totient O)).
-     simplify.intro.reflexivity.
-     |intros.
-      unfold totient.
-      apply (count_times m m2 ? ? ? 
-             (\lambda b,a. cr_pair (S m) (S m2) a b) 
-             (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)))
-       [intros.unfold cr_pair.
-        apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
+intros.
+unfold totient.
+apply (nat_case1 n)
+[ apply (nat_case1 m)
+  [ intros.
+    simplify.
+    reflexivity
+  | intros.
+    simplify.
+    reflexivity
+  ]
+| apply (nat_case1 m)
+  [ intros.
+    change in \vdash (? ? ? (? ? %)) with (O).
+    rewrite > (sym_times (S m1) O).
+    rewrite > sym_times in \vdash (? ? ? %).
+    simplify.
+    reflexivity  
+  | intros.
+    rewrite > H2 in H.
+    rewrite > H1 in H.    
+    apply (sigma_p_times m2 m1 ? ? ? 
+            (\lambda b,a. cr_pair (S m2) (S m1) a b) 
+            (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
+   [intros.unfold cr_pair.
+        apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
           [unfold min.
-           apply le_min_aux_r
+           apply transitive_le;
+            [2: apply le_min_aux_r | skip | apply le_n]
           |unfold lt.
-           apply (nat_case ((S m)*(S m2)))
+           apply (nat_case ((S m2)*(S m1)))
             [apply le_n|intro.apply le_n]
           ]
        |intros.
-        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-        intro.elim H3.
-        apply H4
+        generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+        intro.elim H5.
+        apply H6
        |intros.
-        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-        intro.elim H3.
-        apply H5
+        generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+        intro.elim H5.
+        apply H7
        |intros.
-        generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
-        intro.elim H3.
+        generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
+        intro.elim H5.
         apply eqb_elim
           [intro.
            rewrite > eq_to_eqb_true
              [rewrite > eq_to_eqb_true
                [reflexivity
-               |rewrite < H4.
+               |rewrite < H6.
                 rewrite > sym_gcd.
                 rewrite > gcd_mod
-                  [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
+                  [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
                     [unfold lt.apply le_S_S.apply le_O_n
                     |unfold lt.apply le_S_S.apply le_O_n
                     |assumption
@@ -77,10 +96,10 @@ apply (nat_case n)
                   |unfold lt.apply le_S_S.apply le_O_n
                   ]
                ]           
-            |rewrite < H5.
+            |rewrite < H7.
              rewrite > sym_gcd.
              rewrite > gcd_mod
-               [apply (gcd_times_SO_to_gcd_SO ? ? (S m))
+               [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
                   [unfold lt.apply le_S_S.apply le_O_n
                   |unfold lt.apply le_S_S.apply le_O_n
                   |rewrite > sym_times.assumption
@@ -92,17 +111,17 @@ apply (nat_case n)
            apply eqb_elim
            [intro.apply eqb_elim
               [intro.apply False_ind.
-               apply H6.
+               apply H8.
                apply eq_gcd_times_SO
                  [unfold lt.apply le_S_S.apply le_O_n.
                  |unfold lt.apply le_S_S.apply le_O_n.
                  |rewrite < gcd_mod
-                    [rewrite > H4.
+                    [rewrite > H6.
                      rewrite > sym_gcd.assumption
                     |unfold lt.apply le_S_S.apply le_O_n
                     ]
                  |rewrite < gcd_mod
-                    [rewrite > H5.
+                    [rewrite > H7.
                      rewrite > sym_gcd.assumption
                     |unfold lt.apply le_S_S.apply le_O_n
                     ]
@@ -115,4 +134,4 @@ apply (nat_case n)
        ]
      ]
    ]
-qed.
\ No newline at end of file
+qed.