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