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
  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 on 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 lemma totient1: totient (S(S(S(S(S(S O)))))) = ?.
  37 [|simplify.
  38
  39 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
  40 totient (n*m) = (totient n)*(totient m).
  41 intros.
  42 unfold totient.
  43 apply (nat_case1 n)
  44 [ apply (nat_case1 m)
  45   [ intros.
  46     simplify.
  47     reflexivity
  48   | intros.
  49     simplify.
  50     reflexivity
  51   ]
  52 | apply (nat_case1 m)
  53   [ intros.
  54     change in \vdash (? ? ? (? ? %)) with (O).
  55     rewrite > (sym_times (S m1) O).
  56     rewrite > sym_times in \vdash (? ? ? %).
  57     simplify.
  58     reflexivity
  59   | intros.
  60     rewrite > H2 in H.
  61     rewrite > H1 in H.
  62     apply (sigma_p_times m2 m1 ? ? ?
  63             (\lambda b,a. cr_pair (S m2) (S m1) a b)
  64             (\lambda x. x \mod (S m2)) (\lambda x. x \mod (S m1)))
  65    [intros.unfold cr_pair.
  66         apply (le_to_lt_to_lt ? (pred ((S m2)*(S m1))))
  67           [unfold min.
  68            apply transitive_le;
  69             [2: apply le_min_aux_r | skip | apply le_n]
  70           |unfold lt.
  71            apply (nat_case ((S m2)*(S m1)))
  72             [apply le_n|intro.apply le_n]
  73           ]
  74        |intros.
  75         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  76         intro.elim H5.
  77         apply H6
  78        |intros.
  79         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  80         intro.elim H5.
  81         apply H7
  82        |intros.
  83         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  84         intro.elim H5.
  85         apply eqb_elim
  86           [intro.
  87            rewrite > eq_to_eqb_true
  88              [rewrite > eq_to_eqb_true
  89                [reflexivity
  90                |rewrite < H6.
  91                 rewrite > sym_gcd.
  92                 rewrite > gcd_mod
  93                   [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
  94                     [unfold lt.apply le_S_S.apply le_O_n
  95                     |unfold lt.apply le_S_S.apply le_O_n
  96                     |assumption
  97                     ]
  98                   |unfold lt.apply le_S_S.apply le_O_n
  99                   ]
 100                ]
 101             |rewrite < H7.
 102              rewrite > sym_gcd.
 103              rewrite > gcd_mod
 104                [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
 105                   [unfold lt.apply le_S_S.apply le_O_n
 106                   |unfold lt.apply le_S_S.apply le_O_n
 107                   |rewrite > sym_times.assumption
 108                   ]
 109                |unfold lt.apply le_S_S.apply le_O_n
 110                ]
 111             ]
 112           |intro.
 113            apply eqb_elim
 114            [intro.apply eqb_elim
 115               [intro.apply False_ind.
 116                apply H8.
 117                apply eq_gcd_times_SO
 118                  [unfold lt.apply le_S_S.apply le_O_n.
 119                  |unfold lt.apply le_S_S.apply le_O_n.
 120                  |rewrite < gcd_mod
 121                     [rewrite > H6.
 122                      rewrite > sym_gcd.assumption
 123                     |unfold lt.apply le_S_S.apply le_O_n
 124                     ]
 125                  |rewrite < gcd_mod
 126                     [rewrite > H7.
 127                      rewrite > sym_gcd.assumption
 128                     |unfold lt.apply le_S_S.apply le_O_n
 129                     ]
 130                  ]
 131               |intro.reflexivity
 132               ]
 133            |intro.reflexivity
 134            ]
 135          ]
 136        ]
 137      ]
 138    ]
 139 qed.