matita/library_auto/auto/nat/div_and_mod.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_auto/nat/div_and_mod".
  16
  17 include "datatypes/constructors.ma".
  18 include "auto/nat/minus.ma".
  19
  20 let rec mod_aux p m n: nat \def
  21 match (leb m n) with
  22 [ true \Rightarrow m
  23 | false \Rightarrow
  24   match p with
  25   [O \Rightarrow m
  26   |(S q) \Rightarrow mod_aux q (m-(S n)) n]].
  27
  28 definition mod : nat \to nat \to nat \def
  29 \lambda n,m.
  30 match m with
  31 [O \Rightarrow m
  32 | (S p) \Rightarrow mod_aux n n p].
  33
  34 interpretation "natural remainder" 'module x y =
  35   (cic:/matita/library_auto/nat/div_and_mod/mod.con x y).
  36
  37 let rec div_aux p m n : nat \def
  38 match (leb m n) with
  39 [ true \Rightarrow O
  40 | false \Rightarrow
  41   match p with
  42   [O \Rightarrow O
  43   |(S q) \Rightarrow S (div_aux q (m-(S n)) n)]].
  44
  45 definition div : nat \to nat \to nat \def
  46 \lambda n,m.
  47 match m with
  48 [O \Rightarrow S n
  49 | (S p) \Rightarrow div_aux n n p].
  50
  51 interpretation "natural divide" 'divide x y =
  52   (cic:/matita/library_auto/nat/div_and_mod/div.con x y).
  53
  54 theorem le_mod_aux_m_m:
  55 \forall p,n,m. n \leq p \to (mod_aux p n m) \leq m.
  56 intro.
  57 elim p
  58 [ apply (le_n_O_elim n H (\lambda n.(mod_aux O n m) \leq m)).
  59   auto
  60   (*simplify.
  61   apply le_O_n*)
  62 | simplify.
  63   apply (leb_elim n1 m);simplify;intro
  64   [ assumption
  65   | apply H.
  66     cut (n1 \leq (S n) \to n1-(S m) \leq n)
  67     [ auto
  68       (*apply Hcut.
  69       assumption*)
  70     | elim n1;simplify;auto
  71       (*[ apply le_O_n.
  72       | apply (trans_le ? n2 n)
  73         [ apply le_minus_m
  74         | apply le_S_S_to_le.
  75           assumption
  76         ]
  77       ]*)
  78     ]
  79   ]
  80 ]
  81 qed.
  82
  83 theorem lt_mod_m_m: \forall n,m. O < m \to (n \mod m) < m.
  84 intros 2.
  85 elim m
  86 [ apply False_ind.
  87   apply (not_le_Sn_O O H)
  88 | simplify.
  89   auto
  90   (*unfold lt.
  91   apply le_S_S.
  92   apply le_mod_aux_m_m.
  93   apply le_n*)
  94 ]
  95 qed.
  96
  97 theorem div_aux_mod_aux: \forall p,n,m:nat.
  98 (n=(div_aux p n m)*(S m) + (mod_aux p n m)).
  99 intro.
 100 elim p;simplify
 101 [ elim (leb n m);auto
 102     (*simplify;apply refl_eq.*)
 103 | apply (leb_elim n1 m);simplify;intro
 104   [ apply refl_eq
 105   | rewrite > assoc_plus.
 106     elim (H (n1-(S m)) m).
 107     change with (n1=(S m)+(n1-(S m))).
 108     rewrite < sym_plus.
 109     auto
 110     (*apply plus_minus_m_m.
 111     change with (m < n1).
 112     apply not_le_to_lt.
 113     exact H1*)
 114   ]
 115 ]
 116 qed.
 117
 118 theorem div_mod: \forall n,m:nat. O < m \to n=(n / m)*m+(n \mod m).
 119 intros 2.
 120 elim m
 121 [ elim (not_le_Sn_O O H)
 122 | simplify.
 123   apply div_aux_mod_aux
 124 ]
 125 qed.
 126
 127 inductive div_mod_spec (n,m,q,r:nat) : Prop \def
 128 div_mod_spec_intro: r < m \to n=q*m+r \to (div_mod_spec n m q r).
 129
 130 (*
 131 definition div_mod_spec : nat \to nat \to nat \to nat \to Prop \def
 132 \lambda n,m,q,r:nat.r < m \land n=q*m+r).
 133 *)
 134
 135 theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
 136 intros 4.
 137 unfold Not.
 138 intros.
 139 elim H.
 140 absurd (le (S r) O);auto.
 141 (*[ rewrite < H1.
 142   assumption
 143 | exact (not_le_Sn_O r).
 144 ]*)
 145 qed.
 146
 147 theorem div_mod_spec_div_mod:
 148 \forall n,m. O < m \to (div_mod_spec n m (n / m) (n \mod m)).
 149 intros.
 150 auto.
 151 (*apply div_mod_spec_intro
 152 [ apply lt_mod_m_m.
 153   assumption
 154 | apply div_mod.
 155   assumption
 156 ]*)
 157 qed.
 158
 159 theorem div_mod_spec_to_eq :\forall a,b,q,r,q1,r1.
 160 (div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
 161 (eq nat q q1).
 162 intros.
 163 elim H.
 164 elim H1.
 165 apply (nat_compare_elim q q1)
 166 [ intro.
 167   apply False_ind.
 168   cut (eq nat ((q1-q)*b+r1) r)
 169   [ cut (b \leq (q1-q)*b+r1)
 170     [ cut (b \leq r)
 171       [ apply (lt_to_not_le r b H2 Hcut2)
 172       | elim Hcut.
 173         assumption
 174       ]
 175     | apply (trans_le ? ((q1-q)*b));auto
 176       (*[ apply le_times_n.
 177         apply le_SO_minus.
 178         exact H6
 179       | rewrite < sym_plus.
 180         apply le_plus_n
 181       ]*)
 182     ]
 183   | rewrite < sym_times.
 184     rewrite > distr_times_minus.
 185     rewrite > plus_minus;auto
 186     (*[ rewrite > sym_times.
 187       rewrite < H5.
 188       rewrite < sym_times.
 189       apply plus_to_minus.
 190       apply H3
 191     | apply le_times_r.
 192       apply lt_to_le.
 193       apply H6
 194     ]*)
 195   ]
 196 | (* eq case *)
 197   auto
 198   (*intros.
 199   assumption*)
 200 | (* the following case is symmetric *)
 201   intro.
 202   apply False_ind.
 203   cut (eq nat ((q-q1)*b+r) r1)
 204   [ cut (b \leq (q-q1)*b+r)
 205     [ cut (b \leq r1)
 206       [ apply (lt_to_not_le r1 b H4 Hcut2)
 207       | elim Hcut.
 208         assumption
 209       ]
 210     | apply (trans_le ? ((q-q1)*b));auto
 211       (*[ apply le_times_n.
 212         apply le_SO_minus.
 213         exact H6
 214       | rewrite < sym_plus.
 215         apply le_plus_n
 216       ]*)
 217     ]
 218   | rewrite < sym_times.
 219     rewrite > distr_times_minus.
 220     rewrite > plus_minus;auto
 221     (*[ rewrite > sym_times.
 222       rewrite < H3.
 223       rewrite < sym_times.
 224       apply plus_to_minus.
 225       apply H5
 226     | apply le_times_r.
 227       apply lt_to_le.
 228       apply H6
 229     ]*)
 230   ]
 231 ]
 232 qed.
 233
 234 theorem div_mod_spec_to_eq2 :\forall a,b,q,r,q1,r1.
 235 (div_mod_spec a b q r) \to (div_mod_spec a b q1 r1) \to
 236 (eq nat r r1).
 237 intros.
 238 elim H.
 239 elim H1.
 240 apply (inj_plus_r (q*b)).
 241 rewrite < H3.
 242 rewrite > (div_mod_spec_to_eq a b q r q1 r1 H H1).
 243 assumption.
 244 qed.
 245
 246 theorem div_mod_spec_times : \forall n,m:nat.div_mod_spec ((S n)*m) (S n) m O.
 247 intros.
 248 auto.
 249 (*constructor 1
 250 [ unfold lt.
 251   apply le_S_S.
 252   apply le_O_n
 253 | rewrite < plus_n_O.
 254   rewrite < sym_times.
 255   reflexivity
 256 ]*)
 257 qed.
 258
 259
 260 (*il corpo del seguente teorema non e' stato strutturato *)
 261 (* some properties of div and mod *)
 262 theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m.
 263 intros.
 264 apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O);
 265 [2: apply div_mod_spec_div_mod.auto.
 266 | skip
 267 | auto
 268 ]
 269 (*unfold lt.apply le_S_S.apply le_O_n.
 270 apply div_mod_spec_times.*)
 271 qed.
 272
 273 theorem div_n_n: \forall n:nat. O < n \to n / n = S O.
 274 intros.
 275 apply (div_mod_spec_to_eq n n (n / n) (n \mod n) (S O) O);auto.
 276 (*[ apply div_mod_spec_div_mod.
 277   assumption
 278 | constructor 1
 279   [ assumption
 280   | rewrite < plus_n_O.
 281     simplify.
 282     rewrite < plus_n_O.
 283     reflexivity
 284   ]
 285 ] *)
 286 qed.
 287
 288 theorem eq_div_O: \forall n,m. n < m \to n / m = O.
 289 intros.
 290 apply (div_mod_spec_to_eq n m (n/m) (n \mod m) O n);auto.
 291 (*[ apply div_mod_spec_div_mod.
 292   apply (le_to_lt_to_lt O n m)
 293   [ apply le_O_n
 294   | assumption
 295   ]
 296 | constructor 1
 297   [ assumption
 298   | reflexivity
 299   ]
 300 ]*)
 301 qed.
 302
 303 theorem mod_n_n: \forall n:nat. O < n \to n \mod n = O.
 304 intros.
 305 apply (div_mod_spec_to_eq2 n n (n / n) (n \mod n) (S O) O);auto.
 306 (*[ apply div_mod_spec_div_mod.
 307   assumption
 308 | constructor 1
 309   [ assumption.
 310   | rewrite < plus_n_O.
 311     simplify.
 312     rewrite < plus_n_O.
 313     reflexivity
 314   ]
 315 ]*)
 316 qed.
 317
 318 theorem mod_S: \forall n,m:nat. O < m \to S (n \mod m) < m \to
 319 ((S n) \mod m) = S (n \mod m).
 320 intros.
 321 apply (div_mod_spec_to_eq2 (S n) m ((S n) / m) ((S n) \mod m) (n / m) (S (n \mod m)))
 322 [ auto
 323   (*apply div_mod_spec_div_mod.
 324   assumption*)
 325 | constructor 1
 326   [ assumption
 327   | rewrite < plus_n_Sm.
 328     auto
 329     (*apply eq_f.
 330     apply div_mod.
 331     assumption*)
 332   ]
 333 ]
 334 qed.
 335
 336 theorem mod_O_n: \forall n:nat.O \mod n = O.
 337 intro.
 338 elim n;auto.
 339   (*simplify;reflexivity*)
 340
 341 qed.
 342
 343 theorem lt_to_eq_mod:\forall n,m:nat. n < m \to n \mod m = n.
 344 intros.
 345 apply (div_mod_spec_to_eq2 n m (n/m) (n \mod m) O n);auto.
 346 (*[ apply div_mod_spec_div_mod.
 347   apply (le_to_lt_to_lt O n m)
 348   [ apply le_O_n
 349   | assumption
 350   ]
 351 | constructor 1.
 352   [ assumption
 353   | reflexivity
 354   ]
 355 ]*)
 356 qed.
 357
 358 (* injectivity *)
 359 theorem injective_times_r: \forall n:nat.injective nat nat (\lambda m:nat.(S n)*m).
 360 change with (\forall n,p,q:nat.(S n)*p = (S n)*q \to p=q).
 361 intros.
 362 rewrite < (div_times n).
 363 auto.
 364 (*rewrite < (div_times n q).
 365 apply eq_f2
 366 [ assumption
 367 | reflexivity
 368 ]*)
 369 qed.
 370
 371 variant inj_times_r : \forall n,p,q:nat.(S n)*p = (S n)*q \to p=q \def
 372 injective_times_r.
 373
 374 theorem lt_O_to_injective_times_r: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.n*m).
 375 simplify.
 376 intros 4.
 377 apply (lt_O_n_elim n H).
 378 intros.
 379 auto.
 380 (*apply (inj_times_r m).
 381 assumption.*)
 382 qed.
 383
 384 variant inj_times_r1:\forall n. O < n \to \forall p,q:nat.n*p = n*q \to p=q
 385 \def lt_O_to_injective_times_r.
 386
 387 theorem injective_times_l: \forall n:nat.injective nat nat (\lambda m:nat.m*(S n)).
 388 simplify.
 389 intros.
 390 auto.
 391 (*apply (inj_times_r n x y).
 392 rewrite < sym_times.
 393 rewrite < (sym_times y).
 394 assumption.*)
 395 qed.
 396
 397 variant inj_times_l : \forall n,p,q:nat. p*(S n) = q*(S n) \to p=q \def
 398 injective_times_l.
 399
 400 theorem lt_O_to_injective_times_l: \forall n:nat. O < n \to injective nat nat (\lambda m:nat.m*n).
 401 simplify.
 402 intros 4.
 403 apply (lt_O_n_elim n H).
 404 intros.
 405 auto.
 406 (*apply (inj_times_l m).
 407 assumption.*)
 408 qed.
 409
 410 variant inj_times_l1:\forall n. O < n \to \forall p,q:nat.p*n = q*n \to p=q
 411 \def lt_O_to_injective_times_l.
 412
 413 (* n_divides computes the pair (div,mod) *)
 414
 415 (* p is just an upper bound, acc is an accumulator *)
 416 let rec n_divides_aux p n m acc \def
 417   match n \mod m with
 418   [ O \Rightarrow
 419     match p with
 420       [ O \Rightarrow pair nat nat acc n
 421       | (S p) \Rightarrow n_divides_aux p (n / m) m (S acc)]
 422   | (S a) \Rightarrow pair nat nat acc n].
 423
 424 (* n_divides n m = <q,r> if m divides n q times, with remainder r *)
 425 definition n_divides \def \lambda n,m:nat.n_divides_aux n n m O.