matita/matita/lib/arithmetics/ord.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||
   8     \   /  This file is distributed under the terms of the
   9      \ /   GNU General Public License Version 2
  10       V_____________________________________________________________*)
  11
  12 include "arithmetics/exp.ma".
  13 include "basics/types.ma".
  14 include "arithmetics/primes.ma".
  15 include "arithmetics/gcd.ma".
  16
  17 let rec p_ord_aux p n m ≝
  18   match n \mod m with
  19   [ O ⇒
  20     match p with
  21       [ O ⇒ 〈O,n〉
  22       | S p ⇒ let 〈q,r〉 ≝ p_ord_aux p (n / m) m in 〈S q,r〉]
  23   | S a ⇒ 〈O,n〉].
  24
  25 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
  26 definition p_ord ≝ λn,m:nat.p_ord_aux n n m.
  27
  28 lemma p_ord_aux_0: ∀n,m.p_ord_aux 0 n m = 〈0,n〉.
  29 #n #m whd in match (p_ord_aux 0??); cases (n\mod m) normalize //
  30 qed.
  31
  32 lemma p_ord_aux_Strue: ∀n,m,p,q,r.
  33  n\mod m = 0 → p_ord_aux p (n / m) m = 〈q,r〉 →
  34  p_ord_aux (S p) n m = 〈S q,r〉.
  35 #n #m #p #q #r whd in match (p_ord_aux (S p)??); #H >H
  36 #Hord whd in ⊢(??%?); >Hord //
  37 qed.
  38
  39 lemma p_ord_aux_false: ∀p,n,m,a.
  40  n\mod m = (S a) → p_ord_aux p n m = 〈0,n〉.
  41 #p #n #m #a cases p whd in match (p_ord_aux ???);
  42   [#H whd in match (p_ord_aux ???); >H //
  43   |#p1 #H whd in match (p_ord_aux ???); >H //
  44   ]
  45 qed.
  46
  47 (* the definition of p_ord_aux only makes sense for m>1.
  48    In case m=1 we always end up with the pair 〈p,n〉 *)
  49
  50 lemma p_ord_degenerate: ∀p,n. p_ord_aux p n 1 = 〈p,n〉.
  51 #p elim p // #p1 #Hind #n
  52 cut (mod n 1 = 0) [@divides_to_mod_O //] #Hmod
  53 >(p_ord_aux_Strue … (Hind … ) ) // >(div_mod n 1) in ⊢ (???%); //
  54 qed.
  55
  56 theorem p_ord_aux_to_exp: ∀p,n,m,q,r. O < m →
  57   p_ord_aux p n m = 〈q,r〉 → n = m \sup q *r .
  58 #p elim p
  59   [#n #m @(nat_case (n \mod m))
  60     [#Hmod #q #r #posm >p_ord_aux_0 #Hqr destruct (Hqr) //
  61     |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) //
  62     ]
  63   |#p1 #Hind #n #m @(nat_case (n \mod m))
  64     [#Hmod #q #r #posm lapply (refl …(p_ord_aux p1 (n/m) m));
  65      cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1
  66      >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??);
  67      >(div_mod n m) >Hmod <plus_n_O >(Hind … H1) //
  68     |#a #H #q #r #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr) //
  69     ]
  70   ]
  71 qed.
  72
  73 (* questo va spostato in primes1.ma *)
  74 theorem p_ord_exp: ∀n,m,i. O < m → n \mod m ≠ O →
  75   ∀p. i ≤ p → p_ord_aux p (m \sup i * n) m = 〈i,n〉.
  76 #n #m #i #posm #Hmod
  77 cut (∃a.n\mod m = S a)
  78   [@(nat_case (n\mod m)) [#H @False_ind /2/|#a #Hmod1 %{a} //]] * #mod1 #Hmod1
  79 elim i
  80   [#p normalize #posp <plus_n_O @(p_ord_aux_false … Hmod1)
  81   |-i #i #Hind #p
  82    @(nat_case p) [#Hp >Hp #Habs @False_ind @(absurd … Habs) //]
  83    #p1 #Hp1 #lep1
  84    cut (((m \sup (S i)*n) \mod m) = O)
  85     [whd in match (exp ??); @divides_to_mod_O // %{(m^i*n)} //] #Hmod2
  86    @(p_ord_aux_Strue … Hmod2) <(Hind p1) [2: @le_S_S_to_le //]
  87    @eq_f2 // whd in match (exp ??); >associative_times >(commutative_times m)
  88    <associative_times >div_times //
  89   ]
  90 qed.
  91
  92 theorem p_ord_aux_to_not_mod_O: ∀p,n,m,q,r. 1<m → O<n → n≤p →
  93   p_ord_aux p n m = 〈q,r〉 → r \mod m ≠ O.
  94 #p elim p
  95   [#n #m #q #r #_ #posn #nposn @False_ind @(absurd … posn) /2/
  96   |#p1 #Hind #n #m @(nat_case (n \mod m))
  97     [#Hmod #q #r #lt1m #posn #len lapply (refl …(p_ord_aux p1 (n/m) m));
  98      cases (p_ord_aux p1 (n/m) m) in ⊢ (???%→?); #q1 #r1 #H1
  99      >(p_ord_aux_Strue … Hmod H1) #H destruct (H) whd in match (exp ??);
 100      @(Hind … lt1m … H1)
 101       [@(pos_div … posn Hmod) @lt_to_le //
 102       |@le_S_S_to_le @(transitive_le … len) @lt_times_to_lt_div
 103        >(times_n_1 n) in ⊢ (?%?); @monotonic_lt_times_r //
 104       ]
 105     |#a #H #q #r #lt1m #posn #posm >(p_ord_aux_false … H) #Hqr destruct (Hqr)
 106      >H @sym_not_eq //
 107     ]
 108   ]
 109 qed.
 110
 111 theorem p_ord_exp1: ∀p,n,q,r. O < p → p ∤ r →
 112   n = p \sup q * r → p_ord n p = 〈q,r〉.
 113 #p #n #q #r #posp #ndivpr #Hn >Hn -Hn -n @(p_ord_exp … posp)
 114   [@(not_to_not … ndivpr) /2/
 115   |@(transitive_le ? (p \sup q))
 116     [cut (1<p)
 117       [cases (le_to_or_lt_eq … posp) // #eqp1 @False_ind @(absurd ?? ndivpr)
 118        <eqp1 % //]
 119      #lt1p elim q // -q #q whd in match (exp ??);
 120      cases q [#_ normalize <plus_n_O @lt_to_le //]
 121      #q1 #Hind @(lt_to_le_to_lt ? ((S q1)*2))
 122       [>(times_n_1 (S q1)) in ⊢ (?%?); @monotonic_lt_times_r //
 123       |@le_times //
 124       ]
 125     |>(times_n_1 (p^q)) in ⊢ (?%?); @le_times //
 126      lapply ndivpr -ndivpr cases r // #Habs @False_ind @(absurd ?? Habs) % //
 127     ]
 128   ]
 129 qed.
 130
 131 theorem p_ord_to_exp1: ∀p,n,q,r. 1<p → O<n → p_ord n p = 〈q,r〉 →
 132   p ∤ r ∧ n = p \sup q * r.
 133 #p #n #q #r #lt1p #posn #Hord %
 134   [@(not_to_not … (p_ord_aux_to_not_mod_O … lt1p posn (le_n n)… Hord))
 135    @divides_to_mod_O @lt_to_le //
 136   |@(p_ord_aux_to_exp n …Hord) @lt_to_le //
 137   ]
 138 qed.
 139
 140 theorem eq_p_ord_q_O: ∀p,n,q. p_ord n p = 〈q,O〉 → n=O ∧ q=O.
 141 #p #n whd in match (p_ord ??);  cases n
 142   [#q cases p normalize [|#q1] #H destruct (H) % //
 143   |#n1 #q cases p
 144     [normalize #H destruct (H)
 145     |#p1 cases p1
 146       [>p_ord_degenerate #H destruct (H)
 147       |#p2 lapply (refl …(p_ord_aux (S n1) (S n1) (S (S p2))));
 148        cases (p_ord_aux (S n1) (S n1) (S (S p2))) in ⊢ (???%→?); #qa #ra #H
 149        lapply (p_ord_to_exp1 (S (S p2)) (S n1) … H) //
 150        * #_ #H1 >H #H2 @False_ind destruct (H2) <times_n_O in H1;
 151        #Habs destruct (Habs)
 152       ]
 153     ]
 154   ]
 155 qed.
 156
 157 theorem p_ord_times: ∀p,a,b,qa,ra,qb,rb. prime p → O < a → O < b
 158  → p_ord a p = 〈qa,ra〉  → p_ord b p = 〈qb,rb〉
 159   → p_ord (a*b) p = 〈qa + qb, ra*rb〉.
 160 #p #a #b #qa #ra #qb #rb #Hprime #posa #posb #porda #pordb
 161 cut (1<p) [@prime_to_lt_SO //] #Hp1
 162 cases (p_ord_to_exp1 ???? Hp1 posa porda) -posa -porda #Hdiva #Ha
 163 elim (p_ord_to_exp1 ???? Hp1 posb pordb) -posb -pordb #Hdivb #Hb
 164 @p_ord_exp1
 165   [@lt_to_le //
 166   |% #Hdiv cases (divides_times_to_divides ? ? ? Hprime Hdiv)
 167    #Habs @absurd /2/
 168   |>Ha >Hb -Ha -Hb //
 169   ]
 170 qed.
 171
 172 theorem fst_p_ord_times: ∀p,a,b. prime p → O < a → O < b →
 173   fst ?? (p_ord (a*b) p) = (fst ?? (p_ord a p)) + (fst ?? (p_ord b p)).
 174 #p #a #b #primep #posa #posb
 175 >(p_ord_times p a b (fst ?? (p_ord a p)) (snd ?? (p_ord a p))
 176   (fst ?? (p_ord b p)) (snd ? ? (p_ord b p)) primep posa posb) //
 177 qed.
 178
 179 theorem p_ord_p: ∀p:nat. 1 < p → p_ord p p = 〈1,1〉.
 180 #p #ltp1 @p_ord_exp1
 181   [@lt_to_le //
 182   |% #divp1 @(absurd … ltp1) @le_to_not_lt @divides_to_le //
 183   |//
 184   ]
 185 qed.
 186
 187 (* p_ord and divides *)
 188 theorem divides_to_p_ord: ∀p,a,b,c,d,n,m:nat. O < n → O < m → prime p
 189 → divides n m → p_ord n p = 〈a,b〉 →
 190   p_ord m p = 〈c,d〉 → divides b d ∧ a ≤ c.
 191 #p #a #b #c #d #n #m #posn #posm #primep #divnm #ordn #ordm
 192 cut (1<p) [@prime_to_lt_SO //] #Hposp
 193 cases (p_ord_to_exp1 ? ? ? ? Hposp posn ordn) #divn #eqn
 194 cases (p_ord_to_exp1 ? ? ? ? Hposp posm ordm) #divm #eqm %
 195   [@(gcd_1_to_divides_times_to_divides b (exp p c))
 196     [cases (le_to_or_lt_eq ?? (le_O_n b)) //
 197     |elim c
 198       [>commutative_gcd //
 199       |#c0 #Hind @eq_gcd_times_1
 200         [@lt_O_exp @lt_to_le //
 201         |@lt_to_le //
 202         |@Hind
 203         |>commutative_gcd @prime_to_gcd_1 //
 204         ]
 205       ]
 206     |@(transitive_divides ? n) [%{(exp p a)} // |<eqm //]
 207     ]
 208   |@(le_exp_to_le p) //
 209    @divides_to_le
 210     [@lt_O_exp @lt_to_le //
 211     |@(gcd_1_to_divides_times_to_divides ? d)
 212       [@lt_O_exp @lt_to_le //
 213       |elim a
 214         [@gcd_SO_n
 215         |#a0 #Hind whd in match (exp ??);
 216          >commutative_gcd @eq_gcd_times_1
 217           [@lt_O_exp @lt_to_le //
 218           |@lt_to_le //
 219           |/2/
 220           |>commutative_gcd @prime_to_gcd_1 //
 221           ]
 222         ]
 223       |@(transitive_divides ? n) // %{b} //
 224       ]
 225     ]
 226   ]
 227 qed.
 228
 229 (* p_ord and primes *)
 230 theorem not_divides_to_p_ord_O: ∀n,i.
 231   (nth_prime i) ∤ n → p_ord n (nth_prime i) = 〈O,n〉.
 232 #n #i #H @p_ord_exp1 //
 233 qed.
 234
 235 theorem p_ord_O_to_not_divides: ∀n,i,r. O < n →
 236   p_ord n (nth_prime i) = 〈O,r〉
 237   → (nth_prime i) ∤ n.
 238 #n #i #r #posn #Hord
 239 lapply (p_ord_to_exp1 … Hord) // * #H
 240 normalize <plus_n_O //
 241 qed.
 242
 243 theorem p_ord_to_not_eq_O : ∀n,p,q,r. 1<n →
 244   p_ord n (nth_prime p) = 〈q,r〉 → r≠O.
 245 #n #p #q #r #lt1n #Hord
 246 cut (O<n) [@lt_to_le //] #posn
 247 lapply (p_ord_to_exp1 …posn … Hord)
 248   [@lt_SO_nth_prime_n
 249   |* #H1 #H2 @(not_to_not …(lt_to_not_eq … posn))
 250    #eqr >eqr in H2; //
 251   ]
 252 qed.
 253
 254 definition ord :nat → nat → nat ≝
 255   λn,p. fst ?? (p_ord n p).
 256
 257 definition ord_rem :nat → nat → nat ≝
 258   λn,p. snd ?? (p_ord n p).
 259
 260 lemma ord_eq: ∀n,p. ord n p = fst ?? (p_ord n p). //
 261 qed.
 262
 263 lemma ord_rem_eq: ∀n,p. ord_rem n p = snd ?? (p_ord n p). //
 264 qed.
 265
 266 theorem divides_to_ord: ∀p,n,m:nat.
 267   O < n → O < m → prime p → divides n m
 268   → divides (ord_rem n p) (ord_rem m p) ∧ (ord n p) ≤ (ord m p).
 269 #p #n #m #H #H1 #H2 #H3
 270 @(divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
 271   [@eq_pair_fst_snd|@eq_pair_fst_snd]
 272 qed.
 273
 274 theorem divides_to_divides_ord_rem: ∀p,n,m:nat.
 275 O < n → O < m → prime p → divides n m →
 276   divides (ord_rem n p) (ord_rem m p).
 277 #p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) //
 278 qed.
 279
 280 theorem divides_to_le_ord: ∀p,n,m:nat.
 281 O < n → O < m → prime p → divides n m →
 282   ord n p ≤ ord m p.
 283 #p #n #m #H #H1 #H2 #H3 cases (divides_to_ord p n m H H1 H2 H3) //
 284 qed.
 285
 286 theorem exp_ord: \forall p,n. 1 < p → O < n →
 287   n = p \sup (ord n p) * (ord_rem n p).
 288 #p #n #H #H1
 289 cases (p_ord_to_exp1 p n (ord n p) (ord_rem n p) H H1 ?)
 290   [// |@eq_pair_fst_snd]
 291 qed.
 292
 293 theorem divides_ord_rem: ∀p,n. 1 < p → O < n
 294   → divides (ord_rem n p) n.
 295 #p #n #H #H1 %{(p \sup (ord n p))} >commutative_times @exp_ord //
 296 qed.
 297
 298 theorem lt_O_ord_rem: ∀p,n. 1 < p → O < n → O < ord_rem n p.
 299 #p #n #H #H1
 300 cases (le_to_or_lt_eq … (le_O_n (ord_rem n p))) //
 301 #remO lapply(divides_ord_rem ?? H H1) <remO -remO #Hdiv0
 302 @False_ind @(absurd (0=n)) [cases Hdiv0 // | @lt_to_not_eq //]
 303 qed.
 304
 305 (* properties of ord e ord_rem *)
 306
 307 theorem ord_times: ∀p,m,n.O<m → O<n → prime p →
 308   ord (m*n) p = ord m p+ord n p.
 309 #p #m #n #H #H1 #H2
 310 lapply (p_ord_times ??? (ord m p) (ord_rem m p) (ord n p) (ord_rem n p) H2 H H1
 311   (eq_pair_fst_snd …) (eq_pair_fst_snd …)) #H3
 312   @(eq_f … (fst …) … H3)
 313 qed.
 314
 315 theorem ord_exp: ∀p,m. 1 < p → ord (exp p m) p = m.
 316 #p #m #H >ord_eq >(p_ord_exp1 p (exp p m) m (S O)) //
 317   [@(not_to_not … (lt_to_not_le … H)) @divides_to_le //
 318   |@lt_to_le //
 319   ]
 320 qed.
 321
 322 theorem not_divides_to_ord_O:
 323 ∀p,m. prime p → p ∤ m → ord m p = O.
 324 #p #m #H #H1 >ord_eq >(p_ord_exp1 p m O m) // @prime_to_lt_O //
 325 qed.
 326
 327 theorem ord_O_to_not_divides: ∀p,m. O < m → prime p →
 328   ord m p = O → p ∤ m.
 329 #p #m #H #H1 #H2
 330 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) … H … (eq_pair_fst_snd …))
 331   [@prime_to_lt_SO //
 332   |* #H3 >H2 >commutative_times <times_n_1 //
 333   ]
 334 qed.
 335
 336 theorem divides_to_not_ord_O:
 337 ∀p,m. O < m → prime p → divides p m →
 338   ord m p ≠ O.
 339 #p #m #H #H1 #H2 % #H3 @(absurd … H2) @(ord_O_to_not_divides ? ? H H1 H3)
 340 qed.
 341
 342 theorem not_ord_O_to_divides:
 343 ∀p,m. O < m → prime p → (ord m p ≠ O) → divides p m.
 344 #p #m #H #H1 #H2  >(exp_ord p m) in ⊢ (??%);
 345   [@(transitive_divides ? (exp p (ord m p)))
 346     [lapply H2 cases (ord m p)
 347       [* #H3 @False_ind @H3 //
 348       |#a #_ normalize % //
 349       ]
 350     |%{(ord_rem m p)} //
 351     ]
 352   |//
 353   |@prime_to_lt_SO //
 354   ]
 355 qed.
 356
 357 theorem not_divides_ord_rem: ∀m,p.O< m → 1 < p →
 358   p ∤  (ord_rem m p).
 359 #m #p #H #H1
 360 lapply (p_ord_to_exp1 p m (ord m p) (ord_rem m p) ?? (eq_pair_fst_snd …)) // *
 361 #H2 #H3 @H2
 362 qed.
 363
 364 theorem ord_ord_rem: ∀p,q,m. O < m → prime p → prime q →q < p →
 365   ord (ord_rem m p) q = ord m q.
 366 #p #q #m #H #H1 #H2 #H3 >(exp_ord p m) in ⊢ (???(?%?));
 367   [>(ord_times … H2)
 368     [>not_divides_to_ord_O in ⊢ (???(?%?)); //
 369      @(not_to_not … (lt_to_not_eq ? ? H3))
 370      @(divides_exp_to_eq ? ? ? H2 H1)
 371     |@lt_O_ord_rem // @prime_to_lt_SO //
 372     |@lt_O_exp @prime_to_lt_O //
 373     ]
 374   |//
 375   |@prime_to_lt_SO //
 376   ]
 377 qed.
 378
 379 theorem lt_ord_rem: ∀n,m. prime n → O < m →
 380   divides n m → ord_rem m n < m.
 381 #n #m #H #H1 #H2
 382 cases (le_to_or_lt_eq (ord_rem m n) m ?)
 383   [//
 384   |#Hm @False_ind <Hm in H2; #Habs @(absurd ? Habs)
 385    @not_divides_ord_rem // @prime_to_lt_SO //
 386   |@divides_to_le //
 387    @divides_ord_rem // @prime_to_lt_SO //
 388   ]
 389 qed.
 390
 391 (* p_ord_inv may be used to encode the pair ord and rem into
 392    a single natural number. *)
 393
 394 definition p_ord_inv ≝ λp,m,x.
 395   let 〈q,r〉 ≝ p_ord x p in r*m+q.
 396
 397 theorem  eq_p_ord_inv: ∀p,m,x.
 398   p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
 399 #p #m #x normalize cases(p_ord_aux x x p) //
 400 qed.
 401
 402 theorem div_p_ord_inv:
 403 ∀p,m,x. ord x p < m → p_ord_inv p m x / m = ord_rem x p.
 404 #p #m #x >eq_p_ord_inv @div_plus_times
 405 qed.
 406
 407 theorem mod_p_ord_inv:
 408 ∀p,m,x. ord x p < m → p_ord_inv p m x \mod m = ord x p.
 409 #p #m #x >eq_p_ord_inv @mod_plus_times
 410 qed.