matita/library/nat/totient.ma

   1 (**************************************************************************)
   2 (*       __                                                               *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/totient".
  16
  17 include "nat/chinese_reminder.ma".
  18 include "nat/iteration2.ma".
  19
  20 (*a new definition of totient, which uses sigma_p instead of sigma *)
  21 (*there's a little difference between this definition and the classic one:
  22   the classic definition of totient is:
  23
  24     phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
  25    (so this definition considers the values i=1,2,...,n)
  26
  27   sigma_p doesn't work ok the value n (but the first value it works on is (pred n))
  28   but works also on 0. That's not a problem, in fact
  29    - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1.
  30    - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1.
  31
  32  *)
  33 definition totient : nat \to nat \def
  34 \lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
  35
  36
  37 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
  38 totient (n*m) = (totient n)*(totient m).
  39 intros.
  40 unfold totient.
  41 apply (nat_case1 n)
  42 [ apply (nat_case1 m)
  43   [ intros.
  44     simplify.
  45     reflexivity
  46   | intros.
  47     simplify.
  48     reflexivity
  49   ]
  50 | apply (nat_case1 m)
  51   [ intros.
  52     change in \vdash (? ? ? (? ? %)) with (O).
  53     rewrite > (sym_times (S m1) O).
  54     rewrite > sym_times in \vdash (? ? ? %).
  55     simplify.
  56     reflexivity
  57   | intros.
  58     rewrite > H2 in H.
  59     rewrite > H1 in H.
  60     apply (sigma_p_times m2 m1 ? ? ?
  61             (\lambda b,a. cr_pair (S m2) (S m1) a b)
  62             (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
  63    [intros.unfold cr_pair.
  64         apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
  65           [unfold min.
  66            apply le_min_aux_r
  67           |unfold lt.
  68            apply (nat_case ((S m2)*(S m1)))
  69             [apply le_n|intro.apply le_n]
  70           ]
  71        |intros.
  72         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  73         intro.elim H5.
  74         apply H6
  75        |intros.
  76         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  77         intro.elim H5.
  78         apply H7
  79        |intros.
  80         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  81         intro.elim H5.
  82         apply eqb_elim
  83           [intro.
  84            rewrite > eq_to_eqb_true
  85              [rewrite > eq_to_eqb_true
  86                [reflexivity
  87                |rewrite < H6.
  88                 rewrite > sym_gcd.
  89                 rewrite > gcd_mod
  90                   [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
  91                     [unfold lt.apply le_S_S.apply le_O_n
  92                     |unfold lt.apply le_S_S.apply le_O_n
  93                     |assumption
  94                     ]
  95                   |unfold lt.apply le_S_S.apply le_O_n
  96                   ]
  97                ]
  98             |rewrite < H7.
  99              rewrite > sym_gcd.
 100              rewrite > gcd_mod
 101                [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
 102                   [unfold lt.apply le_S_S.apply le_O_n
 103                   |unfold lt.apply le_S_S.apply le_O_n
 104                   |rewrite > sym_times.assumption
 105                   ]
 106                |unfold lt.apply le_S_S.apply le_O_n
 107                ]
 108             ]
 109           |intro.
 110            apply eqb_elim
 111            [intro.apply eqb_elim
 112               [intro.apply False_ind.
 113                apply H8.
 114                apply eq_gcd_times_SO
 115                  [unfold lt.apply le_S_S.apply le_O_n.
 116                  |unfold lt.apply le_S_S.apply le_O_n.
 117                  |rewrite < gcd_mod
 118                     [rewrite > H6.
 119                      rewrite > sym_gcd.assumption
 120                     |unfold lt.apply le_S_S.apply le_O_n
 121                     ]
 122                  |rewrite < gcd_mod
 123                     [rewrite > H7.
 124                      rewrite > sym_gcd.assumption
 125                     |unfold lt.apply le_S_S.apply le_O_n
 126                     ]
 127                  ]
 128               |intro.reflexivity
 129               ]
 130            |intro.reflexivity
 131            ]
 132          ]
 133        ]
 134      ]
 135    ]
 136 qed.