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