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