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