helm/software/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 "datatypes/bool.ma".
  18 include "nat/nat.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 cic:/matita/Z/z/Z_of_nat.con.
  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 lemma pos_n_eq_S_n : \forall n : nat.
  38   (pos n) = (S n).
  39 intro.reflexivity.
  40 qed.
  41
  42 definition abs \def
  43 \lambda z.
  44  match z with
  45 [ OZ \Rightarrow O
  46 | (pos n) \Rightarrow (S n)
  47 | (neg n) \Rightarrow (S n)].
  48
  49 definition OZ_test \def
  50 \lambda z.
  51 match z with
  52 [ OZ \Rightarrow true
  53 | (pos n) \Rightarrow false
  54 | (neg n) \Rightarrow false].
  55
  56 theorem OZ_test_to_Prop :\forall z:Z.
  57 match OZ_test z with
  58 [true \Rightarrow z=OZ
  59 |false \Rightarrow z \neq OZ].
  60 intros.elim z.
  61 simplify.reflexivity.
  62 simplify. unfold Not. intros (H).
  63 destruct H.
  64 simplify. unfold Not. intros (H).
  65 destruct H.
  66 qed.
  67
  68 (* discrimination *)
  69 theorem injective_pos: injective nat Z pos.
  70 unfold injective.
  71 intros.
  72 apply inj_S.
  73 change with (abs (pos x) = abs (pos y)).
  74 apply eq_f.assumption.
  75 qed.
  76
  77 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
  78 \def injective_pos.
  79
  80 theorem injective_neg: injective nat Z neg.
  81 unfold injective.
  82 intros.
  83 apply inj_S.
  84 change with (abs (neg x) = abs (neg y)).
  85 apply eq_f.assumption.
  86 qed.
  87
  88 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
  89 \def injective_neg.
  90
  91 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
  92 unfold Not.intros (n H).
  93 destruct H.
  94 qed.
  95
  96 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
  97 unfold Not.intros (n H).
  98 destruct H.
  99 qed.
 100
 101 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
 102 unfold Not.intros (n m H).
 103 destruct H.
 104 qed.
 105
 106 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
 107 intros.unfold decidable.
 108 elim x.
 109 (* goal: x=OZ *)
 110   elim y.
 111   (* goal: x=OZ y=OZ *)
 112     left.reflexivity.
 113   (* goal: x=OZ 2=2 *)
 114     right.apply not_eq_OZ_pos.
 115   (* goal: x=OZ 2=3 *)
 116     right.apply not_eq_OZ_neg.
 117 (* goal: x=pos *)
 118   elim y.
 119   (* goal: x=pos y=OZ *)
 120     right.unfold Not.intro.
 121     apply (not_eq_OZ_pos n). symmetry. assumption.
 122   (* goal: x=pos y=pos *)
 123     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
 124     left.apply eq_f.assumption.
 125     right.unfold Not.intros (H_inj).apply H. destruct H_inj. reflexivity.
 126   (* goal: x=pos y=neg *)
 127     right.unfold Not.intro.apply (not_eq_pos_neg n n1). assumption.
 128 (* goal: x=neg *)
 129   elim y.
 130   (* goal: x=neg y=OZ *)
 131     right.unfold Not.intro.
 132     apply (not_eq_OZ_neg n). symmetry. assumption.
 133   (* goal: x=neg y=pos *)
 134     right. unfold Not.intro. apply (not_eq_pos_neg n1 n). symmetry. assumption.
 135   (* goal: x=neg y=neg *)
 136     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False))).
 137     left.apply eq_f.assumption.
 138     right.unfold Not.intro.apply H.apply injective_neg.assumption.
 139 qed.
 140
 141 (* end discrimination *)
 142
 143 definition Zsucc \def
 144 \lambda z. match z with
 145 [ OZ \Rightarrow pos O
 146 | (pos n) \Rightarrow pos (S n)
 147 | (neg n) \Rightarrow
 148           match n with
 149           [ O \Rightarrow OZ
 150           | (S p) \Rightarrow neg p]].
 151
 152 definition Zpred \def
 153 \lambda z. match z with
 154 [ OZ \Rightarrow neg O
 155 | (pos n) \Rightarrow
 156           match n with
 157           [ O \Rightarrow OZ
 158           | (S p) \Rightarrow pos p]
 159 | (neg n) \Rightarrow neg (S n)].
 160
 161 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
 162 intros.
 163 elim z.
 164   reflexivity.
 165   reflexivity.
 166   elim n.
 167     reflexivity.
 168     reflexivity.
 169 qed.
 170
 171 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
 172 intros.
 173 elim z.
 174   reflexivity.
 175   elim n.
 176     reflexivity.
 177     reflexivity.
 178   reflexivity.
 179 qed.
 180