helm/matita/library/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/Z/times".
  16
  17 include "nat/lt_arith.ma".
  18 include "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 (times (S m) (S n))))
  28          | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
  29     | (neg m) \Rightarrow
  30         match y with
  31          [ OZ \Rightarrow OZ
  32          | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
  33          | (neg n) \Rightarrow (pos (pred (times (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/Z/times/Ztimes.con x y).
  37
  38 theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
  39 intro.elim z.
  40 simplify.reflexivity.
  41 simplify.reflexivity.
  42 simplify.reflexivity.
  43 qed.
  44
  45 theorem Ztimes_neg_Zopp: \forall n:nat.\forall x:Z.
  46 eq Z (Ztimes (neg n) x) (Zopp (Ztimes (pos n) x)).
  47 intros.elim x.
  48 simplify.reflexivity.
  49 simplify.reflexivity.
  50 simplify.reflexivity.
  51 qed.
  52 theorem symmetric_Ztimes : symmetric Z Ztimes.
  53 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
  54 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
  55 elim y.simplify.reflexivity.
  56 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
  57 rewrite < sym_times.reflexivity.
  58 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
  59 rewrite < sym_times.reflexivity.
  60 elim y.simplify.reflexivity.
  61 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
  62 rewrite < sym_times.reflexivity.
  63 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
  64 rewrite < sym_times.reflexivity.
  65 qed.
  66
  67 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
  68 \def symmetric_Ztimes.
  69
  70 theorem associative_Ztimes: associative Z Ztimes.
  71 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
  72 intros.elim x.
  73   simplify.reflexivity.
  74   elim y.
  75     simplify.reflexivity.
  76     elim z.
  77       simplify.reflexivity.
  78       change with
  79       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  80         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  81         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
  82          apply lt_O_times_S_S.apply lt_O_times_S_S.
  83       change with
  84       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  85         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  86         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
  87          apply lt_O_times_S_S.apply lt_O_times_S_S.
  88     elim z.
  89       simplify.reflexivity.
  90       change with
  91       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  92         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  93         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
  94          apply lt_O_times_S_S.apply lt_O_times_S_S.
  95       change with
  96       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  97         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  98         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
  99         apply lt_O_times_S_S.apply lt_O_times_S_S.
 100   elim y.
 101     simplify.reflexivity.
 102     elim z.
 103       simplify.reflexivity.
 104       change with
 105       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 106         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 107         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
 108          apply lt_O_times_S_S.apply lt_O_times_S_S.
 109       change with
 110       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 111         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 112         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
 113          apply lt_O_times_S_S.apply lt_O_times_S_S.
 114     elim z.
 115       simplify.reflexivity.
 116       change with
 117       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 118         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 119         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
 120          apply lt_O_times_S_S.apply lt_O_times_S_S.
 121       change with
 122       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 123         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 124         rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
 125          apply lt_O_times_S_S.apply lt_O_times_S_S.
 126 qed.
 127
 128 variant assoc_Ztimes : \forall x,y,z:Z.
 129 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
 130 associative_Ztimes.
 131
 132 lemma times_minus1: \forall n,p,q:nat. lt q p \to
 133 eq nat (times (S n) (S (pred (minus (S p) (S q)))))
 134        (minus (pred (times (S n) (S p)))
 135               (pred (times (S n) (S q)))).
 136 intros.
 137 rewrite < S_pred.
 138 rewrite > minus_pred_pred.
 139 rewrite < distr_times_minus.
 140 reflexivity.
 141 (* we now close all positivity conditions *)
 142 apply lt_O_times_S_S.
 143 apply lt_O_times_S_S.
 144 simplify.
 145 apply le_SO_minus.  exact H.
 146 qed.
 147
 148 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 149 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
 150 intros.
 151 simplify.
 152 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 153 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
 154 rewrite < nat_compare_pred_pred.
 155 rewrite < nat_compare_times_l.
 156 rewrite < nat_compare_S_S.
 157 apply nat_compare_elim p q.
 158 intro.
 159 (* uff *)
 160 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
 161            (pos (pred (minus (pred (times (S n) (S q)))
 162                              (pred (times (S n) (S p))))))).
 163 rewrite < times_minus1 n q p H.reflexivity.
 164 intro.rewrite < H.simplify.reflexivity.
 165 intro.
 166 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
 167            (neg (pred (minus (pred (times (S n) (S p)))
 168                              (pred (times (S n) (S q))))))).
 169 rewrite < times_minus1 n p q H.reflexivity.
 170 (* two more positivity conditions from nat_compare_pred_pred *)
 171 apply lt_O_times_S_S.
 172 apply lt_O_times_S_S.
 173 qed.
 174
 175 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
 176 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
 177 intros.
 178 rewrite < sym_Zplus.
 179 rewrite > Ztimes_Zplus_pos_neg_pos.
 180 apply sym_Zplus.
 181 qed.
 182
 183 lemma distributive2_Ztimes_pos_Zplus:
 184 distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
 185 change with \forall n,y,z.
 186 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
 187 intros.elim y.
 188   reflexivity.
 189   elim z.
 190     reflexivity.
 191     change with
 192     eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
 193       (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
 194       rewrite < distr_times_plus.reflexivity.
 195     apply Ztimes_Zplus_pos_pos_neg.
 196   elim z.
 197     reflexivity.
 198     apply Ztimes_Zplus_pos_neg_pos.
 199     change with
 200     eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
 201      (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
 202     rewrite < distr_times_plus.reflexivity.
 203 qed.
 204
 205 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
 206 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
 207 distributive2_Ztimes_pos_Zplus.
 208
 209 lemma distributive2_Ztimes_neg_Zplus :
 210 distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
 211 change with \forall n,y,z.
 212 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).
 213 intros.
 214 rewrite > Ztimes_neg_Zopp.
 215 rewrite > distr_Ztimes_Zplus_pos.
 216 rewrite > Zopp_Zplus.
 217 rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
 218 reflexivity.
 219 qed.
 220
 221 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
 222 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
 223 distributive2_Ztimes_neg_Zplus.
 224
 225 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
 226 change with \forall x,y,z:Z.
 227 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
 228 intros.elim x.
 229 (* case x = OZ *)
 230 simplify.reflexivity.
 231 (* case x = pos n *)
 232 apply distr_Ztimes_Zplus_pos.
 233 (* case x = neg n *)
 234 apply distr_Ztimes_Zplus_neg.
 235 qed.
 236
 237 variant distr_Ztimes_Zplus: \forall x,y,z.
 238 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
 239 distributive_Ztimes_Zplus.