matita/library/nat/euler_theorem.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/euler_theorem".
  16
  17 include "nat/map_iter_p.ma".
  18 include "nat/totient.ma".
  19
  20 (*
  21 lemma count_card: \forall p.\forall n.
  22 p O = false \to count (S n) p = card n p.
  23 intros.elim n
  24   [simplify.rewrite > H. reflexivity
  25   |simplify.
  26    rewrite < plus_n_O.
  27    apply eq_f.assumption
  28   ]
  29 qed.
  30
  31 lemma count_card1: \forall p.\forall n.
  32 p O = false \to p n = false \to count n p = card n p.
  33 intros 3.apply (nat_case n)
  34   [intro.simplify.rewrite > H. reflexivity
  35   |intros.rewrite > (count_card ? ? H).
  36    simplify.rewrite > H1.reflexivity
  37   ]
  38 qed.
  39
  40
  41 ( a reformulation of totient using card insted of count )
  42
  43 lemma totient_card: \forall n.
  44 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
  45 intro.apply (nat_case n)
  46   [reflexivity
  47   |intro.apply (nat_case m)
  48     [reflexivity
  49     |intro.apply count_card1
  50       [reflexivity
  51       |rewrite > gcd_n_n.reflexivity
  52       ]
  53     ]
  54   ]
  55 qed.
  56 *)
  57
  58 (*this obvious property is useful because simplify, sometimes,
  59   "simplifies too much", and doesn't allow to obtain this simple result.
  60  *)
  61 theorem card_Sn: \forall n:nat. \forall p:nat \to bool.
  62 card (S n) p = (bool_to_nat (p (S n))) + (card n p).
  63 intros.
  64 simplify.
  65 reflexivity.
  66 qed.
  67
  68 (* a reformulation of totient using card insted of sigma_p *)
  69
  70 theorem totient_card_aux: \forall n,m: nat.
  71 m = n \to
  72 sigma_p (S (S n)) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)) (\lambda x:nat. (S O))
  73 = card (S n) (\lambda m:nat.eqb (gcd m (S (S n))) (S O)).
  74 intros.
  75 rewrite < H in \vdash (? ? (? % ? ?) ?).
  76 rewrite < H in \vdash (? ? ? (? % ?)).
  77 elim (m)
  78 [ rewrite > card_Sn.
  79   cut ((eqb (gcd (S O)(S (S n))) (S O) ) = true)
  80   [ rewrite > Hcut.
  81     simplify in \vdash (? ? ? %).
  82     rewrite > true_to_sigma_p_Sn
  83     [ rewrite > false_to_sigma_p_Sn in \vdash (? ? (? ? %) ?)
  84       [ simplify in \vdash (? ? % ?).
  85         reflexivity
  86       | rewrite > gcd_O_n.
  87         apply not_eq_to_eqb_false.
  88         apply cic:/matita/nat/nat/not_eq_S.con.
  89         unfold Not.
  90         intro.
  91         cut ( (S n) \le O)
  92         [ apply (not_le_Sn_n n ?).
  93           apply (transitive_le (S n) O n ? ?);
  94           [ apply (Hcut1)
  95           | apply (le_O_n n)
  96           ]
  97         | rewrite > H1.
  98           apply le_n
  99         ]
 100       ]
 101     | assumption
 102     ]
 103   | apply eq_to_eqb_true.
 104     rewrite > gcd_SO_n.
 105     reflexivity
 106   ]
 107 | cut ((eqb (gcd (S (S n1)) (S (S n))) (S O))  = true
 108     \lor (eqb (gcd (S (S n1)) (S (S n))) (S O))  = false)
 109   [ elim Hcut
 110     [ rewrite > card_Sn.
 111       rewrite > true_to_sigma_p_Sn
 112       [ rewrite > H2.
 113         simplify in \vdash (? ? ? (? % ?)).
 114         apply eq_f.
 115         assumption
 116       | assumption
 117       ]
 118     | rewrite > card_Sn.
 119       rewrite > false_to_sigma_p_Sn
 120       [ rewrite > H2.
 121         simplify in \vdash (? ? ? (? % ?)).
 122         rewrite > sym_plus.
 123         rewrite < plus_n_O.
 124         assumption
 125       | assumption
 126       ]
 127     ]
 128   | elim (eqb (gcd (S (S n1)) (S (S n))) (S O))
 129     [ left.
 130       reflexivity
 131     | right.
 132       reflexivity
 133     ]
 134   ]
 135 ]
 136 qed.
 137
 138 lemma totient_card: \forall n.
 139 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
 140 intros.
 141 elim n
 142 [ simplify.
 143   reflexivity
 144 | elim n1
 145   [ simplify.
 146     reflexivity
 147   |
 148     (*unfold card.
 149     intros.*)
 150     (* here simplify creates problems: it seems it simplifies too much. I had to
 151      * introduce the obvious theorem card_Sn.
 152      *)
 153     rewrite > card_Sn.
 154     rewrite > (gcd_n_n (S (S n2))).
 155     cut ((eqb (S (S n2)) (S O)) = false)
 156     [ rewrite > Hcut.
 157       simplify in \vdash (? ? ? (? % ?)).
 158       rewrite > sym_plus.
 159       rewrite < (plus_n_O).
 160       unfold totient.
 161       apply (totient_card_aux n2 n2).
 162       reflexivity
 163     | apply not_eq_to_eqb_false.
 164       apply cic:/matita/nat/nat/not_eq_S.con.
 165       unfold Not.
 166       intro.
 167       cut ( (S n2) \le O)
 168         [ apply (not_le_Sn_n n2 ?).
 169           apply (transitive_le (S n2) O n2 ? ?);
 170           [ apply (Hcut)
 171           | apply (le_O_n n2)
 172           ]
 173         | rewrite > H2.
 174           apply le_n
 175         ]
 176     ]
 177   ]
 178 ]
 179 qed.
 180
 181 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
 182 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
 183 intros 3.elim H
 184   [rewrite > pi_p_S.
 185    cut (eqb (gcd (S O) n) (S O) = true)
 186     [rewrite > Hcut.
 187      change with ((gcd n (S O)) = (S O)).
 188      apply (transitive_eq nat (gcd n (S O)) (gcd (S O) n) (S O) ? ?);
 189      [ apply (sym_eq nat (gcd (S O) n) (gcd n (S O)) ?).
 190        apply (symmetric_gcd (S O) n).
 191      | apply (gcd_SO_n n).
 192      ]
 193     |apply eq_to_eqb_true.
 194      apply (gcd_SO_n n)
 195     ]
 196   |rewrite > pi_p_S.
 197    apply eqb_elim
 198     [intro.
 199      change with
 200        ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
 201      apply eq_gcd_times_SO
 202       [unfold.apply le_S.assumption
 203       |apply lt_O_pi_p.
 204       |rewrite > sym_gcd. assumption.
 205       |apply H2.
 206        apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
 207       ]
 208     |intro.
 209      change with
 210        (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
 211      apply H2.
 212      apply (trans_le ? (S n1))[apply le_n_Sn|assumption]
 213     ]
 214   ]
 215 qed.
 216
 217 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
 218 O < a \to
 219 congruent
 220 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
 221 (map_iter_p n (\lambda i.eqb (gcd i a) (S O))
 222  (\lambda x.f x \mod a) (S O) times) a.
 223 intros.
 224 elim n
 225   [rewrite > map_iter_p_O.
 226    apply (congruent_n_n ? a)
 227   |apply (eqb_elim (gcd (S n1) a) (S O))
 228     [intro.
 229      rewrite > map_iter_p_S_true
 230       [rewrite > map_iter_p_S_true
 231         [apply congruent_times
 232           [assumption
 233           |apply congruent_n_mod_n.assumption
 234           |assumption
 235           ]
 236         |apply eq_to_eqb_true.assumption
 237         ]
 238       |apply eq_to_eqb_true.assumption
 239       ]
 240     |intro.
 241      rewrite > map_iter_p_S_false
 242       [rewrite > map_iter_p_S_false
 243         [assumption
 244         |apply not_eq_to_eqb_false.assumption
 245         ]
 246       |apply not_eq_to_eqb_false.assumption
 247       ]
 248     ]
 249   ]
 250 qed.
 251
 252 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
 253 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
 254 intros.
 255 lapply (lt_S_to_lt ? ? H) as H3.
 256 unfold permut_p.
 257 simplify.
 258 intros.
 259 split
 260   [split
 261     [apply lt_to_le.
 262      apply lt_mod_m_m.
 263      assumption
 264     |rewrite > sym_gcd.
 265      rewrite > gcd_mod
 266       [apply eq_to_eqb_true.
 267        rewrite > sym_gcd.
 268        apply eq_gcd_times_SO
 269         [assumption
 270         |apply (gcd_SO_to_lt_O i n H).
 271          apply eqb_true_to_eq.
 272          assumption
 273         |rewrite > sym_gcd.assumption
 274         |rewrite > sym_gcd.apply eqb_true_to_eq.
 275          assumption
 276         ]
 277       |assumption
 278       ]
 279     ]
 280   |intros.
 281    lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
 282    lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
 283    lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
 284    lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
 285    unfold Not.intro.
 286    apply H8.
 287    apply (nat_compare_elim i j)
 288     [intro.
 289      absurd (j < n)
 290       [assumption
 291       |apply le_to_not_lt.
 292        apply (trans_le ? (j -i))
 293         [apply divides_to_le
 294           [(*fattorizzare*)
 295            apply (lt_plus_to_lt_l i).
 296            simplify.
 297            rewrite < (plus_minus_m_m)
 298             [assumption|apply lt_to_le.assumption]
 299           |apply (gcd_SO_to_divides_times_to_divides a)
 300             [assumption
 301             |rewrite > sym_gcd.assumption
 302             |apply mod_O_to_divides
 303               [assumption
 304               |rewrite > distr_times_minus.
 305                apply (divides_to_mod_O n (minus (times a j) (times a i)) ? ?);
 306                [ apply (H3).
 307                | apply (eq_mod_to_divides (times a j) (times a i) n ? ?);
 308                 [ apply (H3).
 309                 |apply (sym_eq nat (mod (times a i) n) (mod (times a j) n) ?).
 310                  apply (H13).
 311                 ]
 312                ]
 313               ]
 314             ]
 315           ]
 316         | apply (le_minus_m j i).
 317         ]
 318       ]
 319     |intro.assumption
 320     |intro.
 321      absurd (i < n)
 322       [assumption
 323       |apply le_to_not_lt.
 324        apply (trans_le ? (i -j))
 325         [apply divides_to_le
 326           [(*fattorizzare*)
 327            apply (lt_plus_to_lt_l j).
 328            simplify.
 329            rewrite < (plus_minus_m_m)
 330             [assumption|apply lt_to_le.assumption]
 331           |apply (gcd_SO_to_divides_times_to_divides a)
 332             [assumption
 333             |rewrite > sym_gcd.assumption
 334             |apply mod_O_to_divides
 335               [assumption
 336               |rewrite > distr_times_minus.
 337                apply (divides_to_mod_O n (minus (times a i) (times a j)) ? ?);
 338                [apply (H3).
 339                | apply (eq_mod_to_divides (times a i) (times a j) n ? ?);
 340                  [apply (H3).
 341                  |apply (H13).
 342                  ]
 343                ]
 344               ]
 345             ]
 346           ]
 347         | apply (le_minus_m i j).
 348         ]
 349       ]
 350     ]
 351   ]
 352 qed.
 353
 354 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
 355 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
 356 intros.
 357 cut (O < a)
 358   [ apply divides_to_congruent
 359     [apply (trans_lt ? (S O)).apply lt_O_S. assumption
 360     |change with (O < exp a (totient n)).apply lt_O_exp.assumption
 361     |apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
 362       [apply (trans_lt ? (S O)).apply lt_O_S. assumption
 363       |apply gcd_pi_p
 364         [apply (trans_lt ? (S O)).apply lt_O_S. assumption
 365         |apply le_n
 366         ]
 367       |rewrite < sym_times.
 368        rewrite > times_minus_l.
 369        rewrite > (sym_times (S O)).
 370        rewrite < times_n_SO.
 371        rewrite > totient_card.
 372        rewrite > a_times_pi_p.
 373        apply congruent_to_divides
 374         [apply (trans_lt ? (S O)).apply lt_O_S. assumption
 375         | apply (transitive_congruent n ?
 376                  (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
 377           [apply (congruent_map_iter_p_times ? n n).
 378            apply (trans_lt ? (S O))
 379             [apply lt_O_S|assumption]
 380             |unfold pi_p.
 381              cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
 382                  = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
 383               [rewrite < Hcut1.apply congruent_n_n
 384               |apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
 385                 [apply assoc_times
 386                 |apply sym_times
 387                 |apply (permut_p_mod ? ? H Hcut H1)
 388                 |simplify.
 389                  apply not_eq_to_eqb_false.
 390                  unfold.intro.
 391                  apply (lt_to_not_eq (S O) n)
 392                   [assumption|apply sym_eq.assumption]
 393                 ]
 394               ]
 395             ]
 396           ]
 397         ]
 398       ]
 399     |elim (le_to_or_lt_eq O a (le_O_n a))
 400       [assumption
 401       |absurd (gcd a n = S O)
 402         [assumption
 403         |rewrite < H2.
 404          simplify.
 405          unfold.intro.
 406          apply (lt_to_not_eq (S O) n)
 407           [assumption|apply sym_eq.assumption]
 408         ]
 409       ]
 410     ]
 411 qed.