matita/library_auto/auto/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/library_auto/Z/z".
  16
  17 include "datatypes/bool.ma".
  18 include "auto/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/library_auto/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.
  56 elim z
  57 [ (*qui auto non chiude il goal*)
  58   simplify.
  59   reflexivity
  60 | simplify.
  61   unfold Not.
  62   intros (H).
  63   (*qui auto non chiude il goal*)
  64   destruct H
  65 | simplify.
  66   unfold Not.
  67   intros (H).
  68   (*qui auto non chiude il goal*)
  69   destruct H
  70 ]
  71 qed.
  72
  73 (* discrimination *)
  74 theorem injective_pos: injective nat Z pos.
  75 unfold injective.
  76 intros.
  77 apply inj_S.
  78 change with (abs (pos x) = abs (pos y)).
  79 auto.
  80 (*apply eq_f.
  81 assumption.*)
  82 qed.
  83
  84 variant inj_pos : \forall n,m:nat. pos n = pos m \to n = m
  85 \def injective_pos.
  86
  87 theorem injective_neg: injective nat Z neg.
  88 unfold injective.
  89 intros.
  90 apply inj_S.
  91 change with (abs (neg x) = abs (neg y)).
  92 auto.
  93 (*apply eq_f.
  94 assumption.*)
  95 qed.
  96
  97 variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
  98 \def injective_neg.
  99
 100 theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
 101 unfold Not.
 102 intros (n H).
 103 (*qui auto non chiude il goal*)
 104 destruct H.
 105 qed.
 106
 107 theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
 108 unfold Not.
 109 intros (n H).
 110 (*qui auto non chiude il goal*)
 111 destruct H.
 112 qed.
 113
 114 theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
 115 unfold Not.
 116 intros (n m H).
 117 (*qui auto non chiude il goal*)
 118 destruct H.
 119 qed.
 120
 121 theorem decidable_eq_Z : \forall x,y:Z. decidable (x=y).
 122 intros.
 123 unfold decidable.
 124 elim x
 125 [ (* goal: x=OZ *)
 126   elim y
 127   [ (* goal: x=OZ y=OZ *)
 128     auto
 129     (*left.
 130     reflexivity*)
 131   | (* goal: x=OZ 2=2 *)
 132     auto
 133     (*right.
 134     apply not_eq_OZ_pos*)
 135   | (* goal: x=OZ 2=3 *)
 136     auto
 137     (*right.
 138     apply not_eq_OZ_neg*)
 139   ]
 140 | (* goal: x=pos *)
 141   elim y
 142   [ (* goal: x=pos y=OZ *)
 143     right.
 144     unfold Not.
 145     intro.
 146     apply (not_eq_OZ_pos n).
 147     auto
 148     (*symmetry.
 149     assumption*)
 150   | (* goal: x=pos y=pos *)
 151     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False)))
 152     [ auto
 153       (*left.
 154       apply eq_f.
 155       assumption*)
 156     | right.
 157       unfold Not.
 158       intros (H_inj).
 159       auto
 160       (*apply H.
 161       destruct H_inj.
 162       assumption*)
 163     ]
 164   | (* goal: x=pos y=neg *)
 165     auto
 166     (*right.
 167     unfold Not.
 168     intro.
 169     apply (not_eq_pos_neg n n1).
 170     assumption*)
 171   ]
 172 | (* goal: x=neg *)
 173   elim y
 174   [ (* goal: x=neg y=OZ *)
 175     right.
 176     unfold Not.
 177     intro.
 178     apply (not_eq_OZ_neg n).
 179     auto
 180     (*symmetry.
 181     assumption*)
 182   | (* goal: x=neg y=pos *)
 183     right.
 184     unfold Not.
 185     intro.
 186     apply (not_eq_pos_neg n1 n).
 187     auto
 188     (*symmetry.
 189     assumption*)
 190   | (* goal: x=neg y=neg *)
 191     elim (decidable_eq_nat n n1:((n=n1) \lor ((n=n1) \to False)))
 192     [ auto
 193       (*left.
 194       apply eq_f.
 195       assumption*)
 196     | right.
 197       unfold Not.
 198       intro.
 199       auto
 200       (*apply H.
 201       apply injective_neg.
 202       assumption*)
 203     ]
 204   ]
 205 ]
 206 qed.
 207
 208 (* end discrimination *)
 209
 210 definition Zsucc \def
 211 \lambda z. match z with
 212 [ OZ \Rightarrow pos O
 213 | (pos n) \Rightarrow pos (S n)
 214 | (neg n) \Rightarrow
 215           match n with
 216           [ O \Rightarrow OZ
 217           | (S p) \Rightarrow neg p]].
 218
 219 definition Zpred \def
 220 \lambda z. match z with
 221 [ OZ \Rightarrow neg O
 222 | (pos n) \Rightarrow
 223           match n with
 224           [ O \Rightarrow OZ
 225           | (S p) \Rightarrow pos p]
 226 | (neg n) \Rightarrow neg (S n)].
 227
 228 theorem Zpred_Zsucc: \forall z:Z. Zpred (Zsucc z) = z.
 229 intros.
 230 elim z
 231 [ reflexivity
 232 | reflexivity
 233 | elim n
 234   [ reflexivity
 235   | reflexivity
 236   ]
 237 ]
 238 qed.
 239
 240 theorem Zsucc_Zpred: \forall z:Z. Zsucc (Zpred z) = z.
 241 intros.
 242 elim z
 243 [ reflexivity
 244 | elim n
 245   [ reflexivity
 246   | reflexivity
 247   ]
 248 | reflexivity
 249 ]
 250 qed.
 251