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