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/arith/nat_le.ma".
  16
  17 (* NON-NEGATIVE INTEGERS ****************************************************)
  18
  19 (*** lt *)
  20 definition nlt: relation2 nat nat ≝
  21            λm,n. ↑m ≤ n.
  22
  23 interpretation
  24   "less (non-negative integers)"
  25   'lt m n = (nlt m n).
  26
  27 (* Basic constructions ******************************************************)
  28
  29 lemma nlt_i (m) (n): ↑m ≤ n → m < n.
  30 // qed.
  31
  32 lemma nlt_refl_succ (n): n < ↑n.
  33 // qed.
  34
  35 (*** lt_O_S *)
  36 lemma nlt_zero_succ (m): 𝟎 < ↑m.
  37 /2 width=1 by nle_succ_bi/ qed.
  38
  39 (*** le_to_or_lt_eq *)
  40 lemma nle_lt_eq_e (m) (n): m ≤ n → ∨∨ m < n | m = n.
  41 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/
  42 qed-.
  43
  44 (*** eq_or_gt *)
  45 lemma eq_gt_e (n): ∨∨ 𝟎 = n | 𝟎 < n.
  46 #n elim (nle_lt_eq_e (𝟎) n ?)
  47 /2 width=1 by or_introl, or_intror/
  48 qed-.
  49
  50 (*** lt_or_ge *)
  51 lemma nlt_ge_e (m) (n): ∨∨ m < n | n ≤ m.
  52 #m #n elim (nle_ge_e m n) /2 width=1 by or_intror/
  53 #H elim (nle_lt_eq_e … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
  54 qed-.
  55
  56 (*** not_le_to_lt *)
  57 lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
  58 #m #n elim (nlt_ge_e m n) [ // ]
  59 #H #Hn elim Hn -Hn //
  60 qed.
  61
  62 (*** lt_to_le_to_lt *)
  63 lemma nlt_le_trans (o) (m) (n): m < o → o ≤ n → m < n.
  64 /2 width=3 by nle_trans/ qed-.
  65
  66 lemma le_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
  67 /3 width=3 by nle_succ_bi, nle_trans/ qed-.
  68
  69 (* Basic inversions *********************************************************)
  70
  71 (*** lt_to_not_le *)
  72 lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
  73 /3 width=4 by nle_inv_succ_sn_refl, nlt_le_trans/ qed-.
  74
  75 (*** lt_to_not_eq *)
  76 lemma nlt_inv_refl (m): m < m → ⊥.
  77 /2 width=4 by nlt_ge_false/ qed-.
  78
  79 lemma nlt_inv_zero_dx (m): m < 𝟎 → ⊥.
  80 /2 width=4 by nlt_ge_false/ qed-.
  81
  82 (* Basic destructions *******************************************************)
  83
  84 (*** lt_to_le *)
  85 lemma nlt_des_le (m) (n): m < n → m ≤ n.
  86 /2 width=3 by nle_trans/ qed-.
  87
  88 (*** ltn_to_ltO *)
  89 lemma nlt_des_lt_O_sn (m) (n): m < n → 𝟎 < n.
  90 /3 width=3 by le_nlt_trans/ qed-.
  91
  92 (* Main constructions *******************************************************)
  93
  94 (*** transitive_lt *)
  95 theorem nlt_trans: Transitive … nlt.
  96 /3 width=3 by nlt_des_le, nlt_le_trans/ qed-.
  97
  98 (* Advanced eliminations ****************************************************)
  99
 100 lemma nat_ind_lt_le (Q:predicate …):
 101       (∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
 102 #Q #H1 #n @(nat_ind … n) -n
 103 [ #m #H <(nle_inv_zero_dx … H) -m
 104   @H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
 105 | /5 width=3 by nlt_le_trans, nle_inv_succ_bi/
 106 ]
 107 qed-.
 108
 109 (*** nat_elim1 *)
 110 lemma nat_ind_lt (Q:predicate …):
 111       (∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
 112 /4 width=2 by nat_ind_lt_le/ qed-.