helm/matita/library/Z/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/z".
  16
  17 include "nat/nat.ma".
  18 include "higher_order_defs/functions.ma".
  19
  20 inductive Z : Set \def
  21   OZ : Z
  22 | pos : nat \to Z
  23 | neg : nat \to Z.
  24
  25 definition Z_of_nat \def
  26 \lambda n. match n with
  27 [ O \Rightarrow  OZ
  28 | (S n)\Rightarrow  pos n].
  29
  30 coercion Z_of_nat.
  31
  32 definition neg_Z_of_nat \def
  33 \lambda n. match n with
  34 [ O \Rightarrow  OZ
  35 | (S n)\Rightarrow  neg n].
  36
  37 definition abs \def
  38 \lambda z.
  39  match z with
  40 [ OZ \Rightarrow O
  41 | (pos n) \Rightarrow n
  42 | (neg n) \Rightarrow n].
  43
  44 definition OZ_test \def
  45 \lambda z.
  46 match z with
  47 [ OZ \Rightarrow true
  48 | (pos n) \Rightarrow false
  49 | (neg n) \Rightarrow false].
  50
  51 theorem OZ_test_to_Prop :\forall z:Z.
  52 match OZ_test z with
  53 [true \Rightarrow z=OZ
  54 |false \Rightarrow \lnot (z=OZ)].
  55 intros.elim z.
  56 simplify.reflexivity.
  57 simplify.intros.
  58 cut match neg n with
  59 [ OZ \Rightarrow True
  60 | (pos n) \Rightarrow False
  61 | (neg n) \Rightarrow False].
  62 apply Hcut.rewrite > H.simplify.exact I.
  63 simplify.intros.
  64 cut match pos n with
  65 [ OZ \Rightarrow True
  66 | (pos n) \Rightarrow False
  67 | (neg n) \Rightarrow False].
  68 apply Hcut. rewrite > H.simplify.exact I.
  69 qed.
  70
  71 (* discrimination *)
  72 theorem injective_pos: injective nat Z pos.
  73 simplify.
  74 intros.
  75 change with abs (pos x) = abs (pos y).
  76 apply eq_f.assumption.
  77 qed.
  78
  79 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
  80 \def injective_pos.
  81
  82 theorem injective_neg: injective nat Z neg.
  83 simplify.
  84 intros.
  85 change with abs (neg x) = abs (neg y).
  86 apply eq_f.assumption.
  87 qed.
  88
  89 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
  90 \def injective_neg.
  91
  92 theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)).
  93 simplify.intros.
  94 change with
  95   match pos n with
  96   [ OZ \Rightarrow True
  97   | (pos n) \Rightarrow False
  98   | (neg n) \Rightarrow False].
  99 rewrite < H.
 100 simplify.exact I.
 101 qed.
 102
 103 theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)).
 104 simplify.intros.
 105 change with
 106   match neg n with
 107   [ OZ \Rightarrow True
 108   | (pos n) \Rightarrow False
 109   | (neg n) \Rightarrow False].
 110 rewrite < H.
 111 simplify.exact I.
 112 qed.
 113
 114 theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)).
 115 simplify.intros.
 116 change with
 117   match neg m with
 118   [ OZ \Rightarrow False
 119   | (pos n) \Rightarrow True
 120   | (neg n) \Rightarrow False].
 121 rewrite < H.
 122 simplify.exact I.
 123 qed.
 124
 125 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
 126 intros.simplify.
 127 elim x.elim y.
 128 left.reflexivity.
 129 right.apply not_eq_OZ_neg.
 130 right.apply not_eq_OZ_pos.
 131 elim y.right.intro.
 132 apply not_eq_OZ_neg n ?.apply sym_eq.assumption.
 133 elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
 134 left.apply eq_f.assumption.
 135 right.intro.apply H.apply injective_neg.assumption.
 136 right.intro.apply not_eq_pos_neg n1 n ?.apply sym_eq.assumption.
 137 elim y.right.intro.
 138 apply not_eq_OZ_pos n ?.apply sym_eq.assumption.
 139 right.apply not_eq_pos_neg.
 140 elim (decidable_eq_nat n n1:(Or (n=n1) ((n=n1) \to False))).
 141 left.apply eq_f.assumption.
 142 right.intro.apply H.apply injective_pos.assumption.
 143 qed.
 144
 145 (* end discrimination *)
 146
 147 definition Zsucc \def
 148 \lambda z. match z with
 149 [ OZ \Rightarrow pos O
 150 | (pos n) \Rightarrow pos (S n)
 151 | (neg n) \Rightarrow
 152           match n with
 153           [ O \Rightarrow OZ
 154           | (S p) \Rightarrow neg p]].
 155
 156 definition Zpred \def
 157 \lambda z. match z with
 158 [ OZ \Rightarrow neg O
 159 | (pos n) \Rightarrow
 160           match n with
 161           [ O \Rightarrow OZ
 162           | (S p) \Rightarrow pos p]
 163 | (neg n) \Rightarrow neg (S n)].
 164
 165 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
 166 intros.elim z.reflexivity.
 167 elim n.reflexivity.
 168 reflexivity.
 169 reflexivity.
 170 qed.
 171
 172 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
 173 intros.elim z.reflexivity.
 174 reflexivity.
 175 elim n.reflexivity.
 176 reflexivity.
 177 qed.
 178