helm/matita/library/Z.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/".
  16
  17 include "nat.ma".
  18
  19 inductive Z : Set \def
  20   OZ : Z
  21 | pos : nat \to Z
  22 | neg : nat \to Z.
  23
  24 definition Z_of_nat \def
  25 \lambda n. match n with
  26 [ O \Rightarrow  OZ
  27 | (S n)\Rightarrow  pos n].
  28
  29 coercion Z_of_nat.
  30
  31 definition neg_Z_of_nat \def
  32 \lambda n. match n with
  33 [ O \Rightarrow  OZ
  34 | (S n)\Rightarrow  neg n].
  35
  36 definition absZ \def
  37 \lambda z.
  38  match z with
  39 [ OZ \Rightarrow O
  40 | (pos n) \Rightarrow n
  41 | (neg n) \Rightarrow n].
  42
  43 definition OZ_testb \def
  44 \lambda z.
  45 match z with
  46 [ OZ \Rightarrow true
  47 | (pos n) \Rightarrow false
  48 | (neg n) \Rightarrow false].
  49
  50 theorem OZ_discr :
  51 \forall z. if_then_else (OZ_testb z) (eq Z z OZ) (Not (eq Z z OZ)).
  52 intros.elim z.simplify.reflexivity.
  53 simplify.intros.
  54 cut match neg e1 with
  55 [ OZ \Rightarrow True
  56 | (pos n) \Rightarrow False
  57 | (neg n) \Rightarrow False].
  58 apply Hcut.rewrite > H.simplify.exact I.
  59 simplify.intros.
  60 cut match pos e2 with
  61 [ OZ \Rightarrow True
  62 | (pos n) \Rightarrow False
  63 | (neg n) \Rightarrow False].
  64 apply Hcut. rewrite > H.simplify.exact I.
  65 qed.
  66
  67 definition Zsucc \def
  68 \lambda z. match z with
  69 [ OZ \Rightarrow pos O
  70 | (pos n) \Rightarrow pos (S n)
  71 | (neg n) \Rightarrow
  72           match n with
  73           [ O \Rightarrow OZ
  74           | (S p) \Rightarrow neg p]].
  75
  76 definition Zpred \def
  77 \lambda z. match z with
  78 [ OZ \Rightarrow neg O
  79 | (pos n) \Rightarrow
  80           match n with
  81           [ O \Rightarrow OZ
  82           | (S p) \Rightarrow pos p]
  83 | (neg n) \Rightarrow neg (S n)].
  84
  85 theorem Zpred_succ: \forall z:Z. eq Z (Zpred (Zsucc z)) z.
  86 intros.elim z.reflexivity.
  87 elim e1.reflexivity.
  88 reflexivity.
  89 reflexivity.
  90 qed.
  91
  92 theorem Zsucc_pred: \forall z:Z. eq Z (Zsucc (Zpred z)) z.
  93 intros.elim z.reflexivity.
  94 reflexivity.
  95 elim e2.reflexivity.
  96 reflexivity.
  97 qed.
  98
  99 let rec Zplus x y : Z \def
 100   match x with
 101     [ OZ \Rightarrow y
 102     | (pos m) \Rightarrow
 103         match y with
 104          [ OZ \Rightarrow x
 105          | (pos n) \Rightarrow (pos (S (plus m n)))
 106          | (neg n) \Rightarrow
 107               match nat_compare m n with
 108                 [ LT \Rightarrow (neg (pred (minus n m)))
 109                 | EQ \Rightarrow OZ
 110                 | GT \Rightarrow (pos (pred (minus m n)))]]
 111     | (neg m) \Rightarrow
 112         match y with
 113          [ OZ \Rightarrow x
 114          | (pos n) \Rightarrow
 115               match nat_compare m n with
 116                 [ LT \Rightarrow (pos (pred (minus n m)))
 117                 | EQ \Rightarrow OZ
 118                 | GT \Rightarrow (neg (pred (minus m n)))]
 119          | (neg n) \Rightarrow (neg (S (plus m n)))]].
 120
 121 theorem Zplus_z_O:  \forall z:Z. eq Z (Zplus z OZ) z.
 122 intro.elim z.
 123 simplify.reflexivity.
 124 simplify.reflexivity.
 125 simplify.reflexivity.
 126 qed.
 127
 128 theorem sym_Zplus : \forall x,y:Z. eq Z (Zplus x y) (Zplus y x).
 129 intros.elim x.simplify.rewrite > Zplus_z_O.reflexivity.
 130 elim y.simplify.reflexivity.
 131 simplify.
 132 rewrite < sym_plus.reflexivity.
 133 simplify.
 134 rewrite > nat_compare_invert.
 135 simplify.elim nat_compare ? ?.simplify.reflexivity.
 136 simplify. reflexivity.
 137 simplify. reflexivity.
 138 elim y.simplify.reflexivity.
 139 simplify.rewrite > nat_compare_invert.
 140 simplify.elim nat_compare ? ?.simplify.reflexivity.
 141 simplify. reflexivity.
 142 simplify. reflexivity.
 143 simplify.elim (sym_plus ? ?).reflexivity.
 144 qed.
 145
 146 theorem Zpred_neg : \forall z:Z. eq Z (Zpred z) (Zplus (neg O) z).
 147 intros.elim z.
 148 simplify.reflexivity.
 149 simplify.reflexivity.
 150 elim e2.simplify.reflexivity.
 151 simplify.reflexivity.
 152 qed.
 153
 154 theorem Zsucc_pos : \forall z:Z. eq Z (Zsucc z) (Zplus (pos O) z).
 155 intros.elim z.
 156 simplify.reflexivity.
 157 elim e1.simplify.reflexivity.
 158 simplify.reflexivity.
 159 simplify.reflexivity.
 160 qed.
 161
 162 theorem Zplus_succ_pred_pp :
 163 \forall n,m. eq Z (Zplus (pos n) (pos m)) (Zplus (Zsucc (pos n)) (Zpred (pos m))).
 164 intros.
 165 elim n.elim m.
 166 simplify.reflexivity.
 167 simplify.reflexivity.
 168 elim m.
 169 simplify.
 170 rewrite < plus_n_O.reflexivity.
 171 simplify.
 172 rewrite < plus_n_Sm.reflexivity.
 173 qed.
 174
 175 theorem Zplus_succ_pred_pn :
 176 \forall n,m. eq Z (Zplus (pos n) (neg m)) (Zplus (Zsucc (pos n)) (Zpred (neg m))).
 177 intros.reflexivity.
 178 qed.
 179
 180 theorem Zplus_succ_pred_np :
 181 \forall n,m. eq Z (Zplus (neg n) (pos m)) (Zplus (Zsucc (neg n)) (Zpred (pos m))).
 182 intros.
 183 elim n.elim m.
 184 simplify.reflexivity.
 185 simplify.reflexivity.
 186 elim m.
 187 simplify.reflexivity.
 188 simplify.reflexivity.
 189 qed.
 190
 191 theorem Zplus_succ_pred_nn:
 192 \forall n,m. eq Z (Zplus (neg n) (neg m)) (Zplus (Zsucc (neg n)) (Zpred (neg m))).
 193 intros.
 194 elim n.elim m.
 195 simplify.reflexivity.
 196 simplify.reflexivity.
 197 elim m.
 198 simplify.rewrite < plus_n_Sm.reflexivity.
 199 simplify.rewrite > plus_n_Sm.reflexivity.
 200 qed.
 201
 202 theorem Zplus_succ_pred:
 203 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
 204 intros.
 205 elim x. elim y.
 206 simplify.reflexivity.
 207 simplify.reflexivity.
 208 rewrite < Zsucc_pos.rewrite > Zsucc_pred.reflexivity.
 209 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus (Zpred OZ).
 210 rewrite < Zpred_neg.rewrite > Zpred_succ.
 211 simplify.reflexivity.
 212 rewrite < Zplus_succ_pred_nn.reflexivity.
 213 apply Zplus_succ_pred_np.
 214 elim y.simplify.reflexivity.
 215 apply Zplus_succ_pred_pn.
 216 apply Zplus_succ_pred_pp.
 217 qed.
 218
 219 theorem Zsucc_plus_pp :
 220 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 221 intros.reflexivity.
 222 qed.
 223
 224 theorem Zsucc_plus_pn :
 225 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 226 intros.
 227 apply nat_double_ind
 228 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 229 intros.elim n1.
 230 simplify. reflexivity.
 231 elim e1.simplify. reflexivity.
 232 simplify. reflexivity.
 233 intros. elim n1.
 234 simplify. reflexivity.
 235 simplify.reflexivity.
 236 intros.
 237 rewrite < (Zplus_succ_pred_pn ? m1).
 238 elim H.reflexivity.
 239 qed.
 240
 241 theorem Zsucc_plus_nn :
 242 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 243 intros.
 244 apply nat_double_ind
 245 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 246 intros.elim n1.
 247 simplify. reflexivity.
 248 elim e1.simplify. reflexivity.
 249 simplify. reflexivity.
 250 intros. elim n1.
 251 simplify. reflexivity.
 252 simplify.reflexivity.
 253 intros.
 254 rewrite < (Zplus_succ_pred_nn ? m1).
 255 reflexivity.
 256 qed.
 257
 258 theorem Zsucc_plus_np :
 259 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 260 intros.
 261 apply nat_double_ind
 262 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 263 intros.elim n1.
 264 simplify. reflexivity.
 265 elim e1.simplify. reflexivity.
 266 simplify. reflexivity.
 267 intros. elim n1.
 268 simplify. reflexivity.
 269 simplify.reflexivity.
 270 intros.
 271 rewrite < H.
 272 rewrite < (Zplus_succ_pred_np ? (S m1)).
 273 reflexivity.
 274 qed.
 275
 276
 277 theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
 278 intros.elim x.elim y.
 279 simplify. reflexivity.
 280 rewrite < Zsucc_pos.reflexivity.
 281 simplify.reflexivity.
 282 elim y.rewrite < sym_Zplus.rewrite < sym_Zplus OZ.simplify.reflexivity.
 283 apply Zsucc_plus_nn.
 284 apply Zsucc_plus_np.
 285 elim y.
 286 rewrite < sym_Zplus OZ.reflexivity.
 287 apply Zsucc_plus_pn.
 288 apply Zsucc_plus_pp.
 289 qed.
 290
 291 theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 292 intros.
 293 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
 294 rewrite > Hcut.
 295 rewrite > Zsucc_plus.
 296 rewrite > Zpred_succ.
 297 reflexivity.
 298 rewrite > Zsucc_pred.
 299 reflexivity.
 300 qed.
 301
 302 theorem assoc_Zplus :
 303 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
 304 intros.elim x.simplify.reflexivity.
 305 elim e1.rewrite < (Zpred_neg (Zplus y z)).
 306 rewrite < (Zpred_neg y).
 307 rewrite < Zpred_plus.
 308 reflexivity.
 309 rewrite > Zpred_plus (neg e).
 310 rewrite > Zpred_plus (neg e).
 311 rewrite > Zpred_plus (Zplus (neg e) y).
 312 apply f_equal.assumption.
 313 elim e2.rewrite < Zsucc_pos.
 314 rewrite < Zsucc_pos.
 315 rewrite > Zsucc_plus.
 316 reflexivity.
 317 rewrite > Zsucc_plus (pos e1).
 318 rewrite > Zsucc_plus (pos e1).
 319 rewrite > Zsucc_plus (Zplus (pos e1) y).
 320 apply f_equal.assumption.
 321 qed.