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