matita/library_auto/auto/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/library_auto/nat/euler_theorem".
  16
  17 include "auto/nat/map_iter_p.ma".
  18 include "auto/nat/totient.ma".
  19
  20 (* a reformulation of totient using card insted of count *)
  21 lemma totient_card: \forall n.
  22 totient n = card n (\lambda i.eqb (gcd i n) (S O)).
  23 intro.
  24 apply (nat_case n)
  25 [ reflexivity
  26 | intro.
  27   apply (nat_case m)
  28   [ reflexivity
  29   | intro.
  30     apply count_card1;auto
  31     (*[ reflexivity
  32     | auto.rewrite > gcd_n_n.
  33       reflexivity
  34     ]*)
  35   ]
  36 ]
  37 qed.
  38
  39 theorem gcd_pi_p: \forall n,k. O < k \to k \le n \to
  40 gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) k) = (S O).
  41 intros 3.
  42 elim H
  43 [ rewrite > pi_p_S.
  44   cut (eqb (gcd (S O) n) (S O) = true)
  45   [ rewrite > Hcut.
  46     auto
  47     (*change with ((gcd n (S O)) = (S O)).
  48     auto*)
  49   | auto
  50     (*apply eq_to_eqb_true.auto*)
  51   ]
  52 | rewrite > pi_p_S.
  53   apply eqb_elim
  54   [ intro.
  55     change with
  56      ((gcd n ((S n1)*(pi_p (\lambda i.eqb (gcd i n) (S O)) n1))) = (S O)).
  57     apply eq_gcd_times_SO
  58     [ auto
  59       (*unfold.
  60       apply le_S.
  61       assumption*)
  62     | apply lt_O_pi_p.
  63     | auto
  64       (*rewrite > sym_gcd.
  65       assumption.*)
  66     | apply H2.
  67       auto
  68       (*apply (trans_le ? (S n1))
  69       [ apply le_n_Sn
  70       | assumption
  71       ]*)
  72     ]
  73   | intro.
  74     change with
  75       (gcd n (pi_p (\lambda i.eqb (gcd i n) (S O)) n1) = (S O)).
  76     apply H2.
  77     auto
  78     (*apply (trans_le ? (S n1))
  79     [ apply le_n_Sn
  80     | assumption
  81     ]*)
  82   ]
  83 ]
  84 qed.
  85
  86 theorem congruent_map_iter_p_times:\forall f:nat \to nat. \forall a,n:nat.
  87 O < a \to
  88 congruent
  89 (map_iter_p n (\lambda i.eqb (gcd i a) (S O)) (\lambda x.f x) (S O) times)
  90 (map_iter_p n (\lambda i.eqb (gcd i a) (S O))
  91  (\lambda x.f x \mod a) (S O) times) a.
  92 intros.
  93 elim n
  94 [ auto
  95   (*rewrite > map_iter_p_O.
  96   apply (congruent_n_n ? a)*)
  97 | apply (eqb_elim (gcd (S n1) a) (S O))
  98   [ intro.
  99     rewrite > map_iter_p_S_true
 100     [ rewrite > map_iter_p_S_true
 101       [ apply congruent_times
 102         [ assumption
 103         | auto
 104           (*apply congruent_n_mod_n.
 105           assumption*)
 106         | (*NB qui auto non chiude il goal*)
 107           assumption
 108         ]
 109       | auto
 110         (*apply eq_to_eqb_true.
 111         assumption*)
 112       ]
 113     | auto
 114       (*apply eq_to_eqb_true.
 115       assumption*)
 116     ]
 117   | intro.
 118     rewrite > map_iter_p_S_false
 119     [ rewrite > map_iter_p_S_false
 120       [ (*BN qui auto non chiude il goal*)
 121         assumption
 122       | auto
 123         (*apply not_eq_to_eqb_false.
 124         assumption*)
 125       ]
 126     | auto
 127       (*apply not_eq_to_eqb_false.
 128       assumption*)
 129     ]
 130   ]
 131 ]
 132 qed.
 133
 134 theorem permut_p_mod: \forall a,n. S O < n \to O < a \to gcd a n = (S O) \to
 135 permut_p (\lambda x:nat.a*x \mod n) (\lambda i:nat.eqb (gcd i n) (S O)) n.
 136 intros.
 137 lapply (lt_S_to_lt ? ? H) as H3.
 138 unfold permut_p.
 139 simplify.
 140 intros.
 141 split
 142 [ split
 143   [ auto
 144     (*apply lt_to_le.
 145     apply lt_mod_m_m.
 146     assumption*)
 147   | rewrite > sym_gcd.
 148     rewrite > gcd_mod
 149     [ apply eq_to_eqb_true.
 150       rewrite > sym_gcd.
 151       apply eq_gcd_times_SO
 152       [ assumption
 153       | apply (gcd_SO_to_lt_O i n H).
 154         auto
 155         (*apply eqb_true_to_eq.
 156         assumption*)
 157       | auto
 158         (*rewrite > sym_gcd.
 159         assumption*)
 160       | auto
 161         (*rewrite > sym_gcd.
 162         apply eqb_true_to_eq.
 163         assumption*)
 164       ]
 165     | assumption
 166    ]
 167   ]
 168 | intros.
 169   lapply (gcd_SO_to_lt_n ? ? H H4 (eqb_true_to_eq ? ? H5)) as H9.
 170   lapply (gcd_SO_to_lt_n ? ? H H7 (eqb_true_to_eq ? ? H6)) as H10.
 171   lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H5)) as H11.
 172   lapply (gcd_SO_to_lt_O ? ? H (eqb_true_to_eq ? ? H6)) as H12.
 173   unfold Not.
 174   intro.
 175   apply H8.
 176   apply (nat_compare_elim i j)
 177   [ intro.
 178     absurd (j < n)
 179     [ assumption
 180     | apply le_to_not_lt.
 181       apply (trans_le ? (j -i))
 182       [ apply divides_to_le
 183         [(*fattorizzare*)
 184           unfold lt.auto.
 185           (*apply (lt_plus_to_lt_l i).
 186           simplify.
 187           rewrite < (plus_minus_m_m)
 188           [ assumption
 189           | apply lt_to_le.
 190             assumption
 191           ]*)
 192         | apply (gcd_SO_to_divides_times_to_divides a)
 193           [ assumption
 194           | auto
 195             (*rewrite > sym_gcd.
 196             assumption*)
 197           | apply mod_O_to_divides
 198             [ assumption
 199             | rewrite > distr_times_minus.
 200               auto
 201             ]
 202           ]
 203         ]
 204       | auto
 205       ]
 206     ]
 207   | auto
 208     (*intro.
 209     assumption*)
 210   | intro.
 211     absurd (i < n)
 212     [ assumption
 213     | apply le_to_not_lt.
 214       apply (trans_le ? (i -j))
 215       [ apply divides_to_le
 216         [(*fattorizzare*)
 217           unfold lt.auto.
 218           (*apply (lt_plus_to_lt_l j).
 219           simplify.
 220           rewrite < (plus_minus_m_m)
 221           [ assumption
 222           | apply lt_to_le.
 223             assumption
 224           ]*)
 225         | apply (gcd_SO_to_divides_times_to_divides a)
 226           [ assumption
 227           | auto
 228             (*rewrite > sym_gcd.
 229             assumption*)
 230           | apply mod_O_to_divides
 231             [ assumption
 232             | rewrite > distr_times_minus.
 233               auto
 234             ]
 235           ]
 236         ]
 237       | auto
 238       ]
 239     ]
 240   ]
 241 ]
 242 qed.
 243
 244 theorem congruent_exp_totient_SO: \forall n,a:nat. (S O) < n \to
 245 gcd a n = (S O) \to congruent (exp a (totient n)) (S O) n.
 246 intros.
 247 cut (O < a)
 248 [ apply divides_to_congruent
 249   [ auto
 250     (*apply (trans_lt ? (S O)).
 251     apply lt_O_S.
 252     assumption*)
 253   | auto
 254     (*change with (O < exp a (totient n)).
 255     apply lt_O_exp.
 256     assumption*)
 257   | apply (gcd_SO_to_divides_times_to_divides (pi_p (\lambda i.eqb (gcd i n) (S O)) n))
 258     [ auto
 259       (*apply (trans_lt ? (S O)).
 260       apply lt_O_S.
 261       assumption*)
 262     | auto
 263       (*apply gcd_pi_p
 264       [ apply (trans_lt ? (S O)).
 265         apply lt_O_S.
 266         assumption
 267       | apply le_n
 268       ]*)
 269     | rewrite < sym_times.
 270       rewrite > times_minus_l.
 271       rewrite > (sym_times (S O)).
 272       rewrite < times_n_SO.
 273       rewrite > totient_card.
 274       rewrite > a_times_pi_p.
 275       apply congruent_to_divides
 276       [ auto
 277         (*apply (trans_lt ? (S O)).
 278         apply lt_O_S.
 279         assumption*)
 280       | apply (transitive_congruent n ?
 281          (map_iter_p n (\lambda i.eqb (gcd i n) (S O)) (\lambda x.a*x \mod n) (S O) times))
 282         [ auto
 283           (*apply (congruent_map_iter_p_times ? n n).
 284           apply (trans_lt ? (S O))
 285           [ apply lt_O_S
 286           | assumption
 287           ]*)
 288         | unfold pi_p.
 289           cut ( (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda n:nat.n) (S O) times)
 290              = (map_iter_p n (\lambda i:nat.eqb (gcd i n) (S O)) (\lambda x:nat.a*x\mod n) (S O) times))
 291           [ rewrite < Hcut1.
 292             apply congruent_n_n
 293           | apply (eq_map_iter_p_permut ? ? ? ? ? (λm.m))
 294             [ apply assoc_times
 295             | apply sym_times
 296             | apply (permut_p_mod ? ? H Hcut H1)
 297             | simplify.
 298               apply not_eq_to_eqb_false.
 299               unfold.
 300               intro.
 301               auto
 302               (*apply (lt_to_not_eq (S O) n)
 303               [ assumption
 304               | apply sym_eq.
 305                 assumption
 306               ]*)
 307             ]
 308           ]
 309         ]
 310       ]
 311     ]
 312   ]
 313 | elim (le_to_or_lt_eq O a (le_O_n a));auto
 314   (*[ assumption
 315   | auto.absurd (gcd a n = S O)
 316     [ assumption
 317     | rewrite < H2.
 318       simplify.
 319       unfold.intro.
 320       apply (lt_to_not_eq (S O) n)
 321       [ assumption
 322       | apply sym_eq.
 323         assumption
 324       ]
 325     ]
 326   ]*)
 327 ]
 328 qed.
 329