matita/contribs/library_auto/auto/nat/congruence.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_autobatch/nat/congruence".
  16
  17 include "auto/nat/relevant_equations.ma".
  18 include "auto/nat/primes.ma".
  19
  20 definition S_mod: nat \to nat \to nat \def
  21 \lambda n,m:nat. (S m) \mod n.
  22
  23 definition congruent: nat \to nat \to nat \to Prop \def
  24 \lambda n,m,p:nat. mod n p = mod m p.
  25
  26 interpretation "congruent" 'congruent n m p =
  27   (cic:/matita/library_autobatch/nat/congruence/congruent.con n m p).
  28
  29 notation < "hvbox(n break \cong\sub p m)"
  30   (*non associative*) with precedence 45
  31 for @{ 'congruent $n $m $p }.
  32
  33 theorem congruent_n_n: \forall n,p:nat.congruent n n p.
  34 intros.
  35 unfold congruent.
  36 reflexivity.
  37 qed.
  38
  39 theorem transitive_congruent: \forall p:nat. transitive nat
  40 (\lambda n,m. congruent n m p).
  41 intros.unfold transitive.
  42 unfold congruent.
  43 intros.
  44 whd.
  45 apply (trans_eq ? ? (y \mod p))
  46 [ (*qui autobatch non chiude il goal*)
  47   apply H
  48 | (*qui autobatch non chiude il goal*)
  49   apply H1
  50 ]
  51 qed.
  52
  53 theorem le_to_mod: \forall n,m:nat. n \lt m \to n = n \mod m.
  54 intros.
  55 autobatch.
  56 (*apply (div_mod_spec_to_eq2 n m O n (n/m) (n \mod m))
  57 [ constructor 1
  58   [ assumption
  59   | simplify.
  60     reflexivity
  61   ]
  62 | apply div_mod_spec_div_mod.
  63   apply (le_to_lt_to_lt O n m)
  64   [ apply le_O_n
  65   | assumption
  66   ]
  67 ]*)
  68 qed.
  69
  70 theorem mod_mod : \forall n,p:nat. O<p \to n \mod p = (n \mod p) \mod p.
  71 intros.
  72 autobatch.
  73 (*rewrite > (div_mod (n \mod p) p) in \vdash (? ? % ?)
  74 [ rewrite > (eq_div_O ? p)
  75   [ reflexivity
  76   | apply lt_mod_m_m.
  77     assumption
  78   ]
  79 | assumption
  80 ]*)
  81 qed.
  82
  83 theorem mod_times_mod : \forall n,m,p:nat. O<p \to O<m \to n \mod p = (n \mod (m*p)) \mod p.
  84 intros.
  85 apply (div_mod_spec_to_eq2 n p (n/p) (n \mod p)
  86 (n/(m*p)*m + (n \mod (m*p)/p)))
  87 [ autobatch.
  88   (*apply div_mod_spec_div_mod.
  89   assumption*)
  90 | constructor 1
  91   [ autobatch
  92     (*apply lt_mod_m_m.
  93     assumption*)
  94   | rewrite > times_plus_l.
  95     rewrite > assoc_plus.
  96     rewrite < div_mod
  97     [ rewrite > assoc_times.
  98       rewrite < div_mod;autobatch
  99       (*[ reflexivity
 100       | rewrite > (times_n_O O).
 101         apply lt_times;assumption
 102       ]*)
 103     | assumption
 104     ]
 105   ]
 106 ]
 107 qed.
 108
 109 theorem congruent_n_mod_n :
 110 \forall n,p:nat. O < p \to congruent n (n \mod p) p.
 111 intros.
 112 unfold congruent.
 113 autobatch.
 114 (*apply mod_mod.
 115 assumption.*)
 116 qed.
 117
 118 theorem congruent_n_mod_times :
 119 \forall n,m,p:nat. O < p \to O < m \to congruent n (n \mod (m*p)) p.
 120 intros.unfold congruent.
 121 apply mod_times_mod;assumption.
 122 qed.
 123
 124 theorem eq_times_plus_to_congruent: \forall n,m,p,r:nat. O< p \to
 125 n = r*p+m \to congruent n m p.
 126 intros.
 127 unfold congruent.
 128 apply (div_mod_spec_to_eq2 n p (div n p) (mod n p) (r +(div m p)) (mod m p))
 129 [ autobatch
 130   (*apply div_mod_spec_div_mod.
 131   assumption*)
 132 | constructor 1
 133   [ autobatch
 134     (*apply lt_mod_m_m.
 135     assumption*)
 136   |
 137 (*cut (n = r * p + (m / p * p + m \mod p)).*)
 138 (*lapply (div_mod m p H).
 139 rewrite > sym_times.
 140 rewrite > distr_times_plus.
 141 (*rewrite > (sym_times p (m/p)).*)
 142 (*rewrite > sym_times.*)
 143   rewrite > assoc_plus.
 144   autobatch paramodulation.
 145   rewrite < div_mod.
 146   assumption.
 147   assumption.
 148 *)
 149     rewrite > sym_times.
 150     rewrite > distr_times_plus.
 151     rewrite > sym_times.
 152     rewrite > (sym_times p).
 153     rewrite > assoc_plus.
 154     rewrite < div_mod;assumption.
 155   ]
 156 ]
 157 qed.
 158
 159 theorem divides_to_congruent: \forall n,m,p:nat. O < p \to m \le n \to
 160 divides p (n - m) \to congruent n m p.
 161 intros.
 162 elim H2.
 163 apply (eq_times_plus_to_congruent n m p n2)
 164 [ assumption
 165 | rewrite < sym_plus.
 166   apply minus_to_plus;autobatch
 167   (*[ assumption
 168   | rewrite > sym_times. assumption
 169   ]*)
 170 ]
 171 qed.
 172
 173 theorem congruent_to_divides: \forall n,m,p:nat.
 174 O < p \to congruent n m p \to divides p (n - m).
 175 intros.
 176 unfold congruent in H1.
 177 apply (witness ? ? ((n / p)-(m / p))).
 178 rewrite > sym_times.
 179 rewrite > (div_mod n p) in \vdash (? ? % ?)
 180 [ rewrite > (div_mod m p) in \vdash (? ? % ?)
 181   [ rewrite < (sym_plus (m \mod p)).
 182     autobatch
 183     (*rewrite < H1.
 184     rewrite < (eq_minus_minus_minus_plus ? (n \mod p)).
 185     rewrite < minus_plus_m_m.
 186     apply sym_eq.
 187     apply times_minus_l*)
 188   | assumption
 189   ]
 190 | assumption
 191 ]
 192 qed.
 193
 194 theorem mod_times: \forall n,m,p:nat.
 195 O < p \to mod (n*m) p = mod ((mod n p)*(mod m p)) p.
 196 intros.
 197 change with (congruent (n*m) ((mod n p)*(mod m p)) p).
 198 apply (eq_times_plus_to_congruent ? ? p
 199 ((n / p)*p*(m / p) + (n / p)*(m \mod p) + (n \mod p)*(m / p)))
 200 [ assumption
 201 | apply (trans_eq ? ? (((n/p)*p+(n \mod p))*((m/p)*p+(m \mod p))))
 202   [ apply eq_f2;autobatch(*;apply div_mod.assumption.*)
 203   | apply (trans_eq ? ? (((n/p)*p)*((m/p)*p) + (n/p)*p*(m \mod p) +
 204     (n \mod p)*((m / p)*p) + (n \mod p)*(m \mod p)))
 205     [ apply times_plus_plus
 206     | apply eq_f2
 207       [ rewrite < assoc_times.
 208         autobatch
 209         (*rewrite > (assoc_times (n/p) p (m \mod p)).
 210         rewrite > (sym_times p (m \mod p)).
 211         rewrite < (assoc_times (n/p) (m \mod p) p).
 212         rewrite < times_plus_l.
 213         rewrite < (assoc_times (n \mod p)).
 214         rewrite < times_plus_l.
 215         apply eq_f2
 216         [ apply eq_f2
 217           [ reflexivity
 218           | reflexivity
 219           ]
 220         | reflexivity
 221         ]*)
 222       | reflexivity
 223       ]
 224     ]
 225   ]
 226 ]
 227 qed.
 228
 229 theorem congruent_times: \forall n,m,n1,m1,p. O < p \to congruent n n1 p \to
 230 congruent m m1 p \to congruent (n*m) (n1*m1) p.
 231 unfold congruent.
 232 intros.
 233 rewrite > (mod_times n m p H).
 234 rewrite > H1.
 235 rewrite > H2.
 236 autobatch.
 237 (*
 238 apply sym_eq.
 239 apply mod_times.
 240 assumption.*)
 241 qed.
 242
 243 theorem congruent_pi: \forall f:nat \to nat. \forall n,m,p:nat.O < p \to
 244 congruent (pi n f m) (pi n (\lambda m. mod (f m) p) m) p.
 245 intros.
 246 elim n;simplify
 247 [ autobatch
 248   (*apply congruent_n_mod_n.
 249   assumption*)
 250 | apply congruent_times
 251   [ assumption
 252   | autobatch
 253     (*apply congruent_n_mod_n.
 254     assumption*)
 255   | (*NB: QUI AUTO NON RIESCE A CHIUDERE IL GOAL*)
 256     assumption
 257   ]
 258 ]
 259 qed.