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