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