helm/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.simplify.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.simplify.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.simplify.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.simplify.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 change with
 219 eqb ((cr_pair m n a b) \mod n) b = true
 220 \to a = a \land (cr_pair m n a b) \mod n = b.
 221 intro.split.reflexivity.
 222 apply eqb_true_to_eq.assumption.
 223 intro.
 224 change with false = true \to
 225 (cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b.
 226 intro.apply False_ind.
 227 apply not_eq_true_false.apply sym_eq.assumption.
 228 apply f_min_aux_true
 229 (\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n)).
 230 elim and_congruent_congruent_lt m n a b.
 231 apply ex_intro ? ? a1.split.split.
 232 rewrite < minus_n_n.apply le_O_n.
 233 elim H3.apply le_S_S_to_le.apply trans_le ? (m*n).
 234 assumption.apply nat_case (m*n).apply le_O_n.
 235 intro.
 236 rewrite < pred_Sn.apply le_n.
 237 elim H3.elim H4.
 238 apply andb_elim.
 239 cut a1 \mod m = a.
 240 cut a1 \mod n = b.
 241 rewrite > eq_to_eqb_true ? ? Hcut.
 242 rewrite > eq_to_eqb_true ? ? Hcut1.
 243 simplify.reflexivity.
 244 rewrite < lt_to_eq_mod b n.assumption.
 245 assumption.
 246 rewrite < lt_to_eq_mod a m.assumption.
 247 assumption.
 248 apply le_to_lt_to_lt ? b.apply le_O_n.assumption.
 249 apply le_to_lt_to_lt ? a.apply le_O_n.assumption.
 250 assumption.
 251 qed.