matita/library/nat/totient1.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/nat/totient1".
  16
  17 include "nat/totient.ma".
  18 include "nat/iteration2.ma".
  19 include "nat/gcd_properties1.ma".
  20
  21 (* This file contains the proof of the following theorem about Euler's totient
  22  * function:
  23
  24    The sum of the applications of Phi function over the divisor of a natural
  25    number n is equal to n
  26  *)
  27
  28 (*simple auxiliary properties*)
  29 theorem lt_O_to_divides_to_lt_O_div:
  30 \forall a,b:nat.
  31 O \lt b \to a \divides b \to O \lt (b/a).
  32 intros.
  33 apply (O_lt_times_to_O_lt ? a).
  34 rewrite > (divides_to_div a b);
  35   assumption.
  36 qed.
  37
  38 (*tha main theorem*)
  39 theorem sigma_p_Sn_divides_b_totient_n: \forall n. O \lt n \to sigma_p (S n) (\lambda d.divides_b d n) totient = n.
  40 intros.
  41 unfold totient.
  42 apply (trans_eq ? ?
  43 (sigma_p (S n) (\lambda d:nat.divides_b d n)
  44 (\lambda d:nat.sigma_p (S n) (\lambda m:nat.andb (leb (S m) d) (eqb (gcd m d) (S O))) (\lambda m:nat.S O))))
  45 [ apply eq_sigma_p1
  46   [ intros.
  47     reflexivity
  48   | intros.
  49     apply sym_eq.
  50     apply (trans_eq ? ?
  51      (sigma_p x (\lambda m:nat.leb (S m) x\land eqb (gcd m x) (S O)) (\lambda m:nat.S O)))
  52     [ apply false_to_eq_sigma_p
  53       [ apply lt_to_le.
  54         assumption
  55       | intros.
  56         rewrite > lt_to_leb_false
  57         [ reflexivity
  58         | apply le_S_S.
  59           assumption
  60         ]
  61       ]
  62     | apply eq_sigma_p
  63       [ intros.
  64         rewrite > le_to_leb_true
  65         [ reflexivity
  66         | assumption
  67         ]
  68       | intros.
  69         reflexivity
  70       ]
  71     ]
  72   ]
  73 | apply (trans_eq ? ? (sigma_p n (\lambda x.true) (\lambda x.S O)))
  74   [ apply sym_eq.
  75     apply (sigma_p_knm
  76      (\lambda x. (S O))
  77      (\lambda i,j.j*(n/i))
  78      (\lambda p. n / (gcd p n))
  79      (\lambda p. p / (gcd p n))
  80     );intros
  81     [ cut (O \lt (gcd x n))
  82       [split
  83       [ split
  84         [ split
  85           [ split
  86             [ apply divides_to_divides_b_true
  87               [ apply (O_lt_times_to_O_lt ? (gcd x n)).
  88                 rewrite > (divides_to_div (gcd x n) n)
  89                 [ assumption
  90                 | apply (divides_gcd_m)
  91                 ]
  92               | rewrite > sym_gcd.
  93                 apply (divides_times_to_divides_div_gcd).
  94                 apply (witness n (x * n) x).
  95                 apply (symmetric_times x n)
  96               ]
  97             | apply (true_to_true_to_andb_true)
  98               [ apply (le_to_leb_true).
  99                 change with (x/(gcd x n) \lt n/(gcd x n)).
 100                 apply (lt_times_n_to_lt (gcd x n) ? ?)
 101                 [ assumption
 102                 | rewrite > (divides_to_div (gcd x n) x)
 103                   [ rewrite > (divides_to_div (gcd x n) n)
 104                     [ assumption
 105                     | apply divides_gcd_m
 106                     ]
 107                   | apply divides_gcd_n
 108                   ]
 109                 ]
 110               | apply cic:/matita/nat/compare/eq_to_eqb_true.con.
 111                 rewrite > (eq_gcd_div_div_div_gcd x n (gcd x n))
 112                 [ apply (div_n_n (gcd x n) Hcut)
 113                 | assumption
 114                 | apply divides_gcd_n
 115                 | apply divides_gcd_m
 116                 ]
 117               ]
 118             ]
 119           | apply (inj_times_l1 (n/(gcd x n)))
 120             [ apply lt_O_to_divides_to_lt_O_div
 121               [ assumption
 122               | apply divides_gcd_m
 123               ]
 124             | rewrite > associative_times.
 125               rewrite > (divides_to_div (n/(gcd x n)) n)
 126               [ rewrite > sym_times.
 127                 rewrite > (divides_to_eq_times_div_div_times x)
 128                 [ apply (inj_times_l1 (gcd x n) Hcut).
 129                   rewrite > (divides_to_div (gcd x n) (x * n))
 130                   [ rewrite > assoc_times.
 131                     rewrite > (divides_to_div (gcd x n) x)
 132                     [ apply sym_times
 133                     | apply divides_gcd_n
 134                     ]
 135                   | apply (trans_divides ? x)
 136                     [ apply divides_gcd_n
 137                     | apply (witness ? ? n).
 138                       reflexivity
 139                     ]
 140                   ]
 141                 | assumption
 142                 | apply divides_gcd_m
 143                 ]
 144               | apply (witness ? ? (gcd x n)).
 145                 rewrite > divides_to_div
 146                 [ reflexivity
 147                 | apply divides_gcd_m
 148                 ]
 149               ]
 150             ]
 151           ]
 152         | apply (le_to_lt_to_lt ? n)
 153           [ apply le_div.
 154             assumption
 155           | change with ((S n) \le (S n)).
 156             apply le_n
 157           ]
 158         ]
 159       | apply (le_to_lt_to_lt ? x)
 160         [ apply le_div.
 161           assumption
 162         | apply (trans_lt ? n ?)
 163           [ assumption
 164           | change with ((S n) \le (S n)).
 165             apply le_n
 166           ]
 167         ]
 168       ]
 169     | apply (divides_to_lt_O ? n)
 170       [ assumption
 171       | apply divides_gcd_m
 172       ]
 173     ]
 174     | cut (i \divides n)
 175       [ cut (j \lt i)
 176         [ cut ((gcd j i) = (S O) )
 177           [ cut ((gcd (j*(n/i)) n) = n/i)
 178             [ split
 179               [ split
 180                 [ split
 181                   [ reflexivity
 182                   | rewrite > Hcut3.
 183                     apply (div_div);
 184                       assumption
 185                   ]
 186                 | rewrite > Hcut3.
 187                   rewrite < divides_to_eq_times_div_div_times
 188                   [ rewrite > div_n_n
 189                     [ apply sym_eq.
 190                       apply times_n_SO.
 191                     | apply lt_O_to_divides_to_lt_O_div;
 192                         assumption
 193                     ]
 194                   | apply lt_O_to_divides_to_lt_O_div;
 195                       assumption
 196                   | apply divides_n_n
 197                   ]
 198                 ]
 199               | rewrite < (divides_to_div i n) in \vdash (? ? %)
 200                 [ rewrite > sym_times.
 201                   apply (lt_times_r1)
 202                   [ apply lt_O_to_divides_to_lt_O_div;
 203                       assumption
 204                   | assumption
 205                   ]
 206                 | assumption
 207                 ]
 208               ]
 209             | rewrite < (divides_to_div i n) in \vdash (? ? (? ? %) ?)
 210               [ rewrite > (sym_times j).
 211                 rewrite > times_n_SO in \vdash (? ? ? %).
 212                 rewrite < Hcut2.
 213                 apply eq_gcd_times_times_times_gcd
 214               | assumption
 215               ]
 216             ]
 217           | apply eqb_true_to_eq.
 218             apply (andb_true_true_r (leb (S j) i)).
 219             assumption
 220           ]
 221         | change with ((S j) \le i).
 222           cut((leb (S j) i) = true)
 223           [ change with(
 224             match (true) with
 225             [ true  \Rightarrow ((S j) \leq i)
 226             | false \Rightarrow ((S j) \nleq i)]
 227             ).
 228             rewrite < Hcut1.
 229             apply (leb_to_Prop)
 230           | apply (andb_true_true (leb (S j) i) (eqb (gcd j i) (S O))).
 231             assumption
 232           ]
 233         ]
 234         | apply (divides_b_true_to_divides).
 235           assumption
 236       ]
 237     ]
 238   | apply (sigma_p_true).
 239   ]
 240 ]
 241 qed.
 242
 243