matita/matita/contribs/lambdadelta/ground/arith/pnat_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/pnat_le.ma".
  17
  18 (* STRICT ORDER FOR POSITIVE INTEGERS ***************************************)
  19
  20 definition plt: relation2 pnat pnat ≝
  21            λp,q. ↑p ≤ q.
  22
  23 interpretation
  24   "less (positive integers)"
  25   'lt p q = (plt p q).
  26
  27 (* Basic constructions ******************************************************)
  28
  29 lemma plt_i (p) (q): ↑p ≤ q → p < q.
  30 // qed.
  31
  32 lemma plt_refl_succ (q): q < ↑q.
  33 // qed.
  34
  35 lemma plt_succ_dx (p) (q): p ≤ q → p < ↑q.
  36 /2 width=1 by ple_succ_bi/ qed.
  37
  38 lemma plt_succ_dx_trans (p) (q): p < q → p < ↑q.
  39 /2 width=1 by ple_succ_dx/ qed.
  40
  41 lemma plt_unit_succ (p): 𝟏 < ↑p.
  42 /2 width=1 by ple_succ_bi/ qed.
  43
  44 lemma plt_succ_bi (p) (q): p < q → ↑p < ↑q.
  45 /2 width=1 by ple_succ_bi/ qed.
  46
  47 lemma ple_split_lt_eq (p) (q): p ≤ q → ∨∨ p < q | p = q.
  48 #p #q * -q /3 width=1 by ple_succ_bi, or_introl/
  49 qed-.
  50
  51 lemma pnat_split_unit_gt (q): ∨∨ 𝟏 = q | 𝟏 < q.
  52 #q elim (ple_split_lt_eq (𝟏) q ?)
  53 /2 width=1 by or_introl, or_intror/
  54 qed-.
  55
  56 lemma pnat_split_lt_ge (p) (q): ∨∨ p < q | q ≤ p.
  57 #p #q elim (pnat_split_le_ge p q) /2 width=1 by or_intror/
  58 #H elim (ple_split_lt_eq … H) -H /2 width=1 by ple_refl, or_introl, or_intror/
  59 qed-.
  60
  61 lemma pnat_split_lt_eq_gt (p) (q): ∨∨ p < q | q = p | q < p.
  62 #p #q elim (pnat_split_lt_ge p q) /2 width=1 by or3_intro0/
  63 #H elim (ple_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
  64 qed-.
  65
  66 lemma le_false_plt (p) (q): (q ≤ p → ⊥) → p < q.
  67 #p #q elim (pnat_split_lt_ge p q) [ // ]
  68 #H #Hq elim Hq -Hq //
  69 qed.
  70
  71 lemma plt_ple_trans (r) (p) (q): p < r → r ≤ q → p < q.
  72 /2 width=3 by ple_trans/ qed-.
  73
  74 lemma ple_plt_trans (r) (p) (q): p ≤ r → r < q → p < q.
  75 /3 width=3 by ple_succ_bi, ple_trans/ qed-.
  76
  77 (* Basic inversions *********************************************************)
  78
  79 lemma plt_inv_succ_dx (p) (q): p < ↑q → p ≤ q.
  80 /2 width=1 by ple_inv_succ_bi/ qed-.
  81
  82 lemma plt_inv_succ_bi (p) (q): ↑p < ↑q → p < q.
  83 /2 width=1 by ple_inv_succ_bi/ qed-.
  84
  85 lemma plt_ge_false (p) (q): p < q → q ≤ p → ⊥.
  86 /3 width=4 by ple_inv_succ_sn_refl, plt_ple_trans/ qed-.
  87
  88 lemma plt_inv_refl (p): p < p → ⊥.
  89 /2 width=4 by plt_ge_false/ qed-.
  90
  91 lemma plt_inv_unit_dx (p): p < 𝟏 → ⊥.
  92 /2 width=4 by plt_ge_false/ qed-.
  93
  94 (* Basic destructions *******************************************************)
  95
  96 lemma plt_des_le (p) (q): p < q → p ≤ q.
  97 /2 width=3 by ple_trans/ qed-.
  98
  99 lemma plt_des_lt_unit_sn (p) (q): p < q → 𝟏 < q.
 100 /3 width=3 by ple_plt_trans/ qed-.
 101
 102 (* Main constructions *******************************************************)
 103
 104 theorem plt_trans: Transitive … plt.
 105 /3 width=3 by plt_des_le, plt_ple_trans/ qed-.
 106
 107 (* Advanced eliminations ****************************************************)
 108
 109 lemma pnat_ind_lt_le (Q:predicate …):
 110       (∀q. (∀p. p < q → Q p) → Q q) → ∀q,p. p ≤ q → Q p.
 111 #Q #H1 #q elim q -q
 112 [ #p #H <(ple_inv_unit_dx … H) -p
 113   @H1 -H1 #r #H elim (plt_inv_unit_dx … H)
 114 | /5 width=3 by plt_ple_trans, ple_inv_succ_bi/
 115 ]
 116 qed-.
 117
 118 lemma pnat_ind_lt (Q:predicate …):
 119       (∀q. (∀p. p < q → Q p) → Q q) → ∀q. Q q.
 120 /4 width=2 by pnat_ind_lt_le/ qed-.
 121
 122 lemma plt_ind_alt (Q: relation2 pnat pnat):
 123       (∀q. Q (𝟏) (↑q)) →
 124       (∀p,q. p < q → Q p q → Q (↑p) (↑q)) →
 125       ∀p,q. p < q → Q p q.
 126 #Q #IH1 #IH2 #p #q @(pnat_ind_2 … q p) -p -q //
 127 [ #p #H
 128   elim (plt_inv_unit_dx … H)
 129 | /4 width=1 by plt_inv_succ_bi/
 130 ]
 131 qed-.
 132
 133 (* Advanced constructions (decidability) ************************************)
 134
 135 lemma dec_plt (R:predicate pnat):
 136       (∀q. Decidable … (R q)) →
 137       ∀q. Decidable … (∃∃p. p < q & R p).
 138 #R #HR #q elim q -q [| #q * ]
 139 [ @or_intror * /2 width=2 by plt_inv_unit_dx/
 140 | * /4 width=3 by plt_succ_dx_trans, ex2_intro, or_introl/
 141 | #H0 elim (HR q) -HR
 142   [ /3 width=3 by or_introl, ex2_intro/
 143   | #Hq @or_intror * #p #Hpq #Hp
 144     elim (ple_split_lt_eq … Hpq) -Hpq #H destruct [ -Hq | -H0 ]
 145     /4 width=3 by plt_inv_succ_bi, ex2_intro/
 146   ]
 147 ]
 148 qed-.