matita/library/nat/ord.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 (*       \ /        Matita 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/ord".
  16
  17 include "datatypes/constructors.ma".
  18 include "nat/exp.ma".
  19 include "nat/nth_prime.ma".
  20 include "nat/relevant_equations.ma". (* required by autobatch paramod *)
  21
  22 let rec p_ord_aux p n m \def
  23   match n \mod m with
  24   [ O \Rightarrow
  25     match p with
  26       [ O \Rightarrow pair nat nat O n
  27       | (S p) \Rightarrow
  28        match (p_ord_aux p (n / m) m) with
  29        [ (pair q r) \Rightarrow pair nat nat (S q) r] ]
  30   | (S a) \Rightarrow pair nat nat O n].
  31
  32 (* p_ord n m = <q,r> if m divides n q times, with remainder r *)
  33 definition p_ord \def \lambda n,m:nat.p_ord_aux n n m.
  34
  35 theorem p_ord_aux_to_Prop: \forall p,n,m. O < m \to
  36   match p_ord_aux p n m with
  37   [ (pair q r) \Rightarrow n = m \sup q *r ].
  38 intro.
  39 elim p.simplify.
  40 apply (nat_case (n \mod m)).
  41 simplify.apply plus_n_O.
  42 intros.
  43 simplify.apply plus_n_O.
  44 simplify.
  45 apply (nat_case1 (n1 \mod m)).intro.
  46 simplify.
  47 generalize in match (H (n1 / m) m).
  48 elim (p_ord_aux n (n1 / m) m).
  49 simplify.
  50 rewrite > assoc_times.
  51 rewrite < H3.rewrite > (plus_n_O (m*(n1 / m))).
  52 rewrite < H2.
  53 rewrite > sym_times.
  54 rewrite < div_mod.reflexivity.
  55 assumption.assumption.
  56 intros.simplify.apply plus_n_O.
  57 qed.
  58
  59 theorem p_ord_aux_to_exp: \forall p,n,m,q,r. O < m \to
  60   (pair nat nat q r) = p_ord_aux p n m \to n = m \sup q * r.
  61 intros.
  62 change with
  63 match (pair nat nat q r) with
  64   [ (pair q r) \Rightarrow n = m \sup q * r ].
  65 rewrite > H1.
  66 apply p_ord_aux_to_Prop.
  67 assumption.
  68 qed.
  69
  70 (* questo va spostato in primes1.ma *)
  71 theorem p_ord_exp: \forall n,m,i. O < m \to n \mod m \neq O \to
  72 \forall p. i \le p \to p_ord_aux p (m \sup i * n) m = pair nat nat i n.
  73 intros 5.
  74 elim i.
  75 simplify.
  76 rewrite < plus_n_O.
  77 apply (nat_case p).
  78 simplify.
  79 elim (n \mod m).simplify.reflexivity.simplify.reflexivity.
  80 intro.
  81 simplify.
  82 cut (O < n \mod m \lor O = n \mod m).
  83 elim Hcut.apply (lt_O_n_elim (n \mod m) H3).
  84 intros. simplify.reflexivity.
  85 apply False_ind.
  86 apply H1.apply sym_eq.assumption.
  87 apply le_to_or_lt_eq.apply le_O_n.
  88 generalize in match H3.
  89 apply (nat_case p).intro.apply False_ind.apply (not_le_Sn_O n1 H4).
  90 intros.
  91 simplify. fold simplify (m \sup (S n1)).
  92 cut (((m \sup (S n1)*n) \mod m) = O).
  93 rewrite > Hcut.
  94 simplify.fold simplify (m \sup (S n1)).
  95 cut ((m \sup (S n1) *n) / m = m \sup n1 *n).
  96 rewrite > Hcut1.
  97 rewrite > (H2 m1). simplify.reflexivity.
  98 apply le_S_S_to_le.assumption.
  99 (* div_exp *)
 100 simplify.
 101 rewrite > assoc_times.
 102 apply (lt_O_n_elim m H).
 103 intro.apply div_times.
 104 (* mod_exp = O *)
 105 apply divides_to_mod_O.
 106 assumption.
 107 simplify.rewrite > assoc_times.
 108 apply (witness ? ? (m \sup n1 *n)).reflexivity.
 109 qed.
 110
 111 theorem p_ord_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
 112   match p_ord_aux p n m with
 113   [ (pair q r) \Rightarrow r \mod m \neq O].
 114 intro.elim p.absurd (O < n).assumption.
 115 apply le_to_not_lt.assumption.
 116 simplify.
 117 apply (nat_case1 (n1 \mod m)).intro.
 118 generalize in match (H (n1 / m) m).
 119 elim (p_ord_aux n (n1 / m) m).
 120 apply H5.assumption.
 121 apply eq_mod_O_to_lt_O_div.
 122 apply (trans_lt ? (S O)).unfold lt.apply le_n.
 123 assumption.assumption.assumption.
 124 apply le_S_S_to_le.
 125 apply (trans_le ? n1).change with (n1 / m < n1).
 126 apply lt_div_n_m_n.assumption.assumption.assumption.
 127 intros.simplify.
 128 rewrite > H4.
 129 unfold Not.intro.
 130 apply (not_eq_O_S m1).
 131 rewrite > H5.reflexivity.
 132 qed.
 133
 134 theorem p_ord_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
 135  pair nat nat q r = p_ord_aux p n m \to r \mod m \neq O.
 136 intros.
 137 change with
 138   match (pair nat nat q r) with
 139   [ (pair q r) \Rightarrow r \mod m \neq O].
 140 rewrite > H3.
 141 apply p_ord_aux_to_Prop1.
 142 assumption.assumption.assumption.
 143 qed.
 144
 145 theorem p_ord_exp1: \forall p,n,q,r. O < p \to \lnot p \divides r \to
 146 n = p \sup q * r \to p_ord n p = pair nat nat q r.
 147 intros.unfold p_ord.
 148 rewrite > H2.
 149 apply p_ord_exp
 150  [assumption
 151  |unfold.intro.apply H1.
 152   apply mod_O_to_divides[assumption|assumption]
 153  |apply (trans_le ? (p \sup q)).
 154   cut ((S O) \lt p).
 155   elim q.simplify.apply le_n_Sn.
 156   simplify.
 157   generalize in match H3.
 158   apply (nat_case n1).simplify.
 159   rewrite < times_n_SO.intro.assumption.
 160   intros.
 161   apply (trans_le ? (p*(S m))).
 162   apply (trans_le ? ((S (S O))*(S m))).
 163   simplify.rewrite > plus_n_Sm.
 164   rewrite < plus_n_O.
 165   apply le_plus_n.
 166   apply le_times_l.
 167   assumption.
 168   apply le_times_r.assumption.
 169   apply not_eq_to_le_to_lt.
 170   unfold.intro.apply H1.
 171   rewrite < H3.
 172   apply (witness ? r r ?).simplify.apply plus_n_O.
 173   assumption.
 174   rewrite > times_n_SO in \vdash (? % ?).
 175   apply le_times_r.
 176   change with (O \lt r).
 177   apply not_eq_to_le_to_lt.
 178   unfold.intro.
 179   apply H1.rewrite < H3.
 180   apply (witness ? ? O ?).rewrite < times_n_O.reflexivity.
 181   apply le_O_n.
 182   ]
 183 qed.
 184
 185 theorem p_ord_to_exp1: \forall p,n,q,r. (S O) \lt p \to O \lt n \to p_ord n p = pair nat nat q r\to
 186 \lnot p \divides r \land n = p \sup q * r.
 187 intros.
 188 unfold p_ord in H2.
 189 split.unfold.intro.
 190 apply (p_ord_aux_to_not_mod_O n n p q r).assumption.assumption.
 191 apply le_n.symmetry.assumption.
 192 apply divides_to_mod_O.apply (trans_lt ? (S O)).
 193 unfold.apply le_n.assumption.assumption.
 194 apply (p_ord_aux_to_exp n).apply (trans_lt ? (S O)).
 195 unfold.apply le_n.assumption.symmetry.assumption.
 196 qed.
 197
 198 theorem p_ord_times: \forall p,a,b,qa,ra,qb,rb. prime p
 199 \to O \lt a \to O \lt b
 200 \to p_ord a p = pair nat nat qa ra
 201 \to p_ord b p = pair nat nat qb rb
 202 \to p_ord (a*b) p = pair nat nat (qa + qb) (ra*rb).
 203 intros.
 204 cut ((S O) \lt p).
 205 elim (p_ord_to_exp1 ? ? ? ? Hcut H1 H3).
 206 elim (p_ord_to_exp1 ? ? ? ? Hcut H2 H4).
 207 apply p_ord_exp1.
 208 apply (trans_lt ? (S O)).unfold.apply le_n.assumption.
 209 unfold.intro.
 210 elim (divides_times_to_divides ? ? ? H H9).
 211 apply (absurd ? ? H10 H5).
 212 apply (absurd ? ? H10 H7).
 213 (* rewrite > H6.
 214 rewrite > H8. *)
 215 autobatch paramodulation.
 216 unfold prime in H. elim H. assumption.
 217 qed.
 218
 219 theorem fst_p_ord_times: \forall p,a,b. prime p
 220 \to O \lt a \to O \lt b
 221 \to fst ? ? (p_ord (a*b) p) = (fst ? ? (p_ord a p)) + (fst ? ? (p_ord b p)).
 222 intros.
 223 rewrite > (p_ord_times p a b (fst ? ? (p_ord a p)) (snd ? ? (p_ord a p))
 224 (fst ? ? (p_ord b p)) (snd ? ? (p_ord b p)) H H1 H2).
 225 simplify.reflexivity.
 226 apply eq_pair_fst_snd.
 227 apply eq_pair_fst_snd.
 228 qed.
 229
 230 theorem p_ord_p : \forall p:nat. (S O) \lt p \to p_ord p p = pair ? ? (S O) (S O).
 231 intros.
 232 apply p_ord_exp1.
 233 apply (trans_lt ? (S O)). unfold.apply le_n.assumption.
 234 unfold.intro.
 235 apply (absurd ? ? H).
 236 apply le_to_not_lt.
 237 apply divides_to_le.unfold.apply le_n.assumption.
 238 rewrite < times_n_SO.
 239 apply exp_n_SO.
 240 qed.
 241
 242 (* p_ord and divides *)
 243 theorem divides_to_p_ord: \forall p,a,b,c,d,n,m:nat.
 244 O < n \to O < m \to prime p
 245 \to divides n m \to p_ord n p = pair ? ? a b \to
 246 p_ord m p = pair ? ? c d \to divides b d \land a \le c.
 247 intros.
 248 cut (S O < p)
 249   [lapply (p_ord_to_exp1 ? ? ? ? Hcut H H4).
 250    lapply (p_ord_to_exp1 ? ? ? ? Hcut H1 H5).
 251    elim Hletin. clear Hletin.
 252    elim Hletin1. clear Hletin1.
 253    rewrite > H9 in H3.
 254    split
 255     [apply (gcd_SO_to_divides_times_to_divides (exp p c))
 256       [elim (le_to_or_lt_eq ? ? (le_O_n b))
 257         [assumption
 258         |apply False_ind.
 259          apply (lt_to_not_eq O ? H).
 260          rewrite > H7.
 261          rewrite < H10.
 262          autobatch
 263         ]
 264       |elim c
 265         [rewrite > sym_gcd.
 266          apply gcd_SO_n
 267         |simplify.
 268          apply eq_gcd_times_SO
 269           [apply lt_to_le.assumption
 270           |apply lt_O_exp.apply lt_to_le.assumption
 271           |rewrite > sym_gcd.
 272            (* hint non trova prime_to_gcd_SO e
 273               autobatch non chiude il goal *)
 274            apply prime_to_gcd_SO
 275             [assumption|assumption]
 276           |assumption
 277           ]
 278         ]
 279       |apply (trans_divides ? n)
 280         [apply (witness ? ? (exp p a)).
 281          rewrite > sym_times.
 282          assumption
 283         |assumption
 284         ]
 285       ]
 286     |apply (le_exp_to_le p)
 287       [assumption
 288       |apply divides_to_le
 289         [apply lt_O_exp.apply lt_to_le.assumption
 290         |apply (gcd_SO_to_divides_times_to_divides d)
 291           [apply lt_O_exp.apply lt_to_le.assumption
 292           |elim a
 293             [apply gcd_SO_n
 294             |simplify.rewrite < sym_gcd.
 295              apply eq_gcd_times_SO
 296               [apply lt_to_le.assumption
 297               |apply lt_O_exp.apply lt_to_le.assumption
 298               |rewrite > sym_gcd.
 299               (* hint non trova prime_to_gcd_SO e
 300                  autobatch non chiude il goal *)
 301                apply prime_to_gcd_SO
 302                 [assumption|assumption]
 303               |rewrite > sym_gcd. assumption
 304               ]
 305             ]
 306           |apply (trans_divides ? n)
 307             [apply (witness ? ? b).assumption
 308             |rewrite > sym_times.assumption
 309             ]
 310           ]
 311         ]
 312       ]
 313     ]
 314   |elim H2.assumption
 315   ]
 316 qed.
 317
 318 (* p_ord and primes *)
 319 theorem not_divides_to_p_ord_O: \forall n,i.
 320 Not (divides (nth_prime i) n) \to p_ord n (nth_prime i) =
 321 pair nat nat O n.
 322 intros.
 323 apply p_ord_exp1
 324   [apply lt_O_nth_prime_n
 325   |assumption
 326   |autobatch
 327   ]
 328 qed.
 329
 330 theorem p_ord_O_to_not_divides: \forall n,i,r.
 331 O < n \to
 332 p_ord n (nth_prime i) = pair nat nat O r
 333 \to Not (divides (nth_prime i) n).
 334 intros.
 335 lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 336   [apply lt_SO_nth_prime_n
 337   |assumption
 338   |elim Hletin.
 339    simplify in H3.
 340    rewrite > H3.
 341    rewrite < plus_n_O.
 342    assumption
 343   ]
 344 qed.
 345
 346 theorem p_ord_to_not_eq_O : \forall n,p,q,r.
 347   (S O) < n \to
 348   p_ord n (nth_prime p) = pair nat nat q r \to
 349   Not (r=O).
 350 intros.
 351 unfold.intro.
 352 cut (O < n)
 353   [lapply (p_ord_to_exp1 ? ? ? ? ? ? H1)
 354     [apply lt_SO_nth_prime_n.
 355     |assumption
 356     |elim Hletin.
 357      apply (lt_to_not_eq ? ? Hcut).
 358      rewrite > H4.
 359      rewrite > H2.
 360      apply times_n_O
 361     ]
 362   |apply (trans_lt ? (S O))[apply lt_O_S|assumption]
 363   ]
 364 qed.
 365
 366 definition ord :nat \to nat \to nat \def
 367 \lambda n,p. fst ? ? (p_ord n p).
 368
 369 definition ord_rem :nat \to nat \to nat \def
 370 \lambda n,p. snd ? ? (p_ord n p).
 371
 372 theorem divides_to_ord: \forall p,n,m:nat.
 373 O < n \to O < m \to prime p
 374 \to divides n m
 375 \to divides (ord_rem n p) (ord_rem m p) \land (ord n p) \le (ord m p).
 376 intros.
 377 apply (divides_to_p_ord p ? ? ? ? n m H H1 H2 H3)
 378   [unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 379   |unfold ord.unfold ord_rem.apply eq_pair_fst_snd
 380   ]
 381 qed.
 382
 383 theorem divides_to_divides_ord_rem: \forall p,n,m:nat.
 384 O < n \to O < m \to prime p \to divides n m \to
 385 divides (ord_rem n p) (ord_rem m p).
 386 intros.
 387 elim (divides_to_ord p n m H H1 H2 H3).assumption.
 388 qed.
 389
 390 theorem divides_to_le_ord: \forall p,n,m:nat.
 391 O < n \to O < m \to prime p \to divides n m \to
 392 (ord n p) \le (ord m p).
 393 intros.
 394 elim (divides_to_ord p n m H H1 H2 H3).assumption.
 395 qed.
 396
 397 theorem exp_ord: \forall p,n. (S O) \lt p
 398 \to O \lt n \to n = p \sup (ord n p) * (ord_rem n p).
 399 intros.
 400 elim (p_ord_to_exp1 p n (ord n p) (ord_rem n p))
 401   [assumption
 402   |assumption
 403   |assumption
 404   |unfold ord.unfold ord_rem.
 405    apply eq_pair_fst_snd
 406   ]
 407 qed.
 408
 409 theorem divides_ord_rem: \forall p,n. (S O) < p \to O < n
 410 \to divides (ord_rem n p) n.
 411 intros.
 412 apply (witness ? ? (p \sup (ord n p))).
 413 rewrite > sym_times.
 414 apply exp_ord[assumption|assumption]
 415 qed.
 416
 417 theorem lt_O_ord_rem: \forall p,n. (S O) < p \to O < n \to O < ord_rem n p.
 418 intros.
 419 elim (le_to_or_lt_eq O (ord_rem n p))
 420   [assumption
 421   |apply False_ind.
 422    apply (lt_to_not_eq ? ? H1).
 423    lapply (divides_ord_rem ? ? H H1).
 424    rewrite < H2 in Hletin.
 425    elim Hletin.
 426    rewrite > H3.
 427    reflexivity
 428   |apply le_O_n
 429   ]
 430 qed.
 431
 432 (* p_ord_inv is the inverse of ord *)
 433 definition p_ord_inv \def
 434 \lambda p,m,x.
 435   match p_ord x p with
 436   [pair q r \Rightarrow r*m+q].
 437
 438 theorem  eq_p_ord_inv: \forall p,m,x.
 439 p_ord_inv p m x = (ord_rem x p)*m+(ord x p).
 440 intros.unfold p_ord_inv. unfold ord_rem.
 441 unfold ord.
 442 elim (p_ord x p).
 443 reflexivity.
 444 qed.
 445
 446 theorem div_p_ord_inv:
 447 \forall p,m,x. ord x p < m \to p_ord_inv p m x / m = ord_rem x p.
 448 intros.rewrite > eq_p_ord_inv.
 449 apply div_plus_times.
 450 assumption.
 451 qed.
 452
 453 theorem mod_p_ord_inv:
 454 \forall p,m,x. ord x p < m \to p_ord_inv p m x \mod m = ord x p.
 455 intros.rewrite > eq_p_ord_inv.
 456 apply mod_plus_times.
 457 assumption.
 458 qed.