matita/matita/contribs/lambdadelta/ground/arith/nat_lt.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 "ground/xoa/or_3.ma".
  16 include "ground/arith/nat_le.ma".
  17
  18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
  19
  20 (*** lt *)
  21 definition nlt: relation2 nat nat ≝
  22            λm,n. ↑m ≤ n.
  23
  24 interpretation
  25   "less (non-negative integers)"
  26   'lt m n = (nlt m n).
  27
  28 (* Basic constructions ******************************************************)
  29
  30 lemma nlt_i (m) (n): ↑m ≤ n → m < n.
  31 // qed.
  32
  33 lemma nlt_refl_succ (n): n < ↑n.
  34 // qed.
  35
  36 lemma nlt_succ_dx (m) (n): m ≤ n → m < ↑n.
  37 /2 width=1 by nle_succ_bi/ qed.
  38
  39 (*** lt_S *)
  40 lemma nlt_succ_dx_trans (m) (n): m < n → m < ↑n.
  41 /2 width=1 by nle_succ_dx/ qed.
  42
  43 (*** lt_O_S *)
  44 lemma nlt_zero_succ (m): 𝟎 < ↑m.
  45 /2 width=1 by nle_succ_bi/ qed.
  46
  47 (*** lt_S_S *)
  48 lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n.
  49 /2 width=1 by nle_succ_bi/ qed.
  50
  51 (*** le_to_or_lt_eq *)
  52 lemma nle_split_lt_eq (m) (n): m ≤ n → ∨∨ m < n | m = n.
  53 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/
  54 qed-.
  55
  56 (*** eq_or_gt *)
  57 lemma nat_split_zero_gt (n): ∨∨ 𝟎 = n | 𝟎 < n.
  58 #n elim (nle_split_lt_eq (𝟎) n ?)
  59 /2 width=1 by or_introl, or_intror/
  60 qed-.
  61
  62 (*** lt_or_ge *)
  63 lemma nat_split_lt_ge (m) (n): ∨∨ m < n | n ≤ m.
  64 #m #n elim (nat_split_le_ge m n) /2 width=1 by or_intror/
  65 #H elim (nle_split_lt_eq … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
  66 qed-.
  67
  68 (*** lt_or_eq_or_gt *)
  69 lemma nat_split_lt_eq_gt (m) (n): ∨∨ m < n | n = m | n < m.
  70 #m #n elim (nat_split_lt_ge m n) /2 width=1 by or3_intro0/
  71 #H elim (nle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
  72 qed-.
  73
  74 (*** not_le_to_lt *)
  75 lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
  76 #m #n elim (nat_split_lt_ge m n) [ // ]
  77 #H #Hn elim Hn -Hn //
  78 qed.
  79
  80 (*** lt_to_le_to_lt *)
  81 lemma nlt_nle_trans (o) (m) (n): m < o → o ≤ n → m < n.
  82 /2 width=3 by nle_trans/ qed-.
  83
  84 (*** le_to_lt_to_lt *)
  85 lemma nle_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
  86 /3 width=3 by nle_succ_bi, nle_trans/ qed-.
  87
  88 (* Basic inversions *********************************************************)
  89
  90 lemma nlt_inv_succ_dx (m) (n): m < ↑n → m ≤ n.
  91 /2 width=1 by nle_inv_succ_bi/ qed-.
  92
  93 (*** lt_S_S_to_lt *)
  94 lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n.
  95 /2 width=1 by nle_inv_succ_bi/ qed-.
  96
  97 (*** lt_to_not_le lt_le_false *)
  98 lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
  99 /3 width=4 by nle_inv_succ_sn_refl, nlt_nle_trans/ qed-.
 100
 101 (*** lt_to_not_eq lt_refl_false *)
 102 lemma nlt_inv_refl (m): m < m → ⊥.
 103 /2 width=4 by nlt_ge_false/ qed-.
 104
 105 (*** lt_zero_false *)
 106 lemma nlt_inv_zero_dx (m): m < 𝟎 → ⊥.
 107 /2 width=4 by nlt_ge_false/ qed-.
 108
 109 (* Basic destructions *******************************************************)
 110
 111 (*** lt_to_le *)
 112 lemma nlt_des_le (m) (n): m < n → m ≤ n.
 113 /2 width=3 by nle_trans/ qed-.
 114
 115 (*** ltn_to_ltO *)
 116 lemma nlt_des_lt_zero_sn (m) (n): m < n → 𝟎 < n.
 117 /3 width=3 by nle_nlt_trans/ qed-.
 118
 119 (* Main constructions *******************************************************)
 120
 121 (*** transitive_lt *)
 122 theorem nlt_trans: Transitive … nlt.
 123 /3 width=3 by nlt_des_le, nlt_nle_trans/ qed-.
 124
 125 (* Advanced eliminations ****************************************************)
 126
 127 lemma nat_ind_lt_le (Q:predicate …):
 128       (∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
 129 #Q #H1 #n @(nat_ind_succ … n) -n
 130 [ #m #H <(nle_inv_zero_dx … H) -m
 131   @H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
 132 | /5 width=3 by nlt_nle_trans, nle_inv_succ_bi/
 133 ]
 134 qed-.
 135
 136 (*** nat_elim1 *)
 137 lemma nat_ind_lt (Q:predicate …):
 138       (∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
 139 /4 width=2 by nat_ind_lt_le/ qed-.
 140
 141 (*** lt_elim *)
 142 lemma nlt_ind_alt (Q: relation2 nat nat):
 143       (∀n. Q (𝟎) (↑n)) →
 144       (∀m,n. m < n → Q m n → Q (↑m) (↑n)) →
 145       ∀m,n. m < n → Q m n.
 146 #Q #IH1 #IH2 #m #n @(nat_ind_2_succ … n m) -m -n //
 147 [ #m #H
 148   elim (nlt_inv_zero_dx … H)
 149 | /4 width=1 by nlt_inv_succ_bi/
 150 ]
 151 qed-.
 152
 153 (* Advanced constructions (decidability) ************************************)
 154
 155 (*** dec_lt *)
 156 lemma dec_nlt (R:predicate nat):
 157       (∀n. Decidable … (R n)) →
 158       ∀n. Decidable … (∃∃m. m < n & R m).
 159 #R #HR #n @(nat_ind_succ … n) -n [| #n * ]
 160 [ @or_intror * /2 width=2 by nlt_inv_zero_dx/
 161 | * /4 width=3 by nlt_succ_dx_trans, ex2_intro, or_introl/
 162 | #H0 elim (HR n) -HR
 163   [ /3 width=3 by or_introl, ex2_intro/
 164   | #Hn @or_intror * #m #Hmn #Hm
 165     elim (nle_split_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
 166     [ /4 width=3 by nlt_inv_succ_bi, ex2_intro/
 167     | lapply (eq_inv_nsucc_bi … H) -H /2 width=1 by/
 168   ]
 169 ]
 170 qed-.