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