helm/software/matita/library_auto/auto/Z/compare.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_autobatch/Z/compare".
  16
  17 include "auto/Z/orders.ma".
  18 include "auto/nat/compare.ma".
  19
  20 (* boolean equality *)
  21 definition eqZb : Z \to Z \to bool \def
  22 \lambda x,y:Z.
  23   match x with
  24   [ OZ \Rightarrow
  25       match y with
  26         [ OZ \Rightarrow true
  27         | (pos q) \Rightarrow false
  28         | (neg q) \Rightarrow false]
  29   | (pos p) \Rightarrow
  30       match y with
  31         [ OZ \Rightarrow false
  32         | (pos q) \Rightarrow eqb p q
  33         | (neg q) \Rightarrow false]
  34   | (neg p) \Rightarrow
  35       match y with
  36         [ OZ \Rightarrow false
  37         | (pos q) \Rightarrow false
  38         | (neg q) \Rightarrow eqb p q]].
  39
  40 theorem eqZb_to_Prop:
  41 \forall x,y:Z.
  42 match eqZb x y with
  43 [ true \Rightarrow x=y
  44 | false \Rightarrow x \neq y].
  45 intros.
  46 elim x
  47 [ elim y
  48   [ simplify.
  49     reflexivity
  50   | simplify.
  51     apply not_eq_OZ_pos
  52   | simplify.
  53     apply not_eq_OZ_neg
  54   ]
  55 | elim y
  56   [ simplify.
  57     unfold Not.
  58     intro.
  59     apply (not_eq_OZ_pos n).
  60     autobatch
  61     (*apply sym_eq.
  62     assumption*)
  63   | simplify.
  64     apply eqb_elim
  65     [ intro.
  66       simplify.
  67       autobatch
  68       (*apply eq_f.
  69       assumption*)
  70     | intro.
  71       simplify.
  72       unfold Not.
  73       intro.
  74       autobatch
  75       (*apply H.
  76       apply inj_pos.
  77       assumption*)
  78     ]
  79   | simplify.
  80     apply not_eq_pos_neg
  81   ]
  82 | elim y
  83   [ simplify.
  84     unfold Not.
  85     intro.
  86     apply (not_eq_OZ_neg n).
  87     autobatch
  88     (*apply sym_eq.
  89     assumption*)
  90   | simplify.
  91     unfold Not.
  92     intro.
  93     apply (not_eq_pos_neg n1 n).
  94     autobatch
  95     (*apply sym_eq.
  96     assumption*)
  97   | simplify.
  98     apply eqb_elim
  99     [ intro.
 100       simplify.
 101       autobatch
 102       (*apply eq_f.
 103       assumption*)
 104     | intro.
 105       simplify.
 106       unfold Not.
 107       intro.
 108       autobatch
 109       (*apply H.
 110       apply inj_neg.
 111       assumption*)
 112     ]
 113   ]
 114 ]
 115 qed.
 116
 117 theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
 118 (x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
 119 intros.
 120 cut
 121 (match (eqZb x y) with
 122 [ true \Rightarrow x=y
 123 | false \Rightarrow x \neq y] \to P (eqZb x y))
 124 [ apply Hcut.
 125   (*NB qui autobatch non chiude il goal*)
 126   apply eqZb_to_Prop
 127 | elim (eqZb)
 128   [ (*NB qui autobatch non chiude il goal*)
 129     apply (H H2)
 130   | (*NB qui autobatch non chiude il goal*)
 131     apply (H1 H2)
 132   ]
 133 ]
 134 qed.
 135
 136 definition Z_compare : Z \to Z \to compare \def
 137 \lambda x,y:Z.
 138   match x with
 139   [ OZ \Rightarrow
 140     match y with
 141     [ OZ \Rightarrow EQ
 142     | (pos m) \Rightarrow LT
 143     | (neg m) \Rightarrow GT ]
 144   | (pos n) \Rightarrow
 145     match y with
 146     [ OZ \Rightarrow GT
 147     | (pos m) \Rightarrow (nat_compare n m)
 148     | (neg m) \Rightarrow GT]
 149   | (neg n) \Rightarrow
 150     match y with
 151     [ OZ \Rightarrow LT
 152     | (pos m) \Rightarrow LT
 153     | (neg m) \Rightarrow nat_compare m n ]].
 154
 155 theorem Z_compare_to_Prop :
 156 \forall x,y:Z. match (Z_compare x y) with
 157 [ LT \Rightarrow x < y
 158 | EQ \Rightarrow x=y
 159 | GT \Rightarrow y < x].
 160 intros.
 161 elim x
 162 [ elim y
 163   [ simplify.
 164     apply refl_eq
 165   | simplify.
 166     exact I
 167   | simplify.
 168     exact I
 169   ]
 170 | elim y
 171   [ simplify.
 172     exact I
 173   | simplify.
 174     cut (match (nat_compare n n1) with
 175     [ LT \Rightarrow n<n1
 176     | EQ \Rightarrow n=n1
 177     | GT \Rightarrow n1<n] \to
 178     match (nat_compare n n1) with
 179     [ LT \Rightarrow (S n) \leq n1
 180     | EQ \Rightarrow pos n = pos n1
 181     | GT \Rightarrow (S n1) \leq n])
 182     [ apply Hcut.
 183       (*NB qui autobatch non chiude il goal*)
 184       apply nat_compare_to_Prop
 185     | elim (nat_compare n n1)
 186       [ simplify.
 187         (*NB qui autobatch non chiude il goal*)
 188         exact H
 189       | simplify.
 190         apply eq_f.
 191         (*NB qui autobatch non chiude il goal*)
 192         exact H
 193       | simplify.
 194         (*NB qui autobatch non chiude il goal*)
 195         exact H
 196       ]
 197     ]
 198   | simplify.
 199     exact I
 200   ]
 201 | elim y
 202   [ simplify.
 203     exact I
 204   | simplify.
 205     exact I
 206   | simplify.
 207     cut (match (nat_compare n1 n) with
 208     [ LT \Rightarrow n1<n
 209     | EQ \Rightarrow n1=n
 210     | GT \Rightarrow n<n1] \to
 211     match (nat_compare n1 n) with
 212     [ LT \Rightarrow (S n1) \leq n
 213     | EQ \Rightarrow neg n = neg n1
 214     | GT \Rightarrow (S n) \leq n1])
 215     [ apply Hcut.
 216       (*NB qui autobatch non chiude il goal*)
 217       apply nat_compare_to_Prop
 218     | elim (nat_compare n1 n)
 219       [ simplify.
 220         (*NB qui autobatch non chiude il goal*)
 221         exact H
 222       | simplify.
 223         apply eq_f.
 224         apply sym_eq.
 225         (*NB qui autobatch non chiude il goal*)
 226         exact H
 227       | simplify.
 228         (*NB qui autobatch non chiude il goal*)
 229         exact H
 230       ]
 231     ]
 232   ]
 233 ]
 234 qed.