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