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