]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/pnat_lt.ma
update in delayed_updating
[helm.git] / 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-.