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 y.reflexivity.
 130 elim y.simplify.reflexivity.
 131 simplify.
 132 rewrite < (sym_plus e e1).reflexivity.
 133 simplify.
 134 rewrite > nat_compare_invert e1 e2.
 135 simplify.elim nat_compare e2 e1.simplify.reflexivity.
 136 simplify. reflexivity.
 137 simplify. reflexivity.
 138 elim y.simplify.reflexivity.
 139 simplify.rewrite > nat_compare_invert e1 e2.
 140 simplify.elim nat_compare e2 e1.simplify.reflexivity.
 141 simplify. reflexivity.
 142 simplify. reflexivity.
 143 simplify.elim (sym_plus e2 e).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 e1.reflexivity.
 171 simplify.
 172 rewrite < plus_n_Sm e1 e.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 e1 O.reflexivity.
 199 simplify.rewrite > plus_n_Sm e1 (S e).reflexivity.
 200 qed.
 201
 202 (* da qui in avanti rewrite ancora non utilizzata *)
 203
 204 theorem Zplus_succ_pred:
 205 \forall x,y. eq Z (Zplus x y) (Zplus (Zsucc x) (Zpred y)).
 206 intros.
 207 elim x. elim y.
 208 simplify.reflexivity.
 209 simplify.reflexivity.
 210 elim (Zsucc_pos ?).elim (sym_eq ? ? ? (Zsucc_pred ?)).reflexivity.
 211 elim y.elim sym_Zplus ? ?.elim sym_Zplus (Zpred OZ) ?.
 212 elim (Zpred_neg ?).elim (sym_eq ? ? ? (Zpred_succ ?)).
 213 simplify.reflexivity.
 214 apply Zplus_succ_pred_nn.
 215 apply Zplus_succ_pred_np.
 216 elim y.simplify.reflexivity.
 217 apply Zplus_succ_pred_pn.
 218 apply Zplus_succ_pred_pp.
 219 qed.
 220
 221 theorem Zsucc_plus_pp :
 222 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (pos m)) (Zsucc (Zplus (pos n) (pos m))).
 223 intros.reflexivity.
 224 qed.
 225
 226 theorem Zsucc_plus_pn :
 227 \forall n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m))).
 228 intros.
 229 apply nat_double_ind
 230 (\lambda n,m. eq Z (Zplus (Zsucc (pos n)) (neg m)) (Zsucc (Zplus (pos n) (neg m)))).intro.
 231 intros.elim n1.
 232 simplify. reflexivity.
 233 elim e1.simplify. reflexivity.
 234 simplify. reflexivity.
 235 intros. elim n1.
 236 simplify. reflexivity.
 237 simplify.reflexivity.
 238 intros.
 239 elim (Zplus_succ_pred_pn ? m1).
 240 elim H.reflexivity.
 241 qed.
 242
 243 theorem Zsucc_plus_nn :
 244 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m))).
 245 intros.
 246 apply nat_double_ind
 247 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (neg m)) (Zsucc (Zplus (neg n) (neg m)))).intro.
 248 intros.elim n1.
 249 simplify. reflexivity.
 250 elim e1.simplify. reflexivity.
 251 simplify. reflexivity.
 252 intros. elim n1.
 253 simplify. reflexivity.
 254 simplify.reflexivity.
 255 intros.
 256 elim (Zplus_succ_pred_nn ? m1).
 257 reflexivity.
 258 qed.
 259
 260 theorem Zsucc_plus_np :
 261 \forall n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m))).
 262 intros.
 263 apply nat_double_ind
 264 (\lambda n,m. eq Z (Zplus (Zsucc (neg n)) (pos m)) (Zsucc (Zplus (neg n) (pos m)))).
 265 intros.elim n1.
 266 simplify. reflexivity.
 267 elim e1.simplify. reflexivity.
 268 simplify. reflexivity.
 269 intros. elim n1.
 270 simplify. reflexivity.
 271 simplify.reflexivity.
 272 intros.
 273 elim H.
 274 elim (Zplus_succ_pred_np ? (S m1)).
 275 reflexivity.
 276 qed.
 277
 278
 279 theorem Zsucc_plus : \forall x,y:Z. eq Z (Zplus (Zsucc x) y) (Zsucc (Zplus x y)).
 280 intros.elim x.elim y.
 281 simplify. reflexivity.
 282 elim (Zsucc_pos ?).reflexivity.
 283 simplify.reflexivity.
 284 elim y.elim sym_Zplus ? ?.elim sym_Zplus OZ ?.simplify.reflexivity.
 285 apply Zsucc_plus_nn.
 286 apply Zsucc_plus_np.
 287 elim y.
 288 elim (sym_Zplus OZ ?).reflexivity.
 289 apply Zsucc_plus_pn.
 290 apply Zsucc_plus_pp.
 291 qed.
 292
 293 theorem Zpred_plus : \forall x,y:Z. eq Z (Zplus (Zpred x) y) (Zpred (Zplus x y)).
 294 intros.
 295 cut eq Z (Zpred (Zplus x y)) (Zpred (Zplus (Zsucc (Zpred x)) y)).
 296 elim (sym_eq ? ? ? Hcut).
 297 elim (sym_eq ? ? ? (Zsucc_plus ? ?)).
 298 elim (sym_eq ? ? ? (Zpred_succ ?)).
 299 reflexivity.
 300 elim (sym_eq ? ? ? (Zsucc_pred ?)).
 301 reflexivity.
 302 qed.
 303
 304 theorem assoc_Zplus :
 305 \forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
 306 intros.elim x.simplify.reflexivity.
 307 elim e1.elim (Zpred_neg (Zplus y z)).
 308 elim (Zpred_neg y).
 309 elim (Zpred_plus ? ?).
 310 reflexivity.
 311 elim (sym_eq ? ? ? (Zpred_plus (neg e) ?)).
 312 elim (sym_eq ? ? ? (Zpred_plus (neg e) ?)).
 313 elim (sym_eq ? ? ? (Zpred_plus (Zplus (neg e) y) ?)).
 314 apply f_equal.assumption.
 315 elim e2.elim (Zsucc_pos ?).
 316 elim (Zsucc_pos ?).
 317 apply (sym_eq ? ? ? (Zsucc_plus ? ?)) .
 318 elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)).
 319 elim (sym_eq ? ? ? (Zsucc_plus (pos e1) ?)).
 320 elim (sym_eq ? ? ? (Zsucc_plus (Zplus (pos e1) y) ?)).
 321 apply f_equal.assumption.
 322 qed.