helm/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 intro.simplify.intro.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) (\lambda x. x \mod (S m)) (\lambda x. x \mod (S m2))).
  44 intros.unfold cr_pair.
  45 apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))).
  46 unfold min.
  47 apply le_min_aux_r.
  48 change with ((S (pred ((S m)*(S m2)))) \le ((S m)*(S m2))).
  49 apply (nat_case ((S m)*(S m2))).apply le_n.
  50 intro.apply le_n.
  51 intros.
  52 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  53 intro.elim H3.
  54 apply H4.
  55 intros.
  56 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  57 intro.elim H3.
  58 apply H5.
  59 intros.
  60 generalize in match (mod_cr_pair (S m) (S m2) a b H1 H2 H).
  61 intro.elim H3.
  62 apply eqb_elim.
  63 intro.
  64 rewrite > eq_to_eqb_true.
  65 rewrite > eq_to_eqb_true.
  66 reflexivity.
  67 rewrite < H4.
  68 rewrite > sym_gcd.
  69 rewrite > gcd_mod.
  70 apply (gcd_times_SO_to_gcd_SO ? ? (S m2)).
  71 unfold lt.apply le_S_S.apply le_O_n.
  72 unfold lt.apply le_S_S.apply le_O_n.
  73 assumption.
  74 unfold lt.apply le_S_S.apply le_O_n.
  75 rewrite < H5.
  76 rewrite > sym_gcd.
  77 rewrite > gcd_mod.
  78 apply (gcd_times_SO_to_gcd_SO ? ? (S m)).
  79 unfold lt.apply le_S_S.apply le_O_n.
  80 unfold lt.apply le_S_S.apply le_O_n.
  81 rewrite > sym_times.
  82 assumption.
  83 unfold lt.apply le_S_S.apply le_O_n.
  84 intro.
  85 apply eqb_elim.
  86 intro.apply eqb_elim.
  87 intro.apply False_ind.
  88 apply H6.
  89 apply eq_gcd_times_SO.
  90 unfold lt.apply le_S_S.apply le_O_n.
  91 unfold lt.apply le_S_S.apply le_O_n.
  92 rewrite < gcd_mod.
  93 rewrite > H4.
  94 rewrite > sym_gcd.assumption.
  95 unfold lt.apply le_S_S.apply le_O_n.
  96 rewrite < gcd_mod.
  97 rewrite > H5.
  98 rewrite > sym_gcd.assumption.
  99 unfold lt.apply le_S_S.apply le_O_n.
 100 intro.reflexivity.
 101 intro.reflexivity.
 102 qed.