matita/contribs/library_auto/auto/Z/times.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/library_autobatch/Z/times".
  16
  17 include "auto/nat/lt_arith.ma".
  18 include "auto/Z/plus.ma".
  19
  20 definition Ztimes :Z \to Z \to Z \def
  21 \lambda x,y.
  22   match x with
  23     [ OZ \Rightarrow OZ
  24     | (pos m) \Rightarrow
  25         match y with
  26          [ OZ \Rightarrow OZ
  27          | (pos n) \Rightarrow (pos (pred ((S m) * (S n))))
  28          | (neg n) \Rightarrow (neg (pred ((S m) * (S n))))]
  29     | (neg m) \Rightarrow
  30         match y with
  31          [ OZ \Rightarrow OZ
  32          | (pos n) \Rightarrow (neg (pred ((S m) * (S n))))
  33          | (neg n) \Rightarrow (pos (pred ((S m) * (S n))))]].
  34
  35 (*CSC: the URI must disappear: there is a bug now *)
  36 interpretation "integer times" 'times x y = (cic:/matita/library_autobatch/Z/times/Ztimes.con x y).
  37
  38 theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
  39 intro.
  40 elim z;autobatch.
  41   (*simplify;reflexivity.*)
  42 qed.
  43
  44 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
  45 neg n * x = - (pos n * x).
  46 intros.
  47 elim x;autobatch.
  48   (*simplify;reflexivity.*)
  49 qed.
  50
  51 theorem symmetric_Ztimes : symmetric Z Ztimes.
  52 change with (\forall x,y:Z. x*y = y*x).
  53 intros.
  54 elim x
  55 [ autobatch
  56   (*rewrite > Ztimes_z_OZ.
  57   reflexivity*)
  58 | elim y
  59   [ autobatch
  60     (*simplify.
  61     reflexivity*)
  62   | change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
  63     autobatch
  64     (*rewrite < sym_times.
  65     reflexivity*)
  66   | change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
  67     autobatch
  68     (*rewrite < sym_times.
  69     reflexivity*)
  70   ]
  71 | elim y
  72   [ autobatch
  73     (*simplify.
  74     reflexivity*)
  75   | change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
  76     autobatch
  77     (*rewrite < sym_times.
  78     reflexivity*)
  79   | change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
  80     autobatch
  81     (*rewrite < sym_times.
  82     reflexivity*)
  83   ]
  84 ]
  85 qed.
  86
  87 variant sym_Ztimes : \forall x,y:Z. x*y = y*x
  88 \def symmetric_Ztimes.
  89
  90 theorem associative_Ztimes: associative Z Ztimes.
  91 unfold associative.
  92 intros.
  93 elim x
  94 [ autobatch
  95   (*simplify.
  96   reflexivity*)
  97 | elim y
  98   [ autobatch
  99     (*simplify.
 100     reflexivity*)
 101   | elim z
 102     [ autobatch
 103       (*simplify.
 104       reflexivity*)
 105     | change with
 106        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 107        pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 108       rewrite < S_pred
 109       [ rewrite < S_pred;autobatch
 110         (*[ rewrite < assoc_times.
 111           reflexivity
 112         | apply lt_O_times_S_S
 113         ]*)
 114       | apply lt_O_times_S_S
 115       ]
 116     | change with
 117        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 118        neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 119       rewrite < S_pred
 120       [ rewrite < S_pred;autobatch
 121         (*[ rewrite < assoc_times.
 122           reflexivity
 123         | apply lt_O_times_S_S
 124         ]*)
 125       | apply lt_O_times_S_S
 126       ]
 127     ]
 128   | elim z
 129     [ autobatch
 130       (*simplify.
 131       reflexivity*)
 132     | change with
 133        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 134        neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 135       rewrite < S_pred
 136       [ rewrite < S_pred;autobatch
 137         (*[ rewrite < assoc_times.
 138           reflexivity
 139         | apply lt_O_times_S_S
 140         ]*)
 141       | apply lt_O_times_S_S
 142       ]
 143     | change with
 144        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 145        pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 146       rewrite < S_pred
 147       [ rewrite < S_pred;autobatch
 148         (*[ rewrite < assoc_times.
 149           reflexivity
 150         | apply lt_O_times_S_S
 151         ]*)
 152       | apply lt_O_times_S_S
 153       ]
 154     ]
 155   ]
 156 | elim y
 157   [ autobatch
 158     (*simplify.
 159     reflexivity*)
 160   | elim z
 161     [ autobatch
 162       (*simplify.
 163       reflexivity*)
 164     | change with
 165        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 166        neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 167       rewrite < S_pred
 168       [ rewrite < S_pred;autobatch
 169         (*[ rewrite < assoc_times.
 170           reflexivity
 171         | apply lt_O_times_S_S
 172         ]*)
 173       | apply lt_O_times_S_S
 174       ]
 175     | change with
 176        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 177        pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 178       rewrite < S_pred
 179       [ rewrite < S_pred;autobatch
 180         (*[ rewrite < assoc_times.
 181           reflexivity
 182         | apply lt_O_times_S_S
 183         ]*)
 184       | apply lt_O_times_S_S
 185       ]
 186     ]
 187   | elim z
 188     [ autobatch
 189       (*simplify.
 190       reflexivity*)
 191     | change with
 192        (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 193        pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 194       rewrite < S_pred
 195       [ rewrite < S_pred;autobatch
 196         (*[ rewrite < assoc_times.
 197           reflexivity
 198         | apply lt_O_times_S_S
 199         ]*)
 200       | apply lt_O_times_S_S
 201       ]
 202     | change with
 203        (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
 204        neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
 205       rewrite < S_pred
 206       [ rewrite < S_pred;autobatch
 207         (*[ rewrite < assoc_times.
 208           reflexivity
 209         | apply lt_O_times_S_S
 210         ]*)
 211       | apply lt_O_times_S_S
 212       ]
 213     ]
 214   ]
 215 ]
 216 qed.
 217
 218 variant assoc_Ztimes : \forall x,y,z:Z.
 219 (x * y) * z = x * (y * z) \def
 220 associative_Ztimes.
 221
 222 lemma times_minus1: \forall n,p,q:nat. lt q p \to
 223 (S n) * (S (pred ((S p) - (S q)))) =
 224 pred ((S n) * (S p)) - pred ((S n) * (S q)).
 225 intros.
 226 rewrite < S_pred
 227 [ rewrite > minus_pred_pred
 228   [ autobatch
 229     (*rewrite < distr_times_minus.
 230     reflexivity*)
 231
 232     (* we now close all positivity conditions *)
 233   | apply lt_O_times_S_S
 234   | apply lt_O_times_S_S
 235   ]
 236 | unfold lt.autobatch
 237   (*simplify.
 238   unfold lt.
 239   apply le_SO_minus.
 240   exact H*)
 241 ]
 242 qed.
 243
 244 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 245 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
 246 intros.
 247 simplify.
 248 change in match (p + n * (S p)) with (pred ((S n) * (S p))).
 249 change in match (q + n * (S q)) with (pred ((S n) * (S q))).
 250 rewrite < nat_compare_pred_pred
 251 [ rewrite < nat_compare_times_l.
 252   rewrite < nat_compare_S_S.
 253   apply (nat_compare_elim p q)
 254   [ intro.
 255     (* uff *)
 256     change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
 257             pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
 258     rewrite < (times_minus1 n q p H).
 259     reflexivity
 260   | intro.
 261     autobatch
 262     (*rewrite < H.
 263     simplify.
 264     reflexivity*)
 265   | intro.
 266     change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
 267             neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))).
 268     rewrite < (times_minus1 n p q H).
 269     reflexivity
 270   ]
 271   (* two more positivity conditions from nat_compare_pred_pred *)
 272
 273 | apply lt_O_times_S_S
 274 | apply lt_O_times_S_S
 275 ]
 276 qed.
 277
 278 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
 279 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
 280 intros.
 281 autobatch.
 282 (*rewrite < sym_Zplus.
 283 rewrite > Ztimes_Zplus_pos_neg_pos.
 284 apply sym_Zplus.*)
 285 qed.
 286
 287 lemma distributive2_Ztimes_pos_Zplus:
 288 distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
 289 change with (\forall n,y,z.
 290 (pos n) * (y + z) = (pos n) * y + (pos n) * z).
 291 intros.
 292 elim y
 293 [ reflexivity
 294 | elim z
 295   [ reflexivity
 296   | change with
 297      (pos (pred ((S n) * ((S n1) + (S n2)))) =
 298      pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
 299     autobatch
 300     (*rewrite < distr_times_plus.
 301     reflexivity*)
 302   | apply Ztimes_Zplus_pos_pos_neg
 303   ]
 304 | elim z
 305   [ reflexivity
 306   | apply Ztimes_Zplus_pos_neg_pos
 307   | change with
 308      (neg (pred ((S n) * ((S n1) + (S n2)))) =
 309      neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
 310     autobatch
 311     (*rewrite < distr_times_plus.
 312     reflexivity*)
 313   ]
 314 ]
 315 qed.
 316
 317 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
 318 (pos n) * (y + z) = ((pos n) * y + (pos n) * z) \def
 319 distributive2_Ztimes_pos_Zplus.
 320
 321 lemma distributive2_Ztimes_neg_Zplus :
 322 distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
 323 change with (\forall n,y,z.
 324 (neg n) * (y + z) = (neg n) * y + (neg n) * z).
 325 intros.
 326 rewrite > Ztimes_neg_Zopp.
 327 rewrite > distr_Ztimes_Zplus_pos.
 328 autobatch.
 329 (*rewrite > Zopp_Zplus.
 330 rewrite < Ztimes_neg_Zopp.
 331 rewrite < Ztimes_neg_Zopp.
 332 reflexivity.*)
 333 qed.
 334
 335 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
 336 (neg n) * (y + z) = (neg n) * y + (neg n) * z \def
 337 distributive2_Ztimes_neg_Zplus.
 338
 339 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
 340 change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
 341 intros.
 342 elim x;autobatch.
 343 (*[ simplify.
 344   reflexivity
 345 | apply distr_Ztimes_Zplus_pos
 346 | apply distr_Ztimes_Zplus_neg
 347 ]*)
 348 qed.
 349
 350 variant distr_Ztimes_Zplus: \forall x,y,z.
 351 x * (y + z) = x*y + x*z \def
 352 distributive_Ztimes_Zplus.