]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_le.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_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/nat_succ.ma".
17
18 (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
19
20 (*** le *)
21 inductive nle (m:nat): predicate nat ≝
22 (*** le_n *)
23 | nle_refl   : nle m m
24 (*** le_S *)
25 | nle_succ_dx: ∀n. nle m n → nle m (↑n)
26 .
27
28 interpretation
29   "less equal (non-negative integers)"
30   'leq m n = (nle m n).
31
32 (* Basic constructions ******************************************************)
33
34 (*** le_n_Sn *)
35 lemma nle_succ_dx_refl (m): m ≤ ↑m.
36 /2 width=1 by nle_refl, nle_succ_dx/ qed.
37
38 (*** le_O_n *)
39 lemma nle_zero_sx (m): 𝟎 ≤ m.
40 #m @(nat_ind_succ … m) -m /2 width=1 by nle_succ_dx/
41 qed.
42
43 (*** le_S_S *)
44 lemma nle_succ_bi (m) (n): m ≤ n → ↑m ≤ ↑n.
45 #m #n #H elim H -n /2 width=1 by nle_refl, nle_succ_dx/
46 qed.
47
48 (*** le_or_ge *)
49 lemma nat_split_le_ge (m) (n): ∨∨ m ≤ n | n ≤ m.
50 #m #n @(nat_ind_2_succ … m n) -m -n
51 [ /2 width=1 by or_introl/
52 | /2 width=1 by or_intror/
53 | #m #n * /3 width=2 by nle_succ_bi, or_introl, or_intror/
54 ]
55 qed-.
56
57 (* Basic destructions *******************************************************)
58
59 lemma nle_des_succ_sn (m) (n): ↑m ≤ n → m ≤ n.
60 #m #n #H elim H -n /2 width=1 by nle_succ_dx/
61 qed-.
62
63 (* Basic inversions *********************************************************)
64
65 (*** le_S_S_to_le *)
66 lemma nle_inv_succ_bi (m) (n): ↑m ≤ ↑n → m ≤ n.
67 #m #n @(insert_eq_1 … (↑n))
68 #x * -x
69 [ #H >(eq_inv_nsucc_bi … H) -n //
70 | #o #Ho #H >(eq_inv_nsucc_bi … H) -n
71   /2 width=1 by nle_des_succ_sn/ 
72 ]
73 qed-.
74
75 (*** le_n_O_to_eq *)
76 lemma nle_inv_zero_dx (m): m ≤ 𝟎 → 𝟎 = m.
77 #m @(insert_eq_1 … (𝟎))
78 #y * -y
79 [ #H destruct //
80 | #y #_ #H elim (eq_inv_zero_nsucc … H)
81 ]
82 qed-.
83
84 (* Advanced inversions ******************************************************)
85
86 (*** le_plus_xSy_O_false *)
87 lemma nle_inv_succ_zero (m): ↑m ≤ 𝟎 → ⊥.
88 /3 width=2 by nle_inv_zero_dx, eq_inv_zero_nsucc/ qed-.
89
90 lemma nle_inv_succ_sn_refl (m): ↑m ≤ m → ⊥.
91 #m @(nat_ind_succ … m) -m [| #m #IH ] #H
92 [ /2 width=2 by nle_inv_succ_zero/
93 | /3 width=1 by nle_inv_succ_bi/
94 ]
95 qed-.
96
97 (*** le_to_le_to_eq *)
98 theorem nle_antisym (m) (n): m ≤ n → n ≤ m → m = n.
99 #m #n #H elim H -n //
100 #n #_ #IH #Hn
101 lapply (nle_des_succ_sn … Hn) #H
102 lapply (IH H) -IH -H #H destruct
103 elim (nle_inv_succ_sn_refl … Hn)
104 qed-.
105
106 (* Advanced eliminations ****************************************************)
107
108 (*** le_elim *)
109 lemma nle_ind_alt (Q: relation2 nat nat):
110       (∀n. Q (𝟎) (n)) →
111       (∀m,n. m ≤ n → Q m n → Q (↑m) (↑n)) →
112       ∀m,n. m ≤ n → Q m n.
113 #Q #IH1 #IH2 #m #n @(nat_ind_2_succ … m n) -m -n //
114 [ #m #_ #H elim (nle_inv_succ_zero … H)
115 | /4 width=1 by nle_inv_succ_bi/
116 ]
117 qed-.
118
119 (* Advanced constructions ***************************************************)
120
121 (*** transitive_le *)
122 theorem nle_trans: Transitive … nle.
123 #m #n #H elim H -n /3 width=1 by nle_des_succ_sn/
124 qed-.
125
126 (*** decidable_le le_dec *)
127 lemma nle_dec (m) (n): Decidable … (m ≤ n).
128 #m #n elim (nat_split_le_ge m n) [ /2 width=1 by or_introl/ ]
129 #Hnm elim (eq_nat_dec m n) [ #H destruct /2 width=1 by nle_refl, or_introl/ ]
130 /4 width=1 by nle_antisym, or_intror/
131 qed-.