matita/matita/contribs/lambdadelta/ground/arith/pnat_le.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/generated/insert_eq_1.ma".
  16 include "ground/arith/pnat.ma".
  17
  18 (* ORDER FOR POSITIVE INTEGERS **********************************************)
  19
  20 inductive ple (p:pnat): predicate pnat ≝
  21 | ple_refl   : ple p p
  22 | ple_succ_dx: ∀q. ple p q → ple p (↑q)
  23 .
  24
  25 interpretation
  26   "less equal (positive integers)"
  27   'leq p q = (ple p q).
  28
  29 (* Basic constructions ******************************************************)
  30
  31 lemma ple_succ_dx_refl (p): p ≤ ↑p.
  32 /2 width=1 by ple_refl, ple_succ_dx/ qed.
  33
  34 lemma ple_unit_sx (p): 𝟏 ≤ p.
  35 #p elim p -p /2 width=1 by ple_succ_dx/
  36 qed.
  37
  38 lemma ple_succ_bi (p) (q): p ≤ q → ↑p ≤ ↑q.
  39 #p #q #H elim H -q /2 width=1 by ple_refl, ple_succ_dx/
  40 qed.
  41
  42 lemma pnat_split_le_ge (p) (q): ∨∨ p ≤ q | q ≤ p.
  43 #p #q @(pnat_ind_2 … p q) -p -q
  44 [ /2 width=1 by or_introl/
  45 | /2 width=1 by or_intror/
  46 | #p #q * /3 width=2 by ple_succ_bi, or_introl, or_intror/
  47 ]
  48 qed-.
  49
  50 (* Basic destructions *******************************************************)
  51
  52 lemma ple_des_succ_sn (p) (q): ↑p ≤ q → p ≤ q.
  53 #p #q #H elim H -q /2 width=1 by ple_succ_dx/
  54 qed-.
  55
  56 (* Basic inversions *********************************************************)
  57
  58 lemma ple_inv_succ_bi (p) (q): ↑p ≤ ↑q → p ≤ q.
  59 #p #q @(insert_eq_1 … (↑q))
  60 #x * -x
  61 [ #H destruct //
  62 | #o #Ho #H destruct
  63   /2 width=1 by ple_des_succ_sn/
  64 ]
  65 qed-.
  66
  67 lemma ple_inv_unit_dx (p): p ≤ 𝟏 → 𝟏 = p.
  68 #p @(insert_eq_1 … (𝟏))
  69 #y * -y
  70 [ #H destruct //
  71 | #y #_ #H destruct
  72 ]
  73 qed-.
  74
  75 (* Advanced inversions ******************************************************)
  76
  77 lemma ple_inv_succ_unit (p): ↑p ≤ 𝟏 → ⊥.
  78 #p #H
  79 lapply (ple_inv_unit_dx … H) -H #H destruct
  80 qed-.
  81
  82 lemma ple_inv_succ_sn_refl (p): ↑p ≤ p → ⊥.
  83 #p elim p -p [| #p #IH ] #H
  84 [ /2 width=2 by ple_inv_succ_unit/
  85 | /3 width=1 by ple_inv_succ_bi/
  86 ]
  87 qed-.
  88
  89 theorem ple_antisym (p) (q): p ≤ q → q ≤ p → p = q.
  90 #p #q #H elim H -q //
  91 #q #_ #IH #Hq
  92 lapply (ple_des_succ_sn … Hq) #H
  93 lapply (IH H) -IH -H #H destruct
  94 elim (ple_inv_succ_sn_refl … Hq)
  95 qed-.
  96
  97 (* Advanced eliminations ****************************************************)
  98
  99 lemma ple_ind_alt (Q: relation2 pnat pnat):
 100       (∀q. Q (𝟏) (q)) →
 101       (∀p,q. p ≤ q → Q p q → Q (↑p) (↑q)) →
 102       ∀p,q. p ≤ q → Q p q.
 103 #Q #IH1 #IH2 #p #q @(pnat_ind_2 … p q) -p -q //
 104 [ #p #_ #H elim (ple_inv_succ_unit … H)
 105 | /4 width=1 by ple_inv_succ_bi/
 106 ]
 107 qed-.
 108
 109 (* Advanced constructions ***************************************************)
 110
 111 theorem ple_trans: Transitive … ple.
 112 #p #q #H elim H -q /3 width=1 by ple_des_succ_sn/
 113 qed-.
 114
 115 lemma ple_dec (p) (q): Decidable … (p ≤ q).
 116 #p #q elim (pnat_split_le_ge p q) [ /2 width=1 by or_introl/ ]
 117 #Hqp elim (eq_pnat_dec p q) [ #H destruct /2 width=1 by ple_refl, or_introl/ ]
 118 /4 width=1 by ple_antisym, or_intror/
 119 qed-.