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.elim x.
  74   simplify.reflexivity.
  75   elim y.
  76     simplify.reflexivity.
  77     elim z.
  78       simplify.reflexivity.
  79       change with
  80       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  81         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  82         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  83          apply lt_O_times_S_S.apply lt_O_times_S_S.
  84       change with
  85       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  86         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  87         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  88          apply lt_O_times_S_S.apply lt_O_times_S_S.
  89     elim z.
  90       simplify.reflexivity.
  91       change with
  92       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  93         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  94         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
  95          apply lt_O_times_S_S.apply lt_O_times_S_S.
  96       change with
  97       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
  98         (pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
  99         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 100         apply lt_O_times_S_S.apply lt_O_times_S_S.
 101   elim y.
 102     simplify.reflexivity.
 103     elim z.
 104       simplify.reflexivity.
 105       change with
 106       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 107         (neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 108         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 109          apply lt_O_times_S_S.apply lt_O_times_S_S.
 110       change with
 111       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 112         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 113         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 114          apply lt_O_times_S_S.apply lt_O_times_S_S.
 115     elim z.
 116       simplify.reflexivity.
 117       change with
 118       eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 119         (pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 120         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 121          apply lt_O_times_S_S.apply lt_O_times_S_S.
 122       change with
 123       eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
 124         (neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
 125         rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
 126          apply lt_O_times_S_S.apply lt_O_times_S_S.
 127 qed.
 128
 129 variant assoc_Ztimes : \forall x,y,z:Z.
 130 eq Z (Ztimes (Ztimes x y) z) (Ztimes x (Ztimes y z)) \def
 131 associative_Ztimes.
 132
 133 lemma times_minus1: \forall n,p,q:nat. lt q p \to
 134 eq nat (times (S n) (S (pred (minus (S p) (S q)))))
 135        (minus (pred (times (S n) (S p)))
 136               (pred (times (S n) (S q)))).
 137 intros.
 138 rewrite < S_pred ? ?.
 139 rewrite > minus_pred_pred ? ? ? ?.
 140 rewrite < distr_times_minus.
 141 reflexivity.
 142 (* we now close all positivity conditions *)
 143 apply lt_O_times_S_S.
 144 apply lt_O_times_S_S.
 145 simplify.
 146 apply le_SO_minus.  exact H.
 147 qed.
 148
 149 lemma Ztimes_Zplus_pos_neg_pos: \forall n,p,q:nat.
 150 (pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
 151 intros.
 152 simplify.
 153 change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
 154 change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
 155 rewrite < nat_compare_pred_pred ? ? ? ?.
 156 rewrite < nat_compare_times_l.
 157 rewrite < nat_compare_S_S.
 158 apply nat_compare_elim p q.
 159 intro.
 160 (* uff *)
 161 change with (eq Z (pos (pred (times (S n) (S (pred (minus (S q) (S p)))))))
 162            (pos (pred (minus (pred (times (S n) (S q)))
 163                              (pred (times (S n) (S p))))))).
 164 rewrite < times_minus1 n q p H.reflexivity.
 165 intro.rewrite < H.simplify.reflexivity.
 166 intro.
 167 change with (eq Z (neg (pred (times (S n) (S (pred (minus (S p) (S q)))))))
 168            (neg (pred (minus (pred (times (S n) (S p)))
 169                              (pred (times (S n) (S q))))))).
 170 rewrite < times_minus1 n p q H.reflexivity.
 171 (* two more positivity conditions from nat_compare_pred_pred *)
 172 apply lt_O_times_S_S.
 173 apply lt_O_times_S_S.
 174 qed.
 175
 176 lemma Ztimes_Zplus_pos_pos_neg: \forall n,p,q:nat.
 177 (pos n)*((pos p)+(neg q)) = (pos n)*(pos p)+ (pos n)*(neg q).
 178 intros.
 179 rewrite < sym_Zplus.
 180 rewrite > Ztimes_Zplus_pos_neg_pos.
 181 apply sym_Zplus.
 182 qed.
 183
 184 lemma distributive2_Ztimes_pos_Zplus:
 185 distributive2 nat Z (\lambda n,z. Ztimes (pos n) z) Zplus.
 186 change with \forall n,y,z.
 187 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)).
 188 intros.elim y.
 189   reflexivity.
 190   elim z.
 191     reflexivity.
 192     change with
 193     eq Z (pos (pred (times (S n) (plus (S n1) (S n2)))))
 194       (pos (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
 195       rewrite < distr_times_plus.reflexivity.
 196     apply Ztimes_Zplus_pos_pos_neg.
 197   elim z.
 198     reflexivity.
 199     apply Ztimes_Zplus_pos_neg_pos.
 200     change with
 201     eq Z (neg (pred (times (S n) (plus (S n1) (S n2)))))
 202      (neg (pred (plus (times (S n) (S n1))(times (S n) (S n2))))).
 203     rewrite < distr_times_plus.reflexivity.
 204 qed.
 205
 206 variant distr_Ztimes_Zplus_pos: \forall n,y,z.
 207 eq Z (Ztimes (pos n) (Zplus y z)) (Zplus (Ztimes (pos n) y) (Ztimes (pos n) z)) \def
 208 distributive2_Ztimes_pos_Zplus.
 209
 210 lemma distributive2_Ztimes_neg_Zplus :
 211 distributive2 nat Z (\lambda n,z. Ztimes (neg n) z) Zplus.
 212 change with \forall n,y,z.
 213 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)).
 214 intros.
 215 rewrite > Ztimes_neg_Zopp.
 216 rewrite > distr_Ztimes_Zplus_pos.
 217 rewrite > Zopp_Zplus.
 218 rewrite < Ztimes_neg_Zopp. rewrite < Ztimes_neg_Zopp.
 219 reflexivity.
 220 qed.
 221
 222 variant distr_Ztimes_Zplus_neg: \forall n,y,z.
 223 eq Z (Ztimes (neg n) (Zplus y z)) (Zplus (Ztimes (neg n) y) (Ztimes (neg n) z)) \def
 224 distributive2_Ztimes_neg_Zplus.
 225
 226 theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
 227 change with \forall x,y,z:Z.
 228 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)).
 229 intros.elim x.
 230 (* case x = OZ *)
 231 simplify.reflexivity.
 232 (* case x = pos n *)
 233 apply distr_Ztimes_Zplus_pos.
 234 (* case x = neg n *)
 235 apply distr_Ztimes_Zplus_neg.
 236 qed.
 237
 238 variant distr_Ztimes_Zplus: \forall x,y,z.
 239 eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
 240 distributive_Ztimes_Zplus.