matita/library_auto/auto/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/library_auto/nat/totient".
  16
  17 include "auto/nat/count.ma".
  18 include "auto/nat/chinese_reminder.ma".
  19
  20 definition totient : nat \to nat \def
  21 \lambda n. count n (\lambda m. eqb (gcd m n) (S O)).
  22
  23 theorem totient3: totient (S(S(S O))) = (S(S O)).
  24 reflexivity.
  25 qed.
  26
  27 theorem totient6: totient (S(S(S(S(S(S O)))))) = (S(S O)).
  28 reflexivity.
  29 qed.
  30
  31 theorem totient_times: \forall n,m:nat. (gcd m n) = (S O) \to
  32 totient (n*m) = (totient n)*(totient m).
  33 intro.
  34 apply (nat_case n)
  35 [ intros.
  36   auto
  37   (*simplify.
  38   reflexivity*)
  39 | intros 2.
  40   apply (nat_case m1)
  41   [ rewrite < sym_times.
  42     rewrite < (sym_times (totient O)).
  43     simplify.
  44     intro.
  45     reflexivity
  46   | intros.
  47     unfold totient.
  48     apply (count_times m m2 ? ? ?
  49       (\lambda b,a. cr_pair (S m) (S m2) a b)
  50       (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)))
  51     [ intros.
  52       unfold cr_pair.
  53       apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
  54       [ unfold min.
  55         apply le_min_aux_r
  56       | auto
  57         (*unfold lt.
  58         apply (nat_case ((S m)*(S m2)))
  59         [ apply le_n
  60         | intro.
  61           apply le_n
  62         ]*)
  63       ]
  64     | intros.
  65       generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  66       intro.
  67       elim H3.
  68       apply H4
  69     | intros.
  70       generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  71       intro.
  72       elim H3.
  73       apply H5
  74     | intros.
  75       generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  76       intro.
  77       elim H3.
  78       apply eqb_elim
  79       [ intro.
  80         rewrite > eq_to_eqb_true
  81         [ rewrite > eq_to_eqb_true
  82           [ reflexivity
  83           | rewrite < H4.
  84             rewrite > sym_gcd.
  85             rewrite > gcd_mod
  86             [ apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
  87               [ auto
  88                 (*unfold lt.
  89                 apply le_S_S.
  90                 apply le_O_n*)
  91               | auto
  92                 (*unfold lt.
  93                 apply le_S_S.
  94                 apply le_O_n*)
  95               | assumption
  96               ]
  97             | auto
  98               (*unfold lt.
  99               apply le_S_S.
 100               apply le_O_n*)
 101             ]
 102           ]
 103         | rewrite < H5.
 104           rewrite > sym_gcd.
 105           rewrite > gcd_mod
 106           [ apply (gcd_times_SO_to_gcd_SO ? ? (S m))
 107             [ auto
 108               (*unfold lt.
 109               apply le_S_S.
 110               apply le_O_n*)
 111             | auto
 112               (*unfold lt.
 113               apply le_S_S.
 114               apply le_O_n*)
 115             | auto
 116               (*rewrite > sym_times.
 117               assumption*)
 118             ]
 119           | auto
 120             (*unfold lt.
 121             apply le_S_S.
 122             apply le_O_n*)
 123           ]
 124         ]
 125       | intro.
 126         apply eqb_elim
 127         [ intro.
 128           apply eqb_elim
 129           [ intro.
 130             apply False_ind.
 131             apply H6.
 132             apply eq_gcd_times_SO
 133             [ auto
 134               (*unfold lt.
 135               apply le_S_S.
 136               apply le_O_n*)
 137             | auto
 138               (*unfold lt.
 139               apply le_S_S.
 140               apply le_O_n*)
 141             | rewrite < gcd_mod
 142               [ auto
 143                 (*rewrite > H4.
 144                 rewrite > sym_gcd.
 145                 assumption*)
 146               | auto
 147                 (*unfold lt.
 148                 apply le_S_S.
 149                 apply le_O_n*)
 150               ]
 151             | rewrite < gcd_mod
 152               [ auto
 153                 (*rewrite > H5.
 154                 rewrite > sym_gcd.
 155                 assumption*)
 156               | auto
 157                 (*unfold lt.
 158                 apply le_S_S.
 159                 apply le_O_n*)
 160               ]
 161             ]
 162           | intro.
 163             reflexivity
 164           ]
 165         | intro.
 166           reflexivity
 167         ]
 168       ]
 169     ]
 170   ]
 171 ]
 172 qed.