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/xoa/or_3.ma".
16 include "ground/arith/nat_le.ma".
18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
21 definition nlt: relation2 nat nat ≝
25 "less (non-negative integers)"
28 (* Basic constructions ******************************************************)
30 lemma nlt_i (m) (n): ↑m ≤ n → m < n.
33 lemma nlt_refl_succ (n): n < ↑n.
36 lemma nlt_succ_dx (m) (n): m ≤ n → m < ↑n.
37 /2 width=1 by nle_succ_bi/ qed.
40 lemma nlt_succ_dx_trans (m) (n): m < n → m < ↑n.
41 /2 width=1 by nle_succ_dx/ qed.
44 lemma nlt_zero_succ (m): 𝟎 < ↑m.
45 /2 width=1 by nle_succ_bi/ qed.
48 lemma nlt_succ_bi (m) (n): m < n → ↑m < ↑n.
49 /2 width=1 by nle_succ_bi/ qed.
51 (*** le_to_or_lt_eq *)
52 lemma nle_split_lt_eq (m) (n): m ≤ n → ∨∨ m < n | m = n.
53 #m #n * -n /3 width=1 by nle_succ_bi, or_introl/
57 lemma nat_split_zero_gt (n): ∨∨ 𝟎 = n | 𝟎 < n.
58 #n elim (nle_split_lt_eq (𝟎) n ?)
59 /2 width=1 by or_introl, or_intror/
63 lemma nat_split_lt_ge (m) (n): ∨∨ m < n | n ≤ m.
64 #m #n elim (nat_split_le_ge m n) /2 width=1 by or_intror/
65 #H elim (nle_split_lt_eq … H) -H /2 width=1 by nle_refl, or_introl, or_intror/
68 (*** lt_or_eq_or_gt *)
69 lemma nat_split_lt_eq_gt (m) (n): ∨∨ m < n | n = m | n < m.
70 #m #n elim (nat_split_lt_ge m n) /2 width=1 by or3_intro0/
71 #H elim (nle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
75 lemma le_false_nlt (m) (n): (n ≤ m → ⊥) → m < n.
76 #m #n elim (nat_split_lt_ge m n) [ // ]
80 (*** lt_to_le_to_lt *)
81 lemma nlt_nle_trans (o) (m) (n): m < o → o ≤ n → m < n.
82 /2 width=3 by nle_trans/ qed-.
84 (*** le_to_lt_to_lt *)
85 lemma nle_nlt_trans (o) (m) (n): m ≤ o → o < n → m < n.
86 /3 width=3 by nle_succ_bi, nle_trans/ qed-.
88 (* Basic inversions *********************************************************)
90 lemma nlt_inv_succ_dx (m) (n): m < ↑n → m ≤ n.
91 /2 width=1 by nle_inv_succ_bi/ qed-.
94 lemma nlt_inv_succ_bi (m) (n): ↑m < ↑n → m < n.
95 /2 width=1 by nle_inv_succ_bi/ qed-.
97 (*** lt_to_not_le lt_le_false *)
98 lemma nlt_ge_false (m) (n): m < n → n ≤ m → ⊥.
99 /3 width=4 by nle_inv_succ_sn_refl, nlt_nle_trans/ qed-.
101 (*** lt_to_not_eq lt_refl_false *)
102 lemma nlt_inv_refl (m): m < m → ⊥.
103 /2 width=4 by nlt_ge_false/ qed-.
105 (*** lt_zero_false *)
106 lemma nlt_inv_zero_dx (m): m < 𝟎 → ⊥.
107 /2 width=4 by nlt_ge_false/ qed-.
109 (* Basic destructions *******************************************************)
112 lemma nlt_des_le (m) (n): m < n → m ≤ n.
113 /2 width=3 by nle_trans/ qed-.
116 lemma nlt_des_lt_zero_sn (m) (n): m < n → 𝟎 < n.
117 /3 width=3 by nle_nlt_trans/ qed-.
119 (* Main constructions *******************************************************)
121 (*** transitive_lt *)
122 theorem nlt_trans: Transitive … nlt.
123 /3 width=3 by nlt_des_le, nlt_nle_trans/ qed-.
125 (* Advanced eliminations ****************************************************)
127 lemma nat_ind_lt_le (Q:predicate …):
128 (∀n. (∀m. m < n → Q m) → Q n) → ∀n,m. m ≤ n → Q m.
129 #Q #H1 #n @(nat_ind_succ … n) -n
130 [ #m #H <(nle_inv_zero_dx … H) -m
131 @H1 -H1 #o #H elim (nlt_inv_zero_dx … H)
132 | /5 width=3 by nlt_nle_trans, nle_inv_succ_bi/
137 lemma nat_ind_lt (Q:predicate …):
138 (∀n. (∀m. m < n → Q m) → Q n) → ∀n. Q n.
139 /4 width=2 by nat_ind_lt_le/ qed-.
142 lemma nlt_ind_alt (Q: relation2 nat nat):
144 (∀m,n. m < n → Q m n → Q (↑m) (↑n)) →
146 #Q #IH1 #IH2 #m #n @(nat_ind_2_succ … n m) -m -n //
148 elim (nlt_inv_zero_dx … H)
149 | /4 width=1 by nlt_inv_succ_bi/
153 (* Advanced constructions (decidability) ************************************)
156 lemma dec_nlt (R:predicate nat):
157 (∀n. Decidable … (R n)) →
158 ∀n. Decidable … (∃∃m. m < n & R m).
159 #R #HR #n @(nat_ind_succ … n) -n [| #n * ]
160 [ @or_intror * /2 width=2 by nlt_inv_zero_dx/
161 | * /4 width=3 by nlt_succ_dx_trans, ex2_intro, or_introl/
162 | #H0 elim (HR n) -HR
163 [ /3 width=3 by or_introl, ex2_intro/
164 | #Hn @or_intror * #m #Hmn #Hm
165 elim (nle_split_lt_eq … Hmn) -Hmn #H destruct [ -Hn | -H0 ]
166 [ /4 width=3 by nlt_inv_succ_bi, ex2_intro/
167 | lapply (eq_inv_nsucc_bi … H) -H /2 width=1 by/