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