helm/software/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 include "nat/chinese_reminder.ma".
  16 include "nat/iteration2.ma".
  17
  18 (*a new definition of totient, which uses sigma_p instead of sigma *)
  19 (*there's a little difference between this definition and the classic one:
  20   the classic definition of totient is:
  21
  22     phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1.
  23    (so this definition considers the values i=1,2,...,n)
  24
  25   sigma_p doesn't work on the value n (but the first value it works on is (pred n))
  26   but works also on 0. That's not a problem, in fact
  27    - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1.
  28    - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1.
  29
  30  *)
  31 definition totient : nat \to nat \def
  32 \lambda n.sigma_p n (\lambda m. eqb (gcd m n) (S O)) (\lambda m.S O).
  33
  34 lemma totient1: totient (S(S(S(S(S(S O)))))) = ?.
  35 [|simplify.
  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 transitive_le;
  67             [2: apply le_min_aux_r | skip | apply le_n]
  68           |unfold lt.
  69            apply (nat_case ((S m2)*(S m1)))
  70             [apply le_n|intro.apply le_n]
  71           ]
  72        |intros.
  73         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  74         intro.elim H5.
  75         apply H6
  76        |intros.
  77         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  78         intro.elim H5.
  79         apply H7
  80        |intros.
  81         generalize in match (mod_cr_pair (S m2) (S m1) a b H3 H4 H).
  82         intro.elim H5.
  83         apply eqb_elim
  84           [intro.
  85            rewrite > eq_to_eqb_true
  86              [rewrite > eq_to_eqb_true
  87                [reflexivity
  88                |rewrite < H6.
  89                 rewrite > sym_gcd.
  90                 rewrite > gcd_mod
  91                   [apply (gcd_times_SO_to_gcd_SO ? ? (S m1))
  92                     [unfold lt.apply le_S_S.apply le_O_n
  93                     |unfold lt.apply le_S_S.apply le_O_n
  94                     |assumption
  95                     ]
  96                   |unfold lt.apply le_S_S.apply le_O_n
  97                   ]
  98                ]
  99             |rewrite < H7.
 100              rewrite > sym_gcd.
 101              rewrite > gcd_mod
 102                [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
 103                   [unfold lt.apply le_S_S.apply le_O_n
 104                   |unfold lt.apply le_S_S.apply le_O_n
 105                   |rewrite > sym_times.assumption
 106                   ]
 107                |unfold lt.apply le_S_S.apply le_O_n
 108                ]
 109             ]
 110           |intro.
 111            apply eqb_elim
 112            [intro.apply eqb_elim
 113               [intro.apply False_ind.
 114                apply H8.
 115                apply eq_gcd_times_SO
 116                  [unfold lt.apply le_S_S.apply le_O_n.
 117                  |unfold lt.apply le_S_S.apply le_O_n.
 118                  |rewrite < gcd_mod
 119                     [rewrite > H6.
 120                      rewrite > sym_gcd.assumption
 121                     |unfold lt.apply le_S_S.apply le_O_n
 122                     ]
 123                  |rewrite < gcd_mod
 124                     [rewrite > H7.
 125                      rewrite > sym_gcd.assumption
 126                     |unfold lt.apply le_S_S.apply le_O_n
 127                     ]
 128                  ]
 129               |intro.reflexivity
 130               ]
 131            |intro.reflexivity
 132            ]
 133          ]
 134        ]
 135      ]
 136    ]
 137 qed.