helm/software/matita/contribs/library_auto/auto/nat/orders.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/orders".
  16
  17 include "auto/nat/nat.ma".
  18 include "higher_order_defs/ordering.ma".
  19
  20 (* definitions *)
  21 inductive le (n:nat) : nat \to Prop \def
  22   | le_n : le n n
  23   | le_S : \forall m:nat. le n m \to le n (S m).
  24
  25 interpretation "natural 'less or equal to'" 'leq x y = (le x y).
  26 interpretation "natural 'neither less nor equal to'" 'nleq x y = (Not (le x y)).
  27
  28 definition lt: nat \to nat \to Prop \def
  29 \lambda n,m:nat.(S n) \leq m.
  30
  31 interpretation "natural 'less than'" 'lt x y = (lt x y).
  32 interpretation "natural 'not less than'" 'nless x y = (Not (lt x y)).
  33
  34 definition ge: nat \to nat \to Prop \def
  35 \lambda n,m:nat.m \leq n.
  36
  37 interpretation "natural 'greater or equal to'" 'geq x y = (ge x y).
  38
  39 definition gt: nat \to nat \to Prop \def
  40 \lambda n,m:nat.m<n.
  41
  42 interpretation "natural 'greater than'" 'gt x y = (gt x y).
  43 interpretation "natural 'not greater than'" 'ngtr x y = (Not (gt x y)).
  44
  45 theorem transitive_le : transitive nat le.
  46 unfold transitive.
  47 intros.
  48 elim H1;autobatch.
  49 (*[ assumption
  50 | apply le_S.
  51   assumption
  52 ]*)
  53 qed.
  54
  55 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
  56 \def transitive_le.
  57
  58 theorem transitive_lt: transitive nat lt.
  59 unfold transitive.
  60 unfold lt.
  61 intros.
  62 elim H1;autobatch.
  63   (*apply le_S;assumption.*)
  64
  65 qed.
  66
  67 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
  68 \def transitive_lt.
  69
  70 theorem le_S_S: \forall n,m:nat. n \leq m \to S n \leq S m.
  71 intros.
  72 elim H;autobatch.
  73 (*[ apply le_n.
  74 | apply le_S.
  75   assumption
  76 ]*)
  77 qed.
  78
  79 theorem le_O_n : \forall n:nat. O \leq n.
  80 intros.
  81 elim n;autobatch.
  82 (*[ apply le_n
  83 | apply le_S.
  84   assumption
  85 ]*)
  86 qed.
  87
  88 theorem le_n_Sn : \forall n:nat. n \leq S n.
  89 intros.autobatch.
  90 (*apply le_S.
  91 apply le_n.*)
  92 qed.
  93
  94 theorem le_pred_n : \forall n:nat. pred n \leq n.
  95 intros.
  96 elim n;autobatch.
  97 (*[ simplify.
  98   apply le_n
  99 | simplify.
 100   apply le_n_Sn
 101 ]*)
 102 qed.
 103
 104 theorem le_S_S_to_le : \forall n,m:nat. S n \leq S m \to n \leq m.
 105 intros.
 106 change with (pred (S n) \leq pred (S m)).
 107 elim H;autobatch.
 108 (*[ apply le_n
 109 | apply (trans_le ? (pred n1))
 110   [ assumption
 111   | apply le_pred_n
 112   ]
 113 ]*)
 114 qed.
 115
 116 theorem leS_to_not_zero : \forall n,m:nat. S n \leq m \to not_zero m.
 117 intros.
 118 elim H
 119 [ (*qui autobatch non chiude il goal*)
 120   exact I
 121 | (*qui autobatch non chiude il goal*)
 122   exact I
 123 ]
 124 qed.
 125
 126 (* not le *)
 127 theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
 128 intros.
 129 unfold Not.
 130 simplify.
 131 intros.
 132 (*qui autobatch NON chiude il goal*)
 133 apply (leS_to_not_zero ? ? H).
 134 qed.
 135
 136 theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
 137 intros.
 138 elim n
 139 [ apply not_le_Sn_O
 140 | unfold Not.
 141   simplify.
 142   intros.autobatch
 143   (*cut (S n1 \leq n1).
 144   [ apply H.
 145     assumption
 146   | apply le_S_S_to_le.
 147     assumption
 148   ]*)
 149 ]
 150 qed.
 151
 152 (* le to lt or eq *)
 153 theorem le_to_or_lt_eq : \forall n,m:nat.
 154 n \leq m \to n < m \lor n = m.
 155 intros.
 156 elim H
 157 [ autobatch
 158   (*right.
 159   reflexivity*)
 160 | left.
 161   unfold lt.
 162   autobatch
 163   (*apply le_S_S.
 164   assumption*)
 165 ]
 166 qed.
 167
 168 (* not eq *)
 169 theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
 170 unfold Not.
 171 intros.
 172 cut ((le (S n) m) \to False)
 173 [ autobatch
 174   (*apply Hcut.
 175   assumption*)
 176 | rewrite < H1.
 177   apply not_le_Sn_n
 178 ]
 179 qed.
 180
 181 (* le vs. lt *)
 182 theorem lt_to_le : \forall n,m:nat. n<m \to n \leq m.
 183 simplify.
 184 intros.
 185 autobatch.
 186 (*unfold lt in H.
 187 elim H
 188 [ apply le_S.
 189   apply le_n
 190 | apply le_S.
 191   assumption
 192 ]*)
 193 qed.
 194
 195 theorem lt_S_to_le : \forall n,m:nat. n < S m \to n \leq m.
 196 autobatch.
 197 (*simplify.
 198 intros.
 199 apply le_S_S_to_le.
 200 assumption.*)
 201 qed.
 202
 203 theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
 204 intros 2.
 205 apply (nat_elim2 (\lambda n,m.n \nleq m \to m<n))
 206 [ intros.
 207   apply (absurd (O \leq n1));autobatch
 208   (*[ apply le_O_n
 209   | assumption
 210   ]*)
 211 | unfold Not.
 212   unfold lt.
 213   intros.autobatch
 214   (*apply le_S_S.
 215   apply le_O_n*)
 216 | unfold Not.
 217   unfold lt.
 218   intros.
 219   apply le_S_S.
 220   apply H.
 221   intros.
 222   autobatch
 223   (*apply H1.
 224   apply le_S_S.
 225   assumption*)
 226 ]
 227 qed.
 228
 229 theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
 230 unfold Not.
 231 unfold lt.
 232 intros 3.
 233 elim H;autobatch.
 234 (*[ apply (not_le_Sn_n n H1)
 235 | apply H2.
 236   apply lt_to_le.
 237   apply H3
 238 ]*)
 239 qed.
 240
 241 theorem not_lt_to_le: \forall n,m:nat. Not (lt n m) \to le m n.
 242 simplify.
 243 intros.
 244 apply lt_S_to_le.
 245 apply not_le_to_lt.
 246 (*qui autobatch non chiude il goal*)
 247 exact H.
 248 qed.
 249
 250 theorem le_to_not_lt: \forall n,m:nat. le n m \to Not (lt m n).
 251 intros.
 252 unfold Not.
 253 unfold lt.
 254 apply lt_to_not_le.
 255 unfold lt.autobatch.
 256 (*apply le_S_S.
 257 assumption.*)
 258 qed.
 259
 260 (* le elimination *)
 261 theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n.
 262 intro.
 263 elim n
 264 [ reflexivity
 265 | apply False_ind.autobatch
 266   (*apply not_le_Sn_O.
 267   goal 17. apply H1.*)
 268 ]
 269 qed.
 270
 271 theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop.
 272 P O \to P n.
 273 intro.
 274 elim n
 275 [ assumption
 276 | apply False_ind.
 277   apply  (not_le_Sn_O ? H1)
 278 ]
 279 qed.
 280
 281 theorem le_n_Sm_elim : \forall n,m:nat.n \leq S m \to
 282 \forall P:Prop. (S n \leq S m \to P) \to (n=S m \to P) \to P.
 283 intros 4.
 284 elim H;autobatch.
 285 (*[ apply H2.
 286   reflexivity
 287 | apply H3.
 288   apply le_S_S.
 289   assumption
 290 ]*)
 291 qed.
 292
 293 (* le to eq *)
 294 lemma le_to_le_to_eq: \forall n,m. n \le m \to m \le n \to n = m.
 295 apply nat_elim2
 296 [ intros.
 297   autobatch
 298   (*apply le_n_O_to_eq.
 299   assumption*)
 300 | intros.autobatch
 301   (*apply sym_eq.
 302   apply le_n_O_to_eq.
 303   assumption*)
 304 | intros.
 305   apply eq_f.autobatch
 306   (*apply H
 307   [ apply le_S_S_to_le.assumption
 308   | apply le_S_S_to_le.assumption
 309   ]*)
 310 ]
 311 qed.
 312
 313 (* lt and le trans *)
 314 theorem lt_O_S : \forall n:nat. O < S n.
 315 intro.autobatch.
 316 (*unfold.
 317 apply le_S_S.
 318 apply le_O_n.*)
 319 qed.
 320
 321 theorem lt_to_le_to_lt: \forall n,m,p:nat. lt n m \to le m p \to lt n p.
 322 intros.
 323 elim H1;autobatch.
 324 (*[ assumption
 325 | unfold lt.
 326   apply le_S.
 327   assumption
 328 ]*)
 329 qed.
 330
 331 theorem le_to_lt_to_lt: \forall n,m,p:nat. le n m \to lt m p \to lt n p.
 332 intros 4.
 333 elim H
 334 [ assumption
 335 | apply H2.autobatch
 336   (*unfold lt.
 337   apply lt_to_le.
 338   assumption*)
 339 ]
 340 qed.
 341
 342 theorem lt_S_to_lt: \forall n,m. S n < m \to n < m.
 343 intros.autobatch.
 344 (*apply (trans_lt ? (S n))
 345 [ apply le_n
 346 | assumption
 347 ]*)
 348 qed.
 349
 350 theorem ltn_to_ltO: \forall n,m:nat. lt n m \to lt O m.
 351 intros.
 352 apply (le_to_lt_to_lt O n)
 353 [ apply le_O_n
 354 | assumption
 355 ]
 356 qed.
 357
 358 theorem lt_O_n_elim: \forall n:nat. lt O n \to
 359 \forall P:nat\to Prop. (\forall m:nat.P (S m)) \to P n.
 360 intro.
 361 elim n
 362 [ apply False_ind.
 363   exact (not_le_Sn_O O H)
 364 | apply H2
 365 ]
 366 qed.
 367
 368 (* other abstract properties *)
 369 theorem antisymmetric_le : antisymmetric nat le.
 370 unfold antisymmetric.
 371 autobatch.
 372 (*intros 2.
 373 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m)))
 374 [ intros.
 375   apply le_n_O_to_eq.
 376   assumption
 377 | intros.
 378   apply False_ind.
 379   apply (not_le_Sn_O ? H)
 380 | intros.
 381   apply eq_f.
 382   apply H;
 383     apply le_S_S_to_le;assumption
 384 ]*)
 385 qed.
 386
 387 (*NOTA:
 388  * autobatch chiude il goal prima della tattica intros 2, tuttavia non chiude gli ultimi
 389  * 2 rami aperti dalla tattica apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
 390  * evidentemente autobatch sfrutta una dimostrazione diversa rispetto a quella proposta
 391  * nella libreria
 392  *)
 393
 394 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
 395 \def antisymmetric_le.
 396
 397 theorem decidable_le: \forall n,m:nat. decidable (n \leq m).
 398 intros.
 399 apply (nat_elim2 (\lambda n,m.decidable (n \leq m)))
 400 [ intros.
 401   unfold decidable.autobatch
 402   (*left.
 403   apply le_O_n*)
 404 | intros.
 405   unfold decidable.
 406   autobatch
 407   (*right.
 408   exact (not_le_Sn_O n1)*)
 409 | intros 2.
 410   unfold decidable.
 411   intro.
 412   elim H
 413   [ autobatch
 414     (*left.
 415     apply le_S_S.
 416     assumption*)
 417   | right.
 418     unfold Not.
 419     autobatch
 420     (*intro.
 421     apply H1.
 422     apply le_S_S_to_le.
 423     assumption*)
 424   ]
 425 ]
 426 qed.
 427
 428 theorem decidable_lt: \forall n,m:nat. decidable (n < m).
 429 intros.
 430 (*qui autobatch non chiude il goal*)
 431 exact (decidable_le (S n) m).
 432 qed.
 433
 434 (* well founded induction principles *)
 435
 436 theorem nat_elim1 : \forall n:nat.\forall P:nat \to Prop.
 437 (\forall m.(\forall p. (p \lt m) \to P p) \to P m) \to P n.
 438 intros.
 439 cut (\forall q:nat. q \le n \to P q)
 440 [ autobatch
 441   (*apply (Hcut n).
 442   apply le_n*)
 443 | elim n
 444   [ apply (le_n_O_elim q H1).
 445     apply H.
 446     intros.
 447     apply False_ind.
 448     apply (not_le_Sn_O p H2)
 449   | apply H.
 450     intros.
 451     apply H1.
 452     autobatch
 453     (*cut (p < S n1)
 454     [ apply lt_S_to_le.
 455       assumption
 456     | apply (lt_to_le_to_lt p q (S n1) H3 H2).
 457     ]*)
 458   ]
 459 ]
 460 qed.
 461
 462 (* some properties of functions *)
 463
 464 definition increasing \def \lambda f:nat \to nat.
 465 \forall n:nat. f n < f (S n).
 466
 467 theorem increasing_to_monotonic: \forall f:nat \to nat.
 468 increasing f \to monotonic nat lt f.
 469 unfold monotonic.
 470 unfold lt.
 471 unfold increasing.
 472 unfold lt.
 473 intros.
 474 elim H1;autobatch.
 475 (*[ apply H
 476 | apply (trans_le ? (f n1))
 477   [ assumption
 478   | apply (trans_le ? (S (f n1)))
 479     [ apply le_n_Sn
 480     | apply H
 481     ]
 482   ]
 483 ]*)
 484 qed.
 485
 486 theorem le_n_fn: \forall f:nat \to nat. (increasing f)
 487 \to \forall n:nat. n \le (f n).
 488 intros.
 489 elim n;autobatch.
 490 (*[ apply le_O_n
 491 | apply (trans_le ? (S (f n1)))
 492   [ apply le_S_S.
 493     apply H1
 494   | simplify in H.
 495     unfold increasing in H.
 496     unfold lt in H.
 497     apply H
 498   ]
 499 ]*)
 500 qed.
 501
 502 theorem increasing_to_le: \forall f:nat \to nat. (increasing f)
 503 \to \forall m:nat. \exists i. m \le (f i).
 504 intros.autobatch.
 505 (*elim m
 506 [ apply (ex_intro ? ? O).
 507   apply le_O_n
 508 | elim H1.
 509   apply (ex_intro ? ? (S a)).
 510   apply (trans_le ? (S (f a)))
 511   [ apply le_S_S.
 512     assumption
 513   | simplify in H.
 514     unfold increasing in H.
 515     unfold lt in H.
 516     apply H
 517   ]
 518 ]*)
 519 qed.
 520
 521 theorem increasing_to_le2: \forall f:nat \to nat. (increasing f)
 522 \to \forall m:nat. (f O) \le m \to
 523 \exists i. (f i) \le m \land m <(f (S i)).
 524 intros.
 525 elim H1
 526 [ autobatch.
 527   (*apply (ex_intro ? ? O).
 528   split
 529   [ apply le_n
 530   | apply H
 531   ]*)
 532 | elim H3.
 533   elim H4.
 534   cut ((S n1) < (f (S a)) \lor (S n1) = (f (S a)))
 535   [ elim Hcut
 536     [ apply (ex_intro ? ? a).
 537       autobatch
 538       (*split
 539       [ apply le_S.
 540         assumption
 541       | assumption
 542       ]*)
 543     | apply (ex_intro ? ? (S a)).
 544       split
 545       [ rewrite < H7.
 546         apply le_n
 547       | autobatch
 548         (*rewrite > H7.
 549         apply H*)
 550       ]
 551     ]
 552   | autobatch
 553     (*apply le_to_or_lt_eq.
 554     apply H6*)
 555   ]
 556 ]
 557 qed.