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