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