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