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