1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/generated/insert_eq_1.ma".
16 include "ground/arith/pnat.ma".
18 (* ORDER FOR POSITIVE INTEGERS **********************************************)
20 inductive ple (p:pnat): predicate pnat ≝
22 | ple_succ_dx: ∀q. ple p q → ple p (↑q)
26 "less equal (positive integers)"
29 (* Basic constructions ******************************************************)
31 lemma ple_succ_dx_refl (p): p ≤ ↑p.
32 /2 width=1 by ple_refl, ple_succ_dx/ qed.
34 lemma ple_unit_sx (p): 𝟏 ≤ p.
35 #p elim p -p /2 width=1 by ple_succ_dx/
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/
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/
50 (* Basic destructions *******************************************************)
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/
56 (* Basic inversions *********************************************************)
58 lemma ple_inv_succ_bi (p) (q): ↑p ≤ ↑q → p ≤ q.
59 #p #q @(insert_eq_1 … (↑q))
63 /2 width=1 by ple_des_succ_sn/
67 lemma ple_inv_unit_dx (p): p ≤ 𝟏 → 𝟏 = p.
68 #p @(insert_eq_1 … (𝟏))
75 (* Advanced inversions ******************************************************)
77 lemma ple_inv_succ_unit (p): ↑p ≤ 𝟏 → ⊥.
79 lapply (ple_inv_unit_dx … H) -H #H destruct
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/
89 theorem ple_antisym (p) (q): p ≤ q → q ≤ p → p = q.
92 lapply (ple_des_succ_sn … Hq) #H
93 lapply (IH H) -IH -H #H destruct
94 elim (ple_inv_succ_sn_refl … Hq)
97 (* Advanced eliminations ****************************************************)
99 lemma ple_ind_alt (Q: relation2 pnat pnat):
101 (∀p,q. p ≤ q → 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/
109 (* Advanced constructions ***************************************************)
111 theorem ple_trans: Transitive … ple.
112 #p #q #H elim H -q /3 width=1 by ple_des_succ_sn/
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/