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/count.ma".
  18 include "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.simplify.reflexivity
  36   |intros 2.apply (nat_case m1)
  37     [rewrite < sym_times.
  38      rewrite < (sym_times (totient O)).
  39      simplify.intro.reflexivity.
  40      |intros.
  41       unfold totient.
  42       apply (count_times m m2 ? ? ?
  43              (\lambda b,a. cr_pair (S m) (S m2) a b)
  44              (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2)))
  45        [intros.unfold cr_pair.
  46         apply (le_to_lt_to_lt ? (pred ((S m)*(S m2))))
  47           [unfold min.
  48            apply le_min_aux_r
  49           |unfold lt.
  50            apply (nat_case ((S m)*(S m2)))
  51             [apply le_n|intro.apply le_n]
  52           ]
  53        |intros.
  54         generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  55         intro.elim H3.
  56         apply H4
  57        |intros.
  58         generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  59         intro.elim H3.
  60         apply H5
  61        |intros.
  62         generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  63         intro.elim H3.
  64         apply eqb_elim
  65           [intro.
  66            rewrite > eq_to_eqb_true
  67              [rewrite > eq_to_eqb_true
  68                [reflexivity
  69                |rewrite < H4.
  70                 rewrite > sym_gcd.
  71                 rewrite > gcd_mod
  72                   [apply (gcd_times_SO_to_gcd_SO ? ? (S m2))
  73                     [unfold lt.apply le_S_S.apply le_O_n
  74                     |unfold lt.apply le_S_S.apply le_O_n
  75                     |assumption
  76                     ]
  77                   |unfold lt.apply le_S_S.apply le_O_n
  78                   ]
  79                ]
  80             |rewrite < H5.
  81              rewrite > sym_gcd.
  82              rewrite > gcd_mod
  83                [apply (gcd_times_SO_to_gcd_SO ? ? (S m))
  84                   [unfold lt.apply le_S_S.apply le_O_n
  85                   |unfold lt.apply le_S_S.apply le_O_n
  86                   |rewrite > sym_times.assumption
  87                   ]
  88                |unfold lt.apply le_S_S.apply le_O_n
  89                ]
  90             ]
  91           |intro.
  92            apply eqb_elim
  93            [intro.apply eqb_elim
  94               [intro.apply False_ind.
  95                apply H6.
  96                apply eq_gcd_times_SO
  97                  [unfold lt.apply le_S_S.apply le_O_n.
  98                  |unfold lt.apply le_S_S.apply le_O_n.
  99                  |rewrite < gcd_mod
 100                     [rewrite > H4.
 101                      rewrite > sym_gcd.assumption
 102                     |unfold lt.apply le_S_S.apply le_O_n
 103                     ]
 104                  |rewrite < gcd_mod
 105                     [rewrite > H5.
 106                      rewrite > sym_gcd.assumption
 107                     |unfold lt.apply le_S_S.apply le_O_n
 108                     ]
 109                  ]
 110               |intro.reflexivity
 111               ]
 112            |intro.reflexivity
 113            ]
 114          ]
 115        ]
 116      ]
 117    ]
 118 qed.