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