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 "Z/z.ma".
  18
  19 definition Ztimes :Z \to Z \to Z \def
  20 \lambda x,y.
  21   match x with
  22     [ OZ \Rightarrow OZ
  23     | (pos m) \Rightarrow
  24         match y with
  25          [ OZ \Rightarrow OZ
  26          | (pos n) \Rightarrow (pos (pred (times (S m) (S n))))
  27          | (neg n) \Rightarrow (neg (pred (times (S m) (S n))))]
  28     | (neg m) \Rightarrow
  29         match y with
  30          [ OZ \Rightarrow OZ
  31          | (pos n) \Rightarrow (neg (pred (times (S m) (S n))))
  32          | (neg n) \Rightarrow (pos (pred (times (S m) (S n))))]].
  33
  34 (*CSC: the URI must disappear: there is a bug now *)
  35 interpretation "integer times" 'times x y = (cic:/matita/Z/times/Ztimes.con x y).
  36
  37 theorem Ztimes_z_OZ:  \forall z:Z. z*OZ = OZ.
  38 intro.elim z.
  39 simplify.reflexivity.
  40 simplify.reflexivity.
  41 simplify.reflexivity.
  42 qed.
  43
  44 (*CSC: da qui in avanti niente notazione *)
  45 (*
  46 theorem symmetric_Ztimes : symmetric Z Ztimes.
  47 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
  48 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
  49 elim y.simplify.reflexivity.
  50 change with eq Z (pos (pred (times (S e1) (S e)))) (pos (pred (times (S e) (S e1)))).
  51 rewrite < sym_times.reflexivity.
  52 change with eq Z (neg (pred (times (S e1) (S e2)))) (neg (pred (times (S e2) (S e1)))).
  53 rewrite < sym_times.reflexivity.
  54 elim y.simplify.reflexivity.
  55 change with eq Z (neg (pred (times (S e2) (S e1)))) (neg (pred (times (S e1) (S e2)))).
  56 rewrite < sym_times.reflexivity.
  57 change with eq Z (pos (pred (times (S e2) (S e)))) (pos (pred (times (S e) (S e2)))).
  58 rewrite < sym_times.reflexivity.
  59 qed.
  60
  61 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
  62 \def symmetric_Ztimes.
  63
  64 theorem associative_Ztimes: associative Z Ztimes.
  65 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
  66 intros.
  67 elim x.simplify.reflexivity.
  68 elim y.simplify.reflexivity.
  69 elim z.simplify.reflexivity.
  70 change with
  71 eq Z (neg (pred (times (S (pred (times (S e1) (S e)))) (S e2))))
  72      (neg (pred (times (S e1) (S (pred (times (S e) (S e2))))))).
  73 rewrite < S_pred_S.
  74
  75 theorem Zpred_Zplus_neg_O : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
  76 intros.elim z.
  77 simplify.reflexivity.
  78 simplify.reflexivity.
  79 elim e2.simplify.reflexivity.
  80 simplify.reflexivity.
  81 qed.
  82
  83 theorem Zsucc_Zplus_pos_O : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
  84 intros.elim z.
  85 simplify.reflexivity.
  86 elim e1.simplify.reflexivity.
  87 simplify.reflexivity.
  88 simplify.reflexivity.
  89 qed.
  90
  91 theorem Zplus_pos_pos:
  92 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
  93 intros.
  94 elim n.elim m.
  95 simplify.reflexivity.
  96 simplify.reflexivity.
  97 elim m.
  98 simplify.
  99 rewrite < plus_n_O.reflexivity.
 100 simplify.
 101 rewrite < plus_n_Sm.reflexivity.
 102 qed.
 103
 104 theorem Zplus_pos_neg:
 105 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
 106 intros.reflexivity.
 107 qed.
 108
 109 theorem Zplus_neg_pos :
 110 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
 111 intros.
 112 elim n.elim m.
 113 simplify.reflexivity.
 114 simplify.reflexivity.
 115 elim m.
 116 simplify.reflexivity.
 117 simplify.reflexivity.
 118 qed.
 119
 120 theorem Zplus_neg_neg:
 121 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
 122 intros.
 123 elim n.elim m.
 124 simplify.reflexivity.
 125 simplify.reflexivity.
 126 elim m.
 127 simplify.rewrite < plus_n_Sm.reflexivity.
 128 simplify.rewrite > plus_n_Sm.reflexivity.
 129 qed.
 130
 131 theorem Zplus_Zsucc_Zpred:
 132 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
 133 intros.
 134 elim x. elim y.
 135 simplify.reflexivity.
 136 simplify.reflexivity.
 137 rewrite < Zsucc_Zplus_pos_O.
 138 rewrite > Zsucc_Zpred.reflexivity.
 139 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
 140 rewrite < Zpred_Zplus_neg_O.
 141 rewrite > Zpred_Zsucc.
 142 simplify.reflexivity.
 143 rewrite < Zplus_neg_neg.reflexivity.
 144 apply Zplus_neg_pos.
 145 elim y.simplify.reflexivity.
 146 apply Zplus_pos_neg.
 147 apply Zplus_pos_pos.
 148 qed.
 149
 150 theorem Zplus_Zsucc_pos_pos :
 151 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 152 intros.reflexivity.
 153 qed.
 154
 155 theorem Zplus_Zsucc_pos_neg:
 156 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 157 intros.
 158 apply nat_elim2
 159 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 160 intros.elim n1.
 161 simplify. reflexivity.
 162 elim e1.simplify. reflexivity.
 163 simplify. reflexivity.
 164 intros. elim n1.
 165 simplify. reflexivity.
 166 simplify.reflexivity.
 167 intros.
 168 rewrite < (Zplus_pos_neg ? m1).
 169 elim H.reflexivity.
 170 qed.
 171
 172 theorem Zplus_Zsucc_neg_neg :
 173 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 174 intros.
 175 apply nat_elim2
 176 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 177 intros.elim n1.
 178 simplify. reflexivity.
 179 elim e1.simplify. reflexivity.
 180 simplify. reflexivity.
 181 intros. elim n1.
 182 simplify. reflexivity.
 183 simplify.reflexivity.
 184 intros.
 185 rewrite < (Zplus_neg_neg ? m1).
 186 reflexivity.
 187 qed.
 188
 189 theorem Zplus_Zsucc_neg_pos:
 190 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 191 intros.
 192 apply nat_elim2
 193 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 194 intros.elim n1.
 195 simplify. reflexivity.
 196 elim e1.simplify. reflexivity.
 197 simplify. reflexivity.
 198 intros. elim n1.
 199 simplify. reflexivity.
 200 simplify.reflexivity.
 201 intros.
 202 rewrite < H.
 203 rewrite < (Zplus_neg_pos ? (S m1)).
 204 reflexivity.
 205 qed.
 206
 207 theorem Zplus_Zsucc : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
 208 intros.elim x.elim y.
 209 simplify. reflexivity.
 210 rewrite < Zsucc_Zplus_pos_O.reflexivity.
 211 simplify.reflexivity.
 212 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
 213 apply Zplus_Zsucc_neg_neg.
 214 apply Zplus_Zsucc_neg_pos.
 215 elim y.
 216 rewrite < sym_Zplus OZ.reflexivity.
 217 apply Zplus_Zsucc_pos_neg.
 218 apply Zplus_Zsucc_pos_pos.
 219 qed.
 220
 221 theorem Zplus_Zpred: \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 222 intros.
 223 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
 224 rewrite > Hcut.
 225 rewrite > Zplus_Zsucc.
 226 rewrite > Zpred_Zsucc.
 227 reflexivity.
 228 rewrite > Zsucc_Zpred.
 229 reflexivity.
 230 qed.
 231
 232
 233 theorem associative_Zplus: associative Z Zplus.
 234 change with \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z)).
 235
 236 intros.elim x.simplify.reflexivity.
 237 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
 238 rewrite < (Zpred_Zplus_neg_O y).
 239 rewrite < Zplus_Zpred.
 240 reflexivity.
 241 rewrite > Zplus_Zpred (neg e).
 242 rewrite > Zplus_Zpred (neg e).
 243 rewrite > Zplus_Zpred (Zplus (neg e) y).
 244 apply eq_f.assumption.
 245 elim e2.rewrite < Zsucc_Zplus_pos_O.
 246 rewrite < Zsucc_Zplus_pos_O.
 247 rewrite > Zplus_Zsucc.
 248 reflexivity.
 249 rewrite > Zplus_Zsucc (pos e1).
 250 rewrite > Zplus_Zsucc (pos e1).
 251 rewrite > Zplus_Zsucc (Zplus (pos e1) y).
 252 apply eq_f.assumption.
 253 qed.
 254
 255 variant assoc_Zplus : \forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
 256 \def associative_Zplus.
 257 *)