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