matita/library/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/nat/chinese_reminder".
  16
  17 include "nat/exp.ma".
  18 include "nat/gcd.ma".
  19 include "nat/permutation.ma".
  20 include "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.elim H3.elim H4.
  27 apply (ex_intro nat ? ((a+b*m)*a1*n-b*a2*m)).
  28 split.
  29 (* congruent to a *)
  30 cut (a1*n = a2*m + (S O)).
  31 rewrite > assoc_times.
  32 rewrite > Hcut1.
  33 rewrite < (sym_plus ? (a2*m)).
  34 rewrite > distr_times_plus.
  35 rewrite < times_n_SO.
  36 rewrite > assoc_plus.
  37 rewrite < assoc_times.
  38 rewrite < times_plus_l.
  39 rewrite > eq_minus_plus_plus_minus.
  40 rewrite < times_minus_l.
  41 rewrite > sym_plus.
  42 apply (eq_times_plus_to_congruent ? ? ? ((b+(a+b*m)*a2)-b*a2)).
  43 assumption.reflexivity.
  44 apply le_times_l.
  45 apply (trans_le ? ((a+b*m)*a2)).
  46 apply le_times_l.
  47 apply (trans_le ? (b*m)).
  48 rewrite > times_n_SO in \vdash (? % ?).
  49 apply le_times_r.assumption.
  50 apply le_plus_n.
  51 apply le_plus_n.
  52 apply minus_to_plus.
  53 apply lt_to_le.
  54 change with (O + a2*m < a1*n).
  55 apply lt_minus_to_plus.
  56 rewrite > H5.unfold lt.apply le_n.
  57 assumption.
  58 (* congruent to b *)
  59 cut (a2*m = a1*n - (S O)).
  60 rewrite > (assoc_times b a2).
  61 rewrite > Hcut1.
  62 rewrite > distr_times_minus.
  63 rewrite < assoc_times.
  64 rewrite < eq_plus_minus_minus_minus.
  65 rewrite < times_n_SO.
  66 rewrite < times_minus_l.
  67 rewrite < sym_plus.
  68 apply (eq_times_plus_to_congruent ? ? ? ((a+b*m)*a1-b*a1)).
  69 assumption.reflexivity.
  70 rewrite > assoc_times.
  71 apply le_times_r.
  72 apply (trans_le ? (a1*n - a2*m)).
  73 rewrite > H5.apply le_n.
  74 apply (le_minus_m ? (a2*m)).
  75 apply le_times_l.
  76 apply le_times_l.
  77 apply (trans_le ? (b*m)).
  78 rewrite > times_n_SO in \vdash (? % ?).
  79 apply le_times_r.assumption.
  80 apply le_plus_n.
  81 apply sym_eq. apply plus_to_minus.
  82 rewrite > sym_plus.
  83 apply minus_to_plus.
  84 apply lt_to_le.
  85 change with (O + a2*m < a1*n).
  86 apply lt_minus_to_plus.
  87 rewrite > H5.unfold lt.apply le_n.
  88 assumption.
  89 (* and now the symmetric case; the price to pay for working
  90    in nat instead than Z *)
  91 apply (ex_intro nat ? ((b+a*n)*a2*m-a*a1*n)).
  92 split.
  93 (* congruent to a *)
  94 cut (a1*n = a2*m - (S O)).
  95 rewrite > (assoc_times a a1).
  96 rewrite > Hcut1.
  97 rewrite > distr_times_minus.
  98 rewrite < assoc_times.
  99 rewrite < eq_plus_minus_minus_minus.
 100 rewrite < times_n_SO.
 101 rewrite < times_minus_l.
 102 rewrite < sym_plus.
 103 apply (eq_times_plus_to_congruent ? ? ? ((b+a*n)*a2-a*a2)).
 104 assumption.reflexivity.
 105 rewrite > assoc_times.
 106 apply le_times_r.
 107 apply (trans_le ? (a2*m - a1*n)).
 108 rewrite > H5.apply le_n.
 109 apply (le_minus_m ? (a1*n)).
 110 rewrite > assoc_times.rewrite > assoc_times.
 111 apply le_times_l.
 112 apply (trans_le ? (a*n)).
 113 rewrite > times_n_SO in \vdash (? % ?).
 114 apply le_times_r.assumption.
 115 apply le_plus_n.
 116 apply sym_eq.apply plus_to_minus.
 117 rewrite > sym_plus.
 118 apply minus_to_plus.
 119 apply lt_to_le.
 120 change with (O + a1*n < a2*m).
 121 apply lt_minus_to_plus.
 122 rewrite > H5.unfold lt.apply le_n.
 123 assumption.
 124 (* congruent to a *)
 125 cut (a2*m = a1*n + (S O)).
 126 rewrite > assoc_times.
 127 rewrite > Hcut1.
 128 rewrite > (sym_plus (a1*n)).
 129 rewrite > distr_times_plus.
 130 rewrite < times_n_SO.
 131 rewrite < assoc_times.
 132 rewrite > assoc_plus.
 133 rewrite < times_plus_l.
 134 rewrite > eq_minus_plus_plus_minus.
 135 rewrite < times_minus_l.
 136 rewrite > sym_plus.
 137 apply (eq_times_plus_to_congruent ? ? ? ((a+(b+a*n)*a1)-a*a1)).
 138 assumption.reflexivity.
 139 apply le_times_l.
 140 apply (trans_le ? ((b+a*n)*a1)).
 141 apply le_times_l.
 142 apply (trans_le ? (a*n)).
 143 rewrite > times_n_SO in \vdash (? % ?).
 144 apply le_times_r.
 145 assumption.
 146 apply le_plus_n.
 147 apply le_plus_n.
 148 apply minus_to_plus.
 149 apply lt_to_le.
 150 change with (O + a1*n < a2*m).
 151 apply lt_minus_to_plus.
 152 rewrite > H5.unfold lt.apply le_n.
 153 assumption.
 154 (* proof of the cut *)
 155 rewrite < H2.
 156 apply eq_minus_gcd.
 157 qed.
 158
 159 theorem and_congruent_congruent_lt: \forall m,n,a,b:nat. O < n \to O < m \to
 160 gcd n m = (S O) \to
 161 ex nat (\lambda x. (congruent x a m \land congruent x b n) \land
 162  (x < m*n)).
 163 intros.elim (and_congruent_congruent m n a b).
 164 elim H3.
 165 apply (ex_intro ? ? (a1 \mod (m*n))).
 166 split.split.
 167 apply (transitive_congruent m ? a1).
 168 unfold congruent.
 169 apply sym_eq.
 170 change with (congruent a1 (a1 \mod (m*n)) m).
 171 rewrite < sym_times.
 172 apply congruent_n_mod_times.
 173 assumption.assumption.assumption.
 174 apply (transitive_congruent n ? a1).
 175 unfold congruent.
 176 apply sym_eq.
 177 change with (congruent a1 (a1 \mod (m*n)) n).
 178 apply congruent_n_mod_times.
 179 assumption.assumption.assumption.
 180 apply lt_mod_m_m.
 181 rewrite > (times_n_O O).
 182 apply lt_times.assumption.assumption.
 183 assumption.assumption.assumption.
 184 qed.
 185
 186 definition cr_pair : nat \to nat \to nat \to nat \to nat \def
 187 \lambda n,m,a,b.
 188 min (pred (n*m)) (\lambda x. andb (eqb (x \mod n) a) (eqb (x \mod m) b)).
 189
 190 theorem cr_pair1: cr_pair (S (S O)) (S (S (S O))) O O = O.
 191 reflexivity.
 192 qed.
 193
 194 theorem cr_pair2: cr_pair (S(S O)) (S(S(S O))) (S O) O = (S(S(S O))).
 195 simplify.
 196 reflexivity.
 197 qed.
 198
 199 theorem cr_pair3: cr_pair (S(S O)) (S(S(S O))) (S O) (S(S O)) = (S(S(S(S(S O))))).
 200 reflexivity.
 201 qed.
 202
 203 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)) =
 204 (S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S O))))))))))))))))))))))).
 205 reflexivity.
 206 qed.
 207
 208 theorem mod_cr_pair : \forall m,n,a,b. a \lt m \to b \lt n \to
 209 gcd n m = (S O) \to
 210 (cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
 211 intros.
 212 cut (andb (eqb ((cr_pair m n a b) \mod m) a)
 213          (eqb ((cr_pair m n a b) \mod n) b) = true).
 214 generalize in match Hcut.
 215 apply andb_elim.
 216 apply eqb_elim.intro.
 217 rewrite > H3.
 218 simplify.
 219 intro.split.reflexivity.
 220 apply eqb_true_to_eq.assumption.
 221 intro.
 222 simplify.
 223 intro.apply False_ind.
 224 apply not_eq_true_false.apply sym_eq.assumption.
 225 apply (f_min_aux_true
 226 (\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) O).
 227 elim (and_congruent_congruent_lt m n a b).
 228 apply (ex_intro ? ? a1).split.split.
 229 apply le_O_n.
 230 elim H3.apply le_S_S_to_le.apply (trans_le ? (m*n)).
 231 assumption.apply (nat_case (m*n)).apply le_O_n.
 232 intro.
 233 rewrite < pred_Sn.
 234 rewrite < plus_n_O.apply le_n.
 235 elim H3.elim H4.
 236 apply andb_elim.
 237 cut (a1 \mod m = a).
 238 cut (a1 \mod n = b).
 239 rewrite > (eq_to_eqb_true ? ? Hcut).
 240 rewrite > (eq_to_eqb_true ? ? Hcut1).
 241 simplify.reflexivity.
 242 rewrite < (lt_to_eq_mod b n).assumption.
 243 assumption.
 244 rewrite < (lt_to_eq_mod a m).assumption.
 245 assumption.
 246 apply (le_to_lt_to_lt ? b).apply le_O_n.assumption.
 247 apply (le_to_lt_to_lt ? a).apply le_O_n.assumption.
 248 assumption.
 249 qed.