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