]> matita.cs.unibo.it Git - helm.git/blob - matita/library/nat/lt_arith.ma
More work on groups, real numbers and integration algebras.
[helm.git] / matita / library / nat / lt_arith.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/nat/lt_arith".
16
17 include "nat/div_and_mod.ma".
18
19 (* plus *)
20 theorem monotonic_lt_plus_r: 
21 \forall n:nat.monotonic nat lt (\lambda m.n+m).
22 simplify.intros.
23 elim n.simplify.assumption.
24 simplify.unfold lt.
25 apply le_S_S.assumption.
26 qed.
27
28 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
29 monotonic_lt_plus_r.
30
31 theorem monotonic_lt_plus_l: 
32 \forall n:nat.monotonic nat lt (\lambda m.m+n).
33 simplify.
34 intros.
35 rewrite < sym_plus. rewrite < (sym_plus n).
36 apply lt_plus_r.assumption.
37 qed.
38
39 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
40 monotonic_lt_plus_l.
41
42 theorem lt_plus: \forall n,m,p,q:nat. n < m \to p < q \to n + p < m + q.
43 intros.
44 apply (trans_lt ? (n + q)).
45 apply lt_plus_r.assumption.
46 apply lt_plus_l.assumption.
47 qed.
48
49 theorem lt_plus_to_lt_l :\forall n,p,q:nat. p+n < q+n \to p<q.
50 intro.elim n.
51 rewrite > plus_n_O.
52 rewrite > (plus_n_O q).assumption.
53 apply H.
54 unfold lt.apply le_S_S_to_le.
55 rewrite > plus_n_Sm.
56 rewrite > (plus_n_Sm q).
57 exact H1.
58 qed.
59
60 theorem lt_plus_to_lt_r :\forall n,p,q:nat. n+p < n+q \to p<q.
61 intros.apply (lt_plus_to_lt_l n). 
62 rewrite > sym_plus.
63 rewrite > (sym_plus q).assumption.
64 qed.
65
66 (* times and zero *)
67 theorem lt_O_times_S_S: \forall n,m:nat.O < (S n)*(S m).
68 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
69 qed.
70
71 (* times *)
72 theorem monotonic_lt_times_r: 
73 \forall n:nat.monotonic nat lt (\lambda m.(S n)*m).
74 simplify.
75 intros.elim n.
76 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
77 apply lt_plus.assumption.assumption.
78 qed.
79
80 theorem lt_times_r: \forall n,p,q:nat. p < q \to (S n) * p < (S n) * q
81 \def monotonic_lt_times_r.
82
83 theorem monotonic_lt_times_l: 
84 \forall m:nat.monotonic nat lt (\lambda n.n * (S m)).
85 simplify.
86 intros.
87 rewrite < sym_times.rewrite < (sym_times (S m)).
88 apply lt_times_r.assumption.
89 qed.
90
91 variant lt_times_l: \forall n,p,q:nat. p<q \to p*(S n) < q*(S n)
92 \def monotonic_lt_times_l.
93
94 theorem lt_times:\forall n,m,p,q:nat. n<m \to p<q \to n*p < m*q.
95 intro.
96 elim n.
97 apply (lt_O_n_elim m H).
98 intro.
99 cut (lt O q).
100 apply (lt_O_n_elim q Hcut).
101 intro.change with (O < (S m1)*(S m2)).
102 apply lt_O_times_S_S.
103 apply (ltn_to_ltO p q H1).
104 apply (trans_lt ? ((S n1)*q)).
105 apply lt_times_r.assumption.
106 cut (lt O q).
107 apply (lt_O_n_elim q Hcut).
108 intro.
109 apply lt_times_l.
110 assumption.
111 apply (ltn_to_ltO p q H2).
112 qed.
113
114 theorem lt_times_to_lt_l: 
115 \forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
116 intros.
117 cut (p < q \lor p \nlt q).
118 elim Hcut.
119 assumption.
120 absurd (p * (S n) < q * (S n)).
121 assumption.
122 apply le_to_not_lt.
123 apply le_times_l.
124 apply not_lt_to_le.
125 assumption.
126 exact (decidable_lt p q).
127 qed.
128
129 theorem lt_times_to_lt_r: 
130 \forall n,p,q:nat. (S n)*p < (S n)*q \to lt p q.
131 intros.
132 apply (lt_times_to_lt_l n).
133 rewrite < sym_times.
134 rewrite < (sym_times (S n)).
135 assumption.
136 qed.
137
138 theorem nat_compare_times_l : \forall n,p,q:nat. 
139 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
140 intros.apply nat_compare_elim.intro.
141 apply nat_compare_elim.
142 intro.reflexivity.
143 intro.absurd (p=q).
144 apply (inj_times_r n).assumption.
145 apply lt_to_not_eq. assumption.
146 intro.absurd (q<p).
147 apply (lt_times_to_lt_r n).assumption.
148 apply le_to_not_lt.apply lt_to_le.assumption.
149 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
150 intro.apply nat_compare_elim.intro.
151 absurd (p<q).
152 apply (lt_times_to_lt_r n).assumption.
153 apply le_to_not_lt.apply lt_to_le.assumption.
154 intro.absurd (q=p).
155 symmetry.
156 apply (inj_times_r n).assumption.
157 apply lt_to_not_eq.assumption.
158 intro.reflexivity.
159 qed.
160
161 (* div *) 
162
163 theorem eq_mod_O_to_lt_O_div: \forall n,m:nat. O < m \to O < n\to n \mod m = O \to O < n / m. 
164 intros 4.apply (lt_O_n_elim m H).intros.
165 apply (lt_times_to_lt_r m1).
166 rewrite < times_n_O.
167 rewrite > (plus_n_O ((S m1)*(n / (S m1)))).
168 rewrite < H2.
169 rewrite < sym_times.
170 rewrite < div_mod.
171 rewrite > H2.
172 assumption.
173 unfold lt.apply le_S_S.apply le_O_n.
174 qed.
175
176 theorem lt_div_n_m_n: \forall n,m:nat. (S O) < m \to O < n \to n / m \lt n.
177 intros.
178 apply (nat_case1 (n / m)).intro.
179 assumption.intros.rewrite < H2.
180 rewrite > (div_mod n m) in \vdash (? ? %).
181 apply (lt_to_le_to_lt ? ((n / m)*m)).
182 apply (lt_to_le_to_lt ? ((n / m)*(S (S O)))).
183 rewrite < sym_times.
184 rewrite > H2.
185 simplify.unfold lt.
186 rewrite < plus_n_O.
187 rewrite < plus_n_Sm.
188 apply le_S_S.
189 apply le_S_S.
190 apply le_plus_n.
191 apply le_times_r.
192 assumption.
193 rewrite < sym_plus.
194 apply le_plus_n.
195 apply (trans_lt ? (S O)).
196 unfold lt. apply le_n.assumption.
197 qed.
198
199 (* general properties of functions *)
200 theorem monotonic_to_injective: \forall f:nat\to nat.
201 monotonic nat lt f \to injective nat nat f.
202 unfold injective.intros.
203 apply (nat_compare_elim x y).
204 intro.apply False_ind.apply (not_le_Sn_n (f x)).
205 rewrite > H1 in \vdash (? ? %).
206 change with (f x < f y).
207 apply H.apply H2.
208 intros.assumption.
209 intro.apply False_ind.apply (not_le_Sn_n (f y)).
210 rewrite < H1 in \vdash (? ? %).
211 change with (f y < f x).
212 apply H.apply H2.
213 qed.
214
215 theorem increasing_to_injective: \forall f:nat\to nat.
216 increasing f \to injective nat nat f.
217 intros.apply monotonic_to_injective.
218 apply increasing_to_monotonic.assumption.
219 qed.