matita/library_auto/auto/nat/chinese_reminder.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 (*       \ /        This file 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/chinese_reminder".
  16
  17 include "auto/nat/exp.ma".
  18 include "auto/nat/gcd.ma".
  19 include "auto/nat/permutation.ma".
  20 include "auto/nat/congruence.ma".
  21
  22 theorem and_congruent_congruent: \forall m,n,a,b:nat. O < n \to O < m \to
  23 gcd n m = (S O) \to ex nat (\lambda x. congruent x a m \land congruent x b n).
  24 intros.
  25 cut (\exists c,d.c*n - d*m = (S O) \lor d*m - c*n = (S O))
  26 [ elim Hcut.
  27   elim H3.
  28   elim H4
  29   [
  30     apply (ex_intro nat ? ((a+b*m)*a1*n-b*a2*m)).
  31     split
  32     [ (* congruent to a *)
  33       cut (a1*n = a2*m + (S O))
  34       [ rewrite > assoc_times.
  35         rewrite > Hcut1.
  36         rewrite < (sym_plus ? (a2*m)).
  37         rewrite > distr_times_plus.
  38         rewrite < times_n_SO.
  39         rewrite > assoc_plus.
  40         rewrite < assoc_times.
  41         rewrite < times_plus_l.
  42         rewrite > eq_minus_plus_plus_minus
  43         [ auto
  44           (*rewrite < times_minus_l.
  45           rewrite > sym_plus.
  46           apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2))
  47           [ assumption
  48           | reflexivity
  49           ]*)
  50         | apply le_times_l.
  51           apply (trans_le ? ((a+b*m)*a2))
  52           [ apply le_times_l.
  53             apply (trans_le ? (b*m));auto
  54             (*[ rewrite > times_n_SO in \vdash (? % ?).
  55               apply le_times_r.
  56               assumption
  57             | apply le_plus_n
  58             ]*)
  59           | apply le_plus_n
  60           ]
  61         ]
  62       | apply minus_to_plus
  63         [ apply lt_to_le.
  64           change with (O + a2*m < a1*n).
  65           apply lt_minus_to_plus.
  66           auto
  67           (*rewrite > H5.
  68           unfold lt.
  69           apply le_n*)
  70         | assumption
  71         ]
  72       ]
  73     | (* congruent to b *)
  74       cut (a2*m = a1*n - (S O))
  75       [ rewrite > (assoc_times b a2).
  76         rewrite > Hcut1.
  77         rewrite > distr_times_minus.
  78         rewrite < assoc_times.
  79         rewrite < eq_plus_minus_minus_minus
  80         [ auto
  81           (*rewrite < times_n_SO.
  82           rewrite < times_minus_l.
  83           rewrite < sym_plus.
  84           apply (eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1))
  85           [ assumption
  86           | reflexivity
  87           ]*)
  88         | rewrite > assoc_times.
  89           apply le_times_r.
  90           (*auto genera un'esecuzione troppo lunga*)
  91           apply (trans_le ? (a1*n - a2*m));auto
  92           (*[ rewrite > H5.
  93             apply le_n
  94           | apply (le_minus_m ? (a2*m))
  95           ]*)
  96         | apply le_times_l.
  97           apply le_times_l.
  98           auto
  99           (*apply (trans_le ? (b*m))
 100           [ rewrite > times_n_SO in \vdash (? % ?).
 101             apply le_times_r.
 102             assumption
 103           | apply le_plus_n
 104           ]*)
 105         ]
 106       | apply sym_eq.
 107         apply plus_to_minus.
 108         rewrite > sym_plus.
 109         apply minus_to_plus
 110         [ apply lt_to_le.
 111           change with (O + a2*m < a1*n).
 112           apply lt_minus_to_plus.
 113           auto
 114           (*rewrite > H5.
 115           unfold lt.
 116           apply le_n*)
 117         | assumption
 118         ]
 119       ]
 120     ]
 121  | (* and now the symmetric case; the price to pay for working
 122    in nat instead than Z *)
 123     apply (ex_intro nat ? ((b+a*n)*a2*m-a*a1*n)).
 124     split
 125     [(* congruent to a *)
 126       cut (a1*n = a2*m - (S O))
 127       [ rewrite > (assoc_times a a1).
 128         rewrite > Hcut1.
 129         rewrite > distr_times_minus.
 130         rewrite < assoc_times.
 131         rewrite < eq_plus_minus_minus_minus
 132         [ auto
 133           (*rewrite < times_n_SO.
 134           rewrite < times_minus_l.
 135           rewrite < sym_plus.
 136           apply (eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2))
 137           [ assumption
 138           | reflexivity
 139           ]*)
 140         | rewrite > assoc_times.
 141           apply le_times_r.
 142           apply (trans_le ? (a2*m - a1*n));auto
 143           (*[ rewrite > H5.
 144             apply le_n
 145           | apply (le_minus_m ? (a1*n))
 146           ]*)
 147         | rewrite > assoc_times.
 148           rewrite > assoc_times.
 149           apply le_times_l.
 150           auto
 151           (*apply (trans_le ? (a*n))
 152           [ rewrite > times_n_SO in \vdash (? % ?).
 153             apply le_times_r.
 154             assumption.
 155           | apply le_plus_n.
 156           ]*)
 157         ]
 158       | apply sym_eq.
 159         apply plus_to_minus.
 160         rewrite > sym_plus.
 161         apply minus_to_plus
 162         [ apply lt_to_le.
 163           change with (O + a1*n < a2*m).
 164           apply lt_minus_to_plus.
 165           auto
 166           (*rewrite > H5.
 167           unfold lt.
 168           apply le_n*)
 169         | assumption
 170         ]
 171       ]
 172     | (* congruent to b *)
 173       cut (a2*m = a1*n + (S O))
 174       [ rewrite > assoc_times.
 175         rewrite > Hcut1.
 176         rewrite > (sym_plus (a1*n)).
 177         rewrite > distr_times_plus.
 178         rewrite < times_n_SO.
 179         rewrite < assoc_times.
 180         rewrite > assoc_plus.
 181         rewrite < times_plus_l.
 182         rewrite > eq_minus_plus_plus_minus
 183         [ auto
 184           (*rewrite < times_minus_l.
 185           rewrite > sym_plus.
 186           apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1))
 187           [ assumption
 188           | reflexivity
 189           ]*)
 190         | apply le_times_l.
 191           apply (trans_le ? ((b+a*n)*a1))
 192           [ apply le_times_l.
 193             auto
 194             (*apply (trans_le ? (a*n))
 195             [ rewrite > times_n_SO in \vdash (? % ?).
 196               apply le_times_r.
 197               assumption
 198             | apply le_plus_n
 199             ]*)
 200           | apply le_plus_n
 201           ]
 202         ]
 203       | apply minus_to_plus
 204         [ apply lt_to_le.
 205           change with (O + a1*n < a2*m).
 206           apply lt_minus_to_plus.
 207           auto
 208           (*rewrite > H5.
 209           unfold lt.
 210           apply le_n*)
 211         | assumption
 212         ]
 213       ]
 214     ]
 215   ]
 216 (* proof of the cut *)
 217 | (* qui auto non conclude il goal *)
 218   rewrite < H2.
 219   apply eq_minus_gcd
 220 ]
 221 qed.
 222
 223 theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to
 224 gcd n m = (S O) \to
 225 ex nat (\lambda x. (congruent x a m \land congruent x b n) \land
 226  (x < m*n)).
 227 intros.
 228 elim (and_congruent_congruent m n a b)
 229 [ elim H3.
 230   apply (ex_intro ? ? (a1 \mod (m*n))).
 231   split
 232   [ split
 233     [ apply (transitive_congruent m ? a1)
 234       [ unfold congruent.
 235         apply sym_eq.
 236         change with (congruent a1 (a1 \mod (m*n)) m).
 237         rewrite < sym_times.
 238         auto
 239         (*apply congruent_n_mod_times;assumption*)
 240       | assumption
 241       ]
 242     | apply (transitive_congruent n ? a1)
 243       [ unfold congruent.
 244         apply sym_eq.
 245         change with (congruent a1 (a1 \mod (m*n)) n).
 246         auto
 247         (*apply congruent_n_mod_times;assumption*)
 248       | assumption
 249       ]
 250     ]
 251   | apply lt_mod_m_m.
 252     auto
 253     (*rewrite > (times_n_O O).
 254     apply lt_times;assumption*)
 255   ]
 256 | assumption
 257 | assumption
 258 | assumption
 259 ]
 260 qed.
 261
 262 definition cr_pair : nat \to nat \to nat \to nat \to nat \def
 263 \lambda n,m,a,b.
 264 min (pred (n*m)) (\lambda x. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
 265
 266 theorem cr_pair1: cr_pair (S (S O)) (S (S (S O))) O O = O.
 267 reflexivity.
 268 qed.
 269
 270 theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))).
 271 auto.
 272 (*simplify.
 273 reflexivity.*)
 274 qed.
 275
 276 theorem cr_pair3: cr_pair (S(S O)) (S(S(S O))) (S O) (S(S O)) = (S(S(S(S(S O))))).
 277 reflexivity.
 278 qed.
 279
 280 theorem cr_pair4: cr_pair (S(S(S(S(S O))))) (S(S(S(S(S(S(S O))))))) (S(S(S O))) (S(S O)) =
 281 (S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S O))))))))))))))))))))))).
 282 reflexivity.
 283 qed.
 284
 285 theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to
 286 gcd n m = (S O) \to
 287 (cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
 288 intros.
 289 cut (andb (eqb ((cr_pair m n a b) \mod m) a)
 290          (eqb ((cr_pair m n a b) \mod n) b) = true)
 291 [ generalize in match Hcut.
 292   apply andb_elim.
 293   apply eqb_elim;intro
 294   [ rewrite > H3.
 295     simplify.
 296     intro.
 297     auto
 298     (*split
 299     [ reflexivity
 300     | apply eqb_true_to_eq.
 301       assumption
 302     ]*)
 303   | simplify.
 304     intro.
 305     (* l'invocazione di auto qui genera segmentation fault *)
 306     apply False_ind.
 307     (* l'invocazione di auto qui genera segmentation fault *)
 308     apply not_eq_true_false.
 309     (* l'invocazione di auto qui genera segmentation fault *)
 310     apply sym_eq.
 311     assumption
 312   ]
 313 | apply (f_min_aux_true
 314   (\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n))).
 315   elim (and_congruent_congruent_lt m n a b)
 316   [ apply (ex_intro ? ? a1).
 317     split
 318     [ split
 319       [ auto
 320         (*rewrite < minus_n_n.
 321         apply le_O_n*)
 322       | elim H3.
 323         apply le_S_S_to_le.
 324         apply (trans_le ? (m*n))
 325         [ assumption
 326         | apply (nat_case (m*n))
 327           [ apply le_O_n
 328           | intro.
 329             auto
 330             (*rewrite < pred_Sn.
 331             apply le_n*)
 332           ]
 333         ]
 334       ]
 335     | elim H3.
 336       elim H4.
 337       apply andb_elim.
 338       cut (a1 \mod m = a)
 339       [ cut (a1 \mod n = b)
 340         [ rewrite > (eq_to_eqb_true ? ? Hcut).
 341           rewrite > (eq_to_eqb_true ? ? Hcut1).
 342           (* l'invocazione di auto qui non chiude il goal *)
 343           simplify.
 344           reflexivity
 345         | rewrite < (lt_to_eq_mod b n);
 346           assumption
 347         ]
 348       | rewrite < (lt_to_eq_mod a m);assumption
 349       ]
 350     ]
 351   | auto
 352     (*apply (le_to_lt_to_lt ? b)
 353     [ apply le_O_n
 354     | assumption
 355     ]*)
 356   | auto
 357     (*apply (le_to_lt_to_lt ? a)
 358     [ apply le_O_n
 359     | assumption
 360     ]*)
 361   | assumption
 362   ]
 363 ]
 364 qed.