helm/software/matita/library/nat/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 include "datatypes/bool.ma".
  16 include "datatypes/compare.ma".
  17 include "nat/orders.ma".
  18
  19 let rec eqb n m \def
  20 match n with
  21   [ O \Rightarrow
  22      match m with
  23      [ O \Rightarrow true
  24            | (S q) \Rightarrow false]
  25   | (S p) \Rightarrow
  26            match m with
  27      [ O \Rightarrow false
  28            | (S q) \Rightarrow eqb p q]].
  29
  30 theorem eqb_to_Prop: \forall n,m:nat.
  31 match (eqb n m) with
  32 [ true  \Rightarrow n = m
  33 | false \Rightarrow n \neq m].
  34 intros.
  35 apply (nat_elim2
  36 (\lambda n,m:nat.match (eqb n m) with
  37 [ true  \Rightarrow n = m
  38 | false \Rightarrow n \neq m])).
  39 intro.elim n1.
  40 simplify.reflexivity.
  41 simplify.apply not_eq_O_S.
  42 intro.
  43 simplify.unfold Not.
  44 intro. apply (not_eq_O_S n1).apply sym_eq.assumption.
  45 intros.simplify.
  46 generalize in match H.
  47 elim ((eqb n1 m1)).
  48 simplify.apply eq_f.apply H1.
  49 simplify.unfold Not.intro.apply H1.apply inj_S.assumption.
  50 qed.
  51
  52 theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
  53 (n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)).
  54 intros.
  55 cut
  56 (match (eqb n m) with
  57 [ true  \Rightarrow n = m
  58 | false \Rightarrow n \neq m] \to (P (eqb n m))).
  59 apply Hcut.apply eqb_to_Prop.
  60 elim (eqb n m).
  61 apply ((H H2)).
  62 apply ((H1 H2)).
  63 qed.
  64
  65 theorem eqb_n_n: \forall n. eqb n n = true.
  66 intro.elim n.simplify.reflexivity.
  67 simplify.assumption.
  68 qed.
  69
  70 theorem eqb_true_to_eq: \forall n,m:nat.
  71 eqb n m = true \to n = m.
  72 intros.
  73 change with
  74 match true with
  75 [ true  \Rightarrow n = m
  76 | false \Rightarrow n \neq m].
  77 rewrite < H.
  78 apply eqb_to_Prop.
  79 qed.
  80
  81 theorem eqb_false_to_not_eq: \forall n,m:nat.
  82 eqb n m = false \to n \neq m.
  83 intros.
  84 change with
  85 match false with
  86 [ true  \Rightarrow n = m
  87 | false \Rightarrow n \neq m].
  88 rewrite < H.
  89 apply eqb_to_Prop.
  90 qed.
  91
  92 theorem eq_to_eqb_true: \forall n,m:nat.
  93 n = m \to eqb n m = true.
  94 intros.apply (eqb_elim n m).
  95 intros. reflexivity.
  96 intros.apply False_ind.apply (H1 H).
  97 qed.
  98
  99 theorem not_eq_to_eqb_false: \forall n,m:nat.
 100 \lnot (n = m) \to eqb n m = false.
 101 intros.apply (eqb_elim n m).
 102 intros. apply False_ind.apply (H H1).
 103 intros.reflexivity.
 104 qed.
 105
 106 let rec leb n m \def
 107 match n with
 108     [ O \Rightarrow true
 109     | (S p) \Rightarrow
 110         match m with
 111         [ O \Rightarrow false
 112         | (S q) \Rightarrow leb p q]].
 113
 114 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop.
 115 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
 116 P (leb n m).
 117 apply nat_elim2; intros; simplify
 118   [apply H.apply le_O_n
 119   |apply H1.apply not_le_Sn_O.
 120   |apply H;intros
 121     [apply H1.apply le_S_S.assumption.
 122     |apply H2.unfold Not.intros.apply H3.apply le_S_S_to_le.assumption
 123     ]
 124   ]
 125 qed.
 126
 127 theorem leb_true_to_le:\forall n,m.
 128 leb n m = true \to (n \le m).
 129 intros 2.
 130 apply leb_elim
 131   [intros.assumption
 132   |intros.destruct H1.
 133   ]
 134 qed.
 135
 136 theorem leb_false_to_not_le:\forall n,m.
 137 leb n m = false \to \lnot (n \le m).
 138 intros 2.
 139 apply leb_elim
 140   [intros.destruct H1
 141   |intros.assumption
 142   ]
 143 qed.
 144 (*
 145 theorem decidable_le: \forall n,m. n \leq m \lor n \nleq m.
 146 intros.
 147 apply (leb_elim n m)
 148   [intro.left.assumption
 149   |intro.right.assumption
 150   ]
 151 qed.
 152 *)
 153
 154 theorem le_to_leb_true: \forall n,m. n \leq m \to leb n m = true.
 155 intros.apply leb_elim;intros
 156   [reflexivity
 157   |apply False_ind.apply H1.apply H.
 158   ]
 159 qed.
 160
 161 theorem lt_to_leb_false: \forall n,m. m < n \to leb n m = false.
 162 intros.apply leb_elim;intros
 163   [apply False_ind.apply (le_to_not_lt ? ? H1). assumption
 164   |reflexivity
 165   ]
 166 qed.
 167
 168 theorem leb_to_Prop: \forall n,m:nat.
 169 match (leb n m) with
 170 [ true  \Rightarrow n \leq m
 171 | false \Rightarrow n \nleq m].
 172 apply nat_elim2;simplify
 173   [exact le_O_n
 174   |exact not_le_Sn_O
 175   |intros 2.simplify.
 176    elim ((leb n m));simplify
 177     [apply le_S_S.apply H
 178     |unfold Not.intros.apply H.apply le_S_S_to_le.assumption
 179     ]
 180   ]
 181 qed.
 182
 183 (*
 184 theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop.
 185 (n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
 186 P (leb n m).
 187 intros.
 188 cut
 189 (match (leb n m) with
 190 [ true  \Rightarrow n \leq m
 191 | false \Rightarrow n \nleq m] \to (P (leb n m))).
 192 apply Hcut.apply leb_to_Prop.
 193 elim (leb n m).
 194 apply ((H H2)).
 195 apply ((H1 H2)).
 196 qed.
 197 *)
 198
 199 definition ltb ≝λn,m. leb n m ∧ notb (eqb n m).
 200
 201 theorem ltb_to_Prop :
 202  ∀n,m.
 203   match ltb n m with
 204   [ true ⇒ n < m
 205   | false ⇒ n ≮ m
 206   ].
 207 intros;
 208 unfold ltb;
 209 apply leb_elim;
 210 apply eqb_elim;
 211 intros;
 212 simplify;
 213 [ rewrite < H;
 214   apply le_to_not_lt;
 215   constructor 1
 216 | apply (not_eq_to_le_to_lt ? ? H H1)
 217 | rewrite < H;
 218   apply le_to_not_lt;
 219   constructor 1
 220 | apply le_to_not_lt;
 221   generalize in match (not_le_to_lt ? ? H1);
 222   clear H1;
 223   intro;
 224   apply lt_to_le;
 225   assumption
 226 ].
 227 qed.
 228
 229 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
 230 (n < m → (P true)) → (n ≮ m → (P false)) →
 231 P (ltb n m).
 232 intros.
 233 cut
 234 (match (ltb n m) with
 235 [ true  ⇒ n < m
 236 | false ⇒ n ≮ m] → (P (ltb n m))).
 237 apply Hcut.apply ltb_to_Prop.
 238 elim (ltb n m).
 239 apply ((H H2)).
 240 apply ((H1 H2)).
 241 qed.
 242
 243 let rec nat_compare n m: compare \def
 244 match n with
 245 [ O \Rightarrow
 246     match m with
 247       [ O \Rightarrow EQ
 248       | (S q) \Rightarrow LT ]
 249 | (S p) \Rightarrow
 250     match m with
 251       [ O \Rightarrow GT
 252       | (S q) \Rightarrow nat_compare p q]].
 253
 254 theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
 255 intro.elim n.
 256 simplify.reflexivity.
 257 simplify.assumption.
 258 qed.
 259
 260 theorem nat_compare_S_S: \forall n,m:nat.
 261 nat_compare n m = nat_compare (S n) (S m).
 262 intros.simplify.reflexivity.
 263 qed.
 264
 265 theorem nat_compare_pred_pred:
 266 \forall n,m:nat.lt O n \to lt O m \to
 267 eq compare (nat_compare n m) (nat_compare (pred n) (pred m)).
 268 intros.
 269 apply (lt_O_n_elim n H).
 270 apply (lt_O_n_elim m H1).
 271 intros.
 272 simplify.reflexivity.
 273 qed.
 274
 275 theorem nat_compare_to_Prop: \forall n,m:nat.
 276 match (nat_compare n m) with
 277   [ LT \Rightarrow n < m
 278   | EQ \Rightarrow n=m
 279   | GT \Rightarrow m < n ].
 280 intros.
 281 apply (nat_elim2 (\lambda n,m.match (nat_compare n m) with
 282   [ LT \Rightarrow n < m
 283   | EQ \Rightarrow n=m
 284   | GT \Rightarrow m < n ])).
 285 intro.elim n1.simplify.reflexivity.
 286 simplify.unfold lt.apply le_S_S.apply le_O_n.
 287 intro.simplify.unfold lt.apply le_S_S. apply le_O_n.
 288 intros 2.simplify.elim ((nat_compare n1 m1)).
 289 simplify. unfold lt. apply le_S_S.apply H.
 290 simplify. apply eq_f. apply H.
 291 simplify. unfold lt.apply le_S_S.apply H.
 292 qed.
 293
 294 theorem nat_compare_n_m_m_n: \forall n,m:nat.
 295 nat_compare n m = compare_invert (nat_compare m n).
 296 intros.
 297 apply (nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n))).
 298 intros.elim n1.simplify.reflexivity.
 299 simplify.reflexivity.
 300 intro.elim n1.simplify.reflexivity.
 301 simplify.reflexivity.
 302 intros.simplify.elim H.reflexivity.
 303 qed.
 304
 305 theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
 306 (n < m \to P LT) \to (n=m \to P EQ) \to (m < n \to P GT) \to
 307 (P (nat_compare n m)).
 308 intros.
 309 cut (match (nat_compare n m) with
 310 [ LT \Rightarrow n < m
 311 | EQ \Rightarrow n=m
 312 | GT \Rightarrow m < n] \to
 313 (P (nat_compare n m))).
 314 apply Hcut.apply nat_compare_to_Prop.
 315 elim ((nat_compare n m)).
 316 apply ((H H3)).
 317 apply ((H1 H3)).
 318 apply ((H2 H3)).
 319 qed.
 320
 321 inductive cmp_cases (n,m:nat) : CProp ≝
 322   | cmp_le : n ≤ m → cmp_cases n m
 323   | cmp_gt : m < n → cmp_cases n m.
 324
 325 lemma cmp_nat: ∀n,m.cmp_cases n m.
 326 intros; generalize in match (nat_compare_to_Prop n m);
 327 cases (nat_compare n m); intros;
 328 [constructor 1;apply lt_to_le|constructor 1;rewrite > H|constructor 2]
 329 try assumption; apply le_n;
 330 qed.