helm/software/matita/contribs/dama/dama/nat_ordered_set.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "nat/compare.ma".
  16 include "bishop_set.ma".
  17
  18 definition nat_excess : nat → nat → CProp ≝ λn,m. m<n.
  19
  20 lemma nat_elim2:
  21   ∀R:nat → nat → CProp.
  22   (∀ n:nat. R O n) → (∀n:nat. R (S n) O) → (∀n,m:nat. R n m → R (S n) (S m)) →
  23     ∀n,m:nat. R n m.
  24 intros 5;elim n; [apply H]
  25 cases m;[ apply H1| apply H2; apply H3 ]
  26 qed.
  27
  28 alias symbol "lt" = "natural 'less than'".
  29 lemma nat_discriminable: ∀x,y:nat.x < y ∨ x = y ∨ y < x.
  30 intros (x y); apply (nat_elim2 ???? x y);
  31 [1: intro;left;cases n; [right;reflexivity] left; apply lt_O_S;
  32 |2: intro;right;apply lt_O_S;
  33 |3: intros; cases H;
  34     [1: cases H1; [left; left; apply le_S_S; assumption]
  35         left;right;rewrite > H2; reflexivity;
  36     |2: right;apply le_S_S; assumption]]
  37 qed.
  38
  39 lemma nat_excess_cotransitive: cotransitive ? nat_excess.
  40 intros 3 (x y z); unfold nat_excess; simplify; intros;
  41 cases (nat_discriminable x z); [2: left; assumption] cases H1; clear H1;
  42 [1: right; apply (trans_lt ??? H H2);
  43 |2: right; rewrite < H2; assumption;]
  44 qed.
  45
  46 lemma nat_ordered_set : ordered_set.
  47 apply (mk_ordered_set ? nat_excess);
  48 [1: intro x; intro; apply (not_le_Sn_n ? H);
  49 |2: apply nat_excess_cotransitive]
  50 qed.
  51
  52 alias id "le" = "cic:/matita/nat/orders/le.ind#xpointer(1/1)".
  53 lemma os_le_to_nat_le:
  54   ∀a,b:nat_ordered_set.a ≤ b → le a b.
  55 intros; normalize in H; apply (not_lt_to_le ?? H);
  56 qed.
  57
  58 lemma nat_le_to_os_le:
  59   ∀a,b:nat_ordered_set.le a b → a ≤ b.
  60 intros 3; apply (le_to_not_lt a b);assumption;
  61 qed.
  62
  63 lemma nat_lt_to_os_lt:
  64   ∀a,b:nat_ordered_set.a < b → lt nat_ordered_set a b.
  65 intros 3; split;
  66 [1: apply nat_le_to_os_le; apply lt_to_le;assumption;
  67 |2: right; apply H;]
  68 qed.
  69
  70 lemma os_lt_to_nat_lt:
  71   ∀a,b:nat_ordered_set. lt nat_ordered_set a b → a < b.
  72 intros; cases H; clear H; cases H2;
  73 [2: apply H;| cases (H1 H)]
  74 qed.