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