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