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 (**************************************************************************)
16 theorem inj_S : \forall n,m:nat.(S n)=(S m) \to n=m.
19 theorem plus_Sn_m: ∀n,m:nat. S (n + m) = S n + m.
22 theorem plus_Sn_m1: ∀n,m:nat. S m + n = n + S m.
23 #n (elim n) normalize // qed.
27 theorem plus_n_1 : ∀n:nat. S n = n+1.
30 theorem inj_plus_r: \forall p,n,m:nat. p+n = p+m \to n=m
31 \def injective_plus_r.
33 theorem injective_plus_l: ∀m:nat.injective nat nat (λn.n+m).
36 theorem inj_plus_l: \forall p,n,m:nat. n+p = m+p \to n=m
37 \def injective_plus_l.
39 variant sym_times : \forall n,m:nat. n*m = m*n \def
42 theorem times_O_to_O: ∀n,m:nat.n*m=O → n=O ∨ m=O.
44 #n #m #H normalize #H1 napply False_ind napply not_eq_O_S
47 theorem times_n_SO : ∀n:nat. n = n * S O.
50 theorem times_SSO_n : ∀n:nat. n + n = (S(S O)) * n.
53 nlemma times_SSO: \forall n.(S(S O))*(S n) = S(S((S(S O))*n)).
56 theorem or_eq_eq_S: \forall n.\exists m.
57 n = (S(S O))*m \lor n = S ((S(S O))*m).
60 ##|#a #H nelim H #b#ornelim or#aeq
66 lemma eq_lt: ∀n,m. (n < m) = (S n ≤ m).
69 theorem trans_le: \forall n,m,p:nat. n \leq m \to m \leq p \to n \leq p
72 theorem trans_lt: \forall n,m,p:nat. lt n m \to lt m p \to lt n p
75 (* this are instances of the le versions *)
76 theorem lt_S_S_to_lt: ∀n,m. S n < S m → n < m.
79 theorem lt_to_lt_S_S: ∀n,m. n < m → S n < S m.
82 (* this is le_S_S_to_le *)
83 theorem lt_S_to_le: ∀n,m:nat. n < S m → n ≤ m.
86 theorem lt_SO_n_to_lt_O_pred_n: \forall n:nat.
87 (S O) \lt n \to O \lt (pred n).
89 apply (ltn_to_ltO (pred (S O)) (pred n) ?).
90 apply (lt_pred (S O) n)
96 theorem lt_pred: \forall n,m.
97 O < n \to n < m \to pred n < pred m.
99 [intros.apply False_ind.apply (not_le_Sn_O ? H)
100 |intros.apply False_ind.apply (not_le_Sn_O ? H1)
101 |intros.simplify.unfold.apply le_S_S_to_le.assumption
105 theorem le_pred_to_le:
106 ∀n,m. O < m → pred n ≤ pred m → n ≤ m.
119 theorem eq_to_not_lt: ∀a,b:nat. a = b → a ≮ b.
124 apply (lt_to_not_eq b b)
130 theorem lt_n_m_to_not_lt_m_Sn: ∀n,m. n < m → m ≮ S n.
136 generalize in match (le_S_S ? ? H)
138 generalize in match (transitive_le ? ? ? H2 H1)
140 apply (not_le_Sn_n ? H3).
143 (* other abstract properties *)
144 theorem antisymmetric_le : antisymmetric nat le.
145 unfold antisymmetric.intros 2.
146 apply (nat_elim2 (\lambda n,m.(n \leq m \to m \leq n \to n=m))).
147 intros.apply le_n_O_to_eq.assumption.
148 intros.apply False_ind.apply (not_le_Sn_O ? H).
149 intros.apply eq_f.apply H.
150 apply le_S_S_to_le.assumption.
151 apply le_S_S_to_le.assumption.
154 theorem antisym_le: \forall n,m:nat. n \leq m \to m \leq n \to n=m
155 \def antisymmetric_le.
157 theorem le_n_m_to_lt_m_Sn_to_eq_n_m: ∀n,m. n ≤ m → m < S n → n=m.
160 generalize in match (le_S_S_to_le ? ? H1)
166 theorem le_plus_r: ∀p,n,m:nat. n ≤ m → p + n ≤ p + m
167 ≝ monotonic_le_plus_r.
169 theorem le_plus_l: \forall p,n,m:nat. n \le m \to n + p \le m + p
170 \def monotonic_le_plus_l.
172 variant lt_plus_r: \forall n,p,q:nat. p < q \to n + p < n + q \def
175 variant lt_plus_l: \forall n,p,q:nat. p < q \to p + n < q + n \def
178 theorem le_to_lt_to_lt_plus: ∀a,b,c,d:nat.
179 a ≤ c → b < d → a + b < c+d.
180 (* bello /2/ un po' lento *)
181 #a #b #c #d #leac #lebd
182 normalize napplyS le_plus // qed.
184 theorem le_times_r: \forall p,n,m:nat. n \le m \to p*n \le p*m
185 \def monotonic_le_times_r.
187 theorem monotonic_le_times_l:
188 ∀m:nat.monotonic nat le (λn.n*m).
191 theorem le_times_l: \forall p,n,m:nat. n \le m \to n*p \le m*p
192 \def monotonic_le_times_l.
194 theorem le_S_times_2: ∀n,m.O < m → n ≤ m → S n ≤ 2*m.
195 #n #m #posm #lenm (* interessante *)
196 applyS (le_plus n m) // qed.
198 theorem lt_O_times_S_S: ∀n,m:nat.O < (S n)*(S m).
199 intros.simplify.unfold lt.apply le_S_S.apply le_O_n.
202 theorem lt_times_eq_O: \forall a,b:nat.
203 O < a → a * b = O → b = O.
210 rewrite > (S_pred a) in H1
212 apply (eq_to_not_lt O ((S (pred a))*(S m)))
215 | apply lt_O_times_S_S
222 theorem O_lt_times_to_O_lt: \forall a,c:nat.
223 O \lt (a * c) \to O \lt a.
235 lemma lt_times_to_lt_O: \forall i,n,m:nat. i < n*m \to O < m.
237 elim (le_to_or_lt_eq O ? (le_O_n m))
241 rewrite < times_n_O in H.
242 apply (not_le_Sn_O ? H)
246 theorem monotonic_lt_times_r:
247 ∀n:nat.monotonic nat lt (λm.(S n)*m).
251 simplify.rewrite < plus_n_O.rewrite < plus_n_O.assumption.
252 apply lt_plus.assumption.assumption.
255 theorem nat_compare_times_l : \forall n,p,q:nat.
256 nat_compare p q = nat_compare ((S n) * p) ((S n) * q).
257 intros.apply nat_compare_elim.intro.
258 apply nat_compare_elim.
261 apply (inj_times_r n).assumption.
262 apply lt_to_not_eq. assumption.
264 apply (lt_times_to_lt_r n).assumption.
265 apply le_to_not_lt.apply lt_to_le.assumption.
266 intro.rewrite < H.rewrite > nat_compare_n_n.reflexivity.
267 intro.apply nat_compare_elim.intro.
269 apply (lt_times_to_lt_r n).assumption.
270 apply le_to_not_lt.apply lt_to_le.assumption.
273 apply (inj_times_r n).assumption.
274 apply lt_to_not_eq.assumption.
278 theorem lt_times_plus_times: \forall a,b,n,m:nat.
279 a < n \to b < m \to a*m + b < n*m.
282 [intros.apply False_ind.apply (not_le_Sn_O ? H)
286 change with (S b+a*m1 \leq m1+m*m1).
290 [apply le_S_S_to_le.assumption
297 theorem not_eq_to_le_to_le_minus:
298 ∀n,m.n ≠ m → n ≤ m → n ≤ m - 1.
299 #n * #m (cases m// #m normalize
300 #H #H1 napply le_S_S_to_le
301 napplyS (not_eq_to_le_to_lt n (S m) H H1)
304 theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
305 intros.elim H.elim (minus_Sn_n n).apply le_n.
306 rewrite > minus_Sn_m.
307 apply le_S.assumption.
308 apply lt_to_le.assumption.
311 theorem minus_le_S_minus_S: \forall n,m:nat. m-n \leq S (m-(S n)).
313 apply (nat_elim2 (\lambda n,m.m-n \leq S (m-(S n)))).
314 intro.elim n1.simplify.apply le_n_Sn.
315 simplify.rewrite < minus_n_O.apply le_n.
316 intros.simplify.apply le_n_Sn.
317 intros.simplify.apply H.
320 theorem lt_minus_S_n_to_le_minus_n : \forall n,m,p:nat. m-(S n) < p \to m-n \leq p.
323 (* end auto($Revision: 9739 $) proof: TIME=1.33 SIZE=100 DEPTH=100 *)
324 apply (trans_le (m-n) (S (m-(S n))) p).
325 apply minus_le_S_minus_S.
329 theorem le_minus_m: \forall n,m:nat. n-m \leq n.
330 intros.apply (nat_elim2 (\lambda m,n. n-m \leq n)).
331 intros.rewrite < minus_n_O.apply le_n.
332 intros.simplify.apply le_n.
333 intros.simplify.apply le_S.assumption.
336 theorem lt_minus_m: \forall n,m:nat. O < n \to O < m \to n-m \lt n.
337 intros.apply (lt_O_n_elim n H).intro.
338 apply (lt_O_n_elim m H1).intro.
339 simplify.unfold lt.apply le_S_S.apply le_minus_m.
342 theorem minus_le_O_to_le: \forall n,m:nat. n-m \leq O \to n \leq m.
344 apply (nat_elim2 (\lambda n,m:nat.n-m \leq O \to n \leq m)).
346 simplify.intros. assumption.
347 simplify.intros.apply le_S_S.apply H.assumption.
350 theorem plus_minus: ∀n,m,p. p ≤ m → (n+m)-p = n +(m-p).
351 #n #m #p #lepm @plus_to_minus >(commutative_plus p)
352 >associative_plus <plus_minus_m_m //
355 (* serve anche ltb? *)
356 ndefinition ltb ≝λn,m. leb (S n) m.
358 theorem ltb_elim: ∀n,m:nat. ∀P:bool → Prop.
359 (n < m → P true) → (n ≮ m → P false) → P (ltb n m).
361 napply leb_elim /3/ qed.
363 theorem ltb_true_to_lt:∀n,m.ltb n m = true → n < m.
364 #n #m #Hltb napply leb_true_to_le nassumption
367 theorem ltb_false_to_not_lt:∀n,m.
368 ltb n m = false → n ≮ m.
369 #n #m #Hltb napply leb_false_to_not_le nassumption
372 theorem lt_to_ltb_true: ∀n,m. n < m → ltb n m = true.
373 #n #m #Hltb napply le_to_leb_true nassumption
376 theorem le_to_ltb_false: ∀n,m. m \le n → ltb n m = false.
377 #n #m #Hltb napply lt_to_leb_false /2/