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/z.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 symmetric_Ztimes : symmetric Z Ztimes.
  46 change with \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x).
  47 intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
  48 elim y.simplify.reflexivity.
  49 change with eq Z (pos (pred (times (S n) (S n1)))) (pos (pred (times (S n1) (S n)))).
  50 rewrite < sym_times.reflexivity.
  51 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
  52 rewrite < sym_times.reflexivity.
  53 elim y.simplify.reflexivity.
  54 change with eq Z (neg (pred (times (S n) (S n1)))) (neg (pred (times (S n1) (S n)))).
  55 rewrite < sym_times.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 qed.
  59
  60 variant sym_Ztimes : \forall x,y:Z. eq Z (Ztimes x y) (Ztimes y x)
  61 \def symmetric_Ztimes.
  62
  63 theorem associative_Ztimes: associative Z Ztimes.
  64 change with \forall x,y,z:Z.eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)).
  65 intros.
  66 elim x.simplify.reflexivity.
  67 elim y.simplify.reflexivity.
  68 elim z.simplify.reflexivity.
  69 change with
  70 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  71      (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  72 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  73 apply lt_O_times_S_S.
  74 apply lt_O_times_S_S.
  75 change with
  76 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  77      (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  78 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  79 apply lt_O_times_S_S.apply lt_O_times_S_S.
  80 elim z.simplify.reflexivity.
  81 change with
  82 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  83      (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  84 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  85 apply lt_O_times_S_S.apply lt_O_times_S_S.
  86 change with
  87 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  88      (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  89 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  90 apply lt_O_times_S_S.
  91 apply lt_O_times_S_S.
  92 elim y.simplify.reflexivity.
  93 elim z.simplify.reflexivity.
  94 change with
  95 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  96      (pos (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 change with
 101 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 102      (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 103 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 104 apply lt_O_times_S_S.apply lt_O_times_S_S.
 105 elim z.simplify.reflexivity.
 106 change with
 107 eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 108      (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 109 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 110 apply lt_O_times_S_S.apply lt_O_times_S_S.
 111 change with
 112 eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 113      (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 114 rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 115 apply lt_O_times_S_S.
 116 apply lt_O_times_S_S.
 117 qed.
 118
 119 variant assoc_Ztimes : \forall x,y,z:Z.
 120 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
 121 associative_Ztimes.
 122
 123
 124 theorem distributive_Ztimes: distributive Z Ztimes Zplus.
 125 change with \forall x,y,z:Z.
 126 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
 127 intros.elim x.
 128 simplify.reflexivity.
 129 (* case x = neg n *)
 130 elim y.reflexivity.
 131 elim z.reflexivity.
 132 change with
 133 eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
 134      (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
 135 rewrite < times_plus_distr.reflexivity.
 136 simplify. (* problemi di naming su n *)
 137 (* sintassi della change ??? *)
 138 cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
 139 rewrite > Hcut.
 140 rewrite > Hcut.
 141 rewrite < nat_compare_pred_pred ? ? ? ?.
 142 rewrite < nat_compare_times_l.
 143 rewrite < nat_compare_S_S.
 144 apply nat_compare_elim n1 n2.
 145 intro.
 146 (* per ricavare questo change ci ho messo un'ora;
 147 LA GESTIONE DELLA RIDUZIONE NON VA *)
 148 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
 149            (neg (pred (minus (pred (times (S n) (S n2)))
 150                              (pred (times (S n) (S n1))))))).
 151 rewrite < S_pred ? ?.
 152 rewrite > minus_pred_pred ? ? ? ?.
 153 rewrite < distr_times_minus.
 154 reflexivity.
 155 (* we start closing stupid positivity conditions *)
 156 apply lt_O_times_S_S.
 157 apply lt_O_times_S_S.
 158 simplify.
 159 apply le_SO_minus.  exact H.
 160 intro.rewrite < H.simplify.reflexivity.
 161 intro.
 162 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
 163            (pos (pred (minus (pred (times (S n) (S n1)))
 164                              (pred (times (S n) (S n2))))))).
 165 rewrite < S_pred ? ?.
 166 rewrite > minus_pred_pred ? ? ? ?.
 167 rewrite < distr_times_minus.
 168 reflexivity.
 169 (* we start closing stupid positivity conditions *)
 170 apply lt_O_times_S_S.
 171 apply lt_O_times_S_S.
 172 simplify.
 173 apply le_SO_minus.  exact H.
 174 (* questi non so neppure da dove vengano *)
 175 apply lt_O_times_S_S.
 176 apply lt_O_times_S_S.
 177 (* adesso chiudo il cut stupido *)
 178 intros.reflexivity.
 179 elim z.reflexivity.
 180 simplify.
 181 cut \forall n,m:nat.eq nat (plus m (times n (S m))) (pred (times (S n) (S m))).
 182 rewrite > Hcut.
 183 rewrite > Hcut.
 184 rewrite < nat_compare_pred_pred ? ? ? ?.
 185 rewrite < nat_compare_times_l.
 186 rewrite < nat_compare_S_S.
 187 apply nat_compare_elim n1 n2.
 188 intro.
 189 (* per ricavare questo change ci ho messo un'ora;
 190 LA GESTIONE DELLA RIDUZIONE NON VA *)
 191 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S n2) (S n1)))))))
 192            (pos (pred (minus (pred (times (S n) (S n2)))
 193                              (pred (times (S n) (S n1))))))).
 194 rewrite < S_pred ? ?.
 195 rewrite > minus_pred_pred ? ? ? ?.
 196 rewrite < distr_times_minus.
 197 reflexivity.
 198 (* we start closing stupid positivity conditions *)
 199 apply lt_O_times_S_S.
 200 apply lt_O_times_S_S.
 201 simplify.
 202 apply le_SO_minus.  exact H.
 203 intro.rewrite < H.simplify.reflexivity.
 204 intro.
 205 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S n1) (S n2)))))))
 206            (neg (pred (minus (pred (times (S n) (S n1)))
 207                              (pred (times (S n) (S n2))))))).
 208 rewrite < S_pred ? ?.
 209 rewrite > minus_pred_pred ? ? ? ?.
 210 rewrite < distr_times_minus.
 211 reflexivity.
 212 (* we start closing stupid positivity conditions *)
 213 apply lt_O_times_S_S.
 214 apply lt_O_times_S_S.
 215 simplify.
 216 apply le_SO_minus.  exact H.
 217 (* questi non so neppure da dove vengano *)
 218 apply lt_O_times_S_S.
 219 apply lt_O_times_S_S.
 220 (* adesso chiudo il cut stupido *)
 221 intros.reflexivity.
 222 change with
 223 eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
 224      (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
 225 rewrite < times_plus_distr.
 226 reflexivity.
 227 (* and now the case x = pos n *)