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