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