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 | (* little endian positive binary numbers. *) |
---|
16 | |
---|
17 | include "basics/logic.ma". |
---|
18 | include "arithmetics/nat.ma". |
---|
19 | |
---|
20 | (* arithmetics/comparison.ma --> *) |
---|
21 | inductive compare : Type[0] ≝ |
---|
22 | | LT : compare |
---|
23 | | EQ : compare |
---|
24 | | GT : compare. |
---|
25 | |
---|
26 | definition compare_invert: compare → compare ≝ |
---|
27 | λc.match c with |
---|
28 | [ LT ⇒ GT |
---|
29 | | EQ ⇒ EQ |
---|
30 | | GT ⇒ LT ]. |
---|
31 | |
---|
32 | (* <-- *) |
---|
33 | |
---|
34 | inductive Pos : Type[0] ≝ |
---|
35 | | one : Pos |
---|
36 | | p1 : Pos → Pos |
---|
37 | | p0 : Pos → Pos. |
---|
38 | |
---|
39 | let rec pred (n:Pos) ≝ |
---|
40 | match n with |
---|
41 | [ one ⇒ one |
---|
42 | | p1 ps ⇒ p0 ps |
---|
43 | | p0 ps ⇒ match ps with [ one ⇒ one | _ ⇒ p1 (pred ps) ] |
---|
44 | ]. |
---|
45 | |
---|
46 | example test : pred (p0 (p0 (p0 one))) = p1 (p1 one). |
---|
47 | //; qed. |
---|
48 | |
---|
49 | let rec succ (n:Pos) ≝ |
---|
50 | match n with |
---|
51 | [ one ⇒ p0 one |
---|
52 | | p0 ps ⇒ p1 ps |
---|
53 | | p1 ps ⇒ p0 (succ ps) |
---|
54 | ]. |
---|
55 | |
---|
56 | lemma succ_elim : ∀P:Pos → Prop. (∀n. P (p0 n)) → (∀n. P (p1 n)) → ∀n. P (succ n). |
---|
57 | #P #H0 #H1 #n cases n; normalize; //; qed. |
---|
58 | |
---|
59 | theorem pred_succ_n : ∀n. n = pred (succ n). |
---|
60 | #n elim n; |
---|
61 | [ 1,3: // |
---|
62 | | #p' normalize; @succ_elim /2/; |
---|
63 | ] qed. |
---|
64 | (* |
---|
65 | theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). |
---|
66 | #n elim n; |
---|
67 | [ #H @False_ind elim H; /2/; |
---|
68 | | //; |
---|
69 | | #n' cases n'; /2/; #n'' #IH #_ <IH normalize; |
---|
70 | *) |
---|
71 | theorem succ_injective: injective Pos Pos succ. |
---|
72 | //; qed. |
---|
73 | |
---|
74 | let rec nat_of_pos (p:Pos) : nat ≝ |
---|
75 | match p with |
---|
76 | [ one ⇒ 1 |
---|
77 | | p0 ps ⇒ 2 * (nat_of_pos ps) |
---|
78 | | p1 ps ⇒ S (2 * (nat_of_pos ps)) |
---|
79 | ]. |
---|
80 | |
---|
81 | let rec succ_pos_of_nat (n:nat) : Pos ≝ |
---|
82 | match n with |
---|
83 | [ O ⇒ one |
---|
84 | | S n' ⇒ succ (succ_pos_of_nat n') |
---|
85 | ]. |
---|
86 | |
---|
87 | theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n). |
---|
88 | //; qed. |
---|
89 | |
---|
90 | theorem succ_pos_of_nat_inj: injective ?? succ_pos_of_nat. |
---|
91 | #n elim n; |
---|
92 | [ #m cases m; |
---|
93 | [ // |
---|
94 | | #m' normalize; @succ_elim #p #H destruct |
---|
95 | ] |
---|
96 | | #n' #IH #m cases m; |
---|
97 | [ normalize; @succ_elim #p #H destruct; |
---|
98 | | normalize; #m' #H >(IH m' ?) //; |
---|
99 | ] |
---|
100 | ] qed. |
---|
101 | |
---|
102 | example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed. |
---|
103 | |
---|
104 | (* Usual induction principle; proof roughly following Coq's, |
---|
105 | apparently due to Conor McBride. *) |
---|
106 | |
---|
107 | inductive possucc : Pos → Prop ≝ |
---|
108 | | psone : possucc one |
---|
109 | | pssucc : ∀n. possucc n → possucc (succ n). |
---|
110 | |
---|
111 | let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝ |
---|
112 | match p return λn',p'.possucc (p0 n') with |
---|
113 | [ psone ⇒ pssucc ? psone |
---|
114 | | pssucc _ p'' ⇒ pssucc ? (pssucc ? (possucc0 ? p'')) |
---|
115 | ]. |
---|
116 | |
---|
117 | let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝ |
---|
118 | match p return λn',p'. possucc (p1 n') with |
---|
119 | [ psone ⇒ pssucc ? (pssucc ? psone) |
---|
120 | | pssucc _ p' ⇒ pssucc ? (pssucc ? (pssucc ? (possucc0 ? p'))) |
---|
121 | ]. |
---|
122 | |
---|
123 | let rec possuccinj (n:Pos) : possucc n ≝ |
---|
124 | match n with |
---|
125 | [ one ⇒ psone |
---|
126 | | p0 ps ⇒ possucc0 ? (possuccinj ps) |
---|
127 | | p1 ps ⇒ possucc1 ? (possuccinj ps) |
---|
128 | ]. |
---|
129 | |
---|
130 | let rec possucc_elim |
---|
131 | (P : Pos → Prop) |
---|
132 | (Pone : P one) |
---|
133 | (Psucc : ∀n. P n → P (succ n)) |
---|
134 | (n : Pos) |
---|
135 | (p:possucc n) on p : P n ≝ |
---|
136 | match p with |
---|
137 | [ psone ⇒ Pone |
---|
138 | | pssucc _ p' ⇒ Psucc ? (possucc_elim P Pone Psucc ? p') |
---|
139 | ]. |
---|
140 | |
---|
141 | definition pos_elim : ∀P:Pos → Prop. P one → (∀n. P n → P (succ n)) → ∀n. P n. |
---|
142 | #P #Pone #Psucc #n @(possucc_elim … (possuccinj n)) /2/; qed. |
---|
143 | |
---|
144 | let rec possucc_cases |
---|
145 | (P : Pos → Prop) |
---|
146 | (Pone : P one) |
---|
147 | (Psucc : ∀n. P (succ n)) |
---|
148 | (n : Pos) |
---|
149 | (p:possucc n) on p : P n ≝ |
---|
150 | match p with |
---|
151 | [ psone ⇒ Pone |
---|
152 | | pssucc _ p' ⇒ Psucc ? |
---|
153 | ]. |
---|
154 | |
---|
155 | definition pos_cases : ∀P:Pos → Prop. P one → (∀n. P (succ n)) → ∀n. P n. |
---|
156 | #P #Pone #Psucc #n @(possucc_cases … (possuccinj n)) /2/; qed. |
---|
157 | |
---|
158 | theorem succ_pred_n : ∀n. n≠one → n = succ (pred n). |
---|
159 | @pos_elim |
---|
160 | [ #H @False_ind elim H; /2/; |
---|
161 | | //; |
---|
162 | ] qed. |
---|
163 | |
---|
164 | theorem not_eq_one_succ : ∀n:Pos. one ≠ succ n. |
---|
165 | #n elim n; normalize; |
---|
166 | [ % #H destruct; |
---|
167 | | 2,3: #n' #H % #H' destruct; |
---|
168 | ] qed. |
---|
169 | |
---|
170 | theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n. |
---|
171 | #n elim n; |
---|
172 | [ //; |
---|
173 | | *: #n' #IH normalize; % #H destruct |
---|
174 | ] qed. |
---|
175 | |
---|
176 | theorem pos_elim2: |
---|
177 | ∀R:Pos → Pos → Prop. |
---|
178 | (∀n:Pos. R one n) |
---|
179 | → (∀n:Pos. R (succ n) one) |
---|
180 | → (∀n,m:Pos. R n m → R (succ n) (succ m)) |
---|
181 | → ∀n,m:Pos. R n m. |
---|
182 | #R #ROn #RSO #RSS @pos_elim //; |
---|
183 | #n0 #Rn0m @pos_elim /2/; qed. |
---|
184 | |
---|
185 | |
---|
186 | theorem decidable_eq_pos: ∀n,m:Pos. decidable (n=m). |
---|
187 | @pos_elim2 #n |
---|
188 | [ @(pos_elim ??? n) /2/; |
---|
189 | | /3/; |
---|
190 | | #m #Hind cases Hind; /3/; |
---|
191 | ] qed. |
---|
192 | |
---|
193 | let rec plus n m ≝ |
---|
194 | match n with |
---|
195 | [ one ⇒ succ m |
---|
196 | | p0 n' ⇒ |
---|
197 | match m with |
---|
198 | [ one ⇒ p1 n' |
---|
199 | | p0 m' ⇒ p0 (plus n' m') |
---|
200 | | p1 m' ⇒ p1 (plus n' m') |
---|
201 | ] |
---|
202 | | p1 n' ⇒ |
---|
203 | match m with |
---|
204 | [ one ⇒ succ n |
---|
205 | | p0 m' ⇒ p1 (plus n' m') |
---|
206 | | p1 m' ⇒ p0 (succ (plus n' m')) |
---|
207 | ] |
---|
208 | ]. |
---|
209 | |
---|
210 | interpretation "positive plus" 'plus x y = (plus x y). |
---|
211 | |
---|
212 | theorem plus_n_succm: ∀n,m. succ (n + m) = n + (succ m). |
---|
213 | #n elim n; normalize; |
---|
214 | [ // |
---|
215 | | 2,3: #n' #IH #m cases m; /3 by eq_f, sym_eq/ |
---|
216 | normalize; cases n' // |
---|
217 | ] qed. |
---|
218 | |
---|
219 | theorem commutative_plus : commutative ? plus. |
---|
220 | #n elim n; |
---|
221 | [ #y cases y; normalize; //; |
---|
222 | | 2,3: #n' #IH #y cases y; normalize; //; |
---|
223 | ] qed. |
---|
224 | |
---|
225 | theorem pluss_succn_m: ∀n,m. succ (n + m) = (succ n) + m. |
---|
226 | #n #m >(commutative_plus (succ n) m) |
---|
227 | <(plus_n_succm …) //; qed. |
---|
228 | |
---|
229 | theorem associative_plus : associative Pos plus. |
---|
230 | @pos_elim |
---|
231 | [ normalize; //; |
---|
232 | | #x' #IHx @pos_elim |
---|
233 | [ #z <(pluss_succn_m …) <(pluss_succn_m …) |
---|
234 | <(pluss_succn_m …) //; |
---|
235 | | #y' #IHy' #z |
---|
236 | <(pluss_succn_m y' …) |
---|
237 | <(plus_n_succm …) |
---|
238 | <(plus_n_succm …) |
---|
239 | <(pluss_succn_m ? z) >(IHy' …) //; |
---|
240 | ] |
---|
241 | ] qed. |
---|
242 | |
---|
243 | theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m). |
---|
244 | @pos_elim normalize; /3/; qed. |
---|
245 | |
---|
246 | theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n). |
---|
247 | /2/; qed. |
---|
248 | |
---|
249 | theorem nat_plus_pos_plus: ∀n,m:nat. succ_pos_of_nat (n+m) = pred (succ_pos_of_nat n + succ_pos_of_nat m). |
---|
250 | #n elim n; |
---|
251 | [ normalize; //; |
---|
252 | | #n' #IH #m normalize; >(IH m) <(pluss_succn_m …) |
---|
253 | <(pred_succ_n ?) <(succ_pred_n …) //; |
---|
254 | elim n'; normalize; /2/; |
---|
255 | ] qed. |
---|
256 | |
---|
257 | let rec times n m ≝ |
---|
258 | match n with |
---|
259 | [ one ⇒ m |
---|
260 | | p0 n' ⇒ p0 (times n' m) |
---|
261 | | p1 n' ⇒ m + p0 (times n' m) |
---|
262 | ]. |
---|
263 | |
---|
264 | interpretation "positive times" 'times x y = (times x y). |
---|
265 | |
---|
266 | lemma p0_times2: ∀n. p0 n = (succ one) * n. |
---|
267 | //; qed. |
---|
268 | |
---|
269 | lemma plus_times2: ∀n. n + n = (succ one) * n. |
---|
270 | #n elim n; |
---|
271 | [ //; |
---|
272 | | 2,3: #n' #IH normalize; >IH //; |
---|
273 | ] qed. |
---|
274 | |
---|
275 | |
---|
276 | theorem times_succn_m: ∀n,m. m+n*m = (succ n)*m. |
---|
277 | #n elim n; |
---|
278 | [ /2/ |
---|
279 | | #n' #IH normalize; #m <(IH m) //; |
---|
280 | | /2/ |
---|
281 | ] qed. |
---|
282 | |
---|
283 | theorem times_n_succm: ∀n,m:Pos. n+(n*m) = n*(succ m). |
---|
284 | @pos_elim |
---|
285 | [ // |
---|
286 | | #n #IH #m <(times_succn_m …) <(times_succn_m …) /3 by succ_injective, trans_eq/ |
---|
287 | ] qed. |
---|
288 | |
---|
289 | theorem times_n_one: ∀n:Pos. n * one = n. |
---|
290 | #n elim n; /3/; qed. |
---|
291 | |
---|
292 | theorem commutative_times: commutative Pos times. |
---|
293 | @pos_elim /2/; qed. |
---|
294 | |
---|
295 | theorem distributive_times_plus : distributive Pos times plus. |
---|
296 | @pos_elim /2/; qed. |
---|
297 | |
---|
298 | theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a. |
---|
299 | //; qed. |
---|
300 | |
---|
301 | theorem associative_times: associative Pos times. |
---|
302 | @pos_elim |
---|
303 | [ //; |
---|
304 | | #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //; |
---|
305 | ] qed. |
---|
306 | |
---|
307 | lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z). |
---|
308 | //; qed. |
---|
309 | |
---|
310 | (*** ordering relations ***) |
---|
311 | |
---|
312 | (* sticking closely to the unary version; not sure if this is a good idea, |
---|
313 | but it means the proofs are much the same. *) |
---|
314 | |
---|
315 | inductive le (n:Pos) : Pos → Prop ≝ |
---|
316 | | le_n : le n n |
---|
317 | | le_S : ∀m:Pos. le n m → le n (succ m). |
---|
318 | |
---|
319 | interpretation "positive 'less than or equal to'" 'leq x y = (le x y). |
---|
320 | interpretation "positive 'neither less than or equal to'" 'nleq x y = (Not (le x y)). |
---|
321 | |
---|
322 | definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m. |
---|
323 | |
---|
324 | interpretation "positive 'less than'" 'lt x y = (lt x y). |
---|
325 | interpretation "positive 'not less than'" 'nless x y = (Not (lt x y)). |
---|
326 | |
---|
327 | definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n. |
---|
328 | |
---|
329 | interpretation "positive 'greater than or equal to'" 'geq x y = (ge x y). |
---|
330 | interpretation "positive 'neither greater than or equal to'" 'ngeq x y = (Not (ge x y)). |
---|
331 | |
---|
332 | definition gt: Pos → Pos → Prop ≝ λn,m. m<n. |
---|
333 | |
---|
334 | interpretation "positive 'greater than'" 'gt x y = (gt x y). |
---|
335 | interpretation "positive 'not greater than'" 'ngtr x y = (Not (gt x y)). |
---|
336 | |
---|
337 | theorem transitive_le: transitive Pos le. |
---|
338 | #a #b #c #leab #lebc elim lebc; /2/; qed. |
---|
339 | |
---|
340 | theorem transitive_lt: transitive Pos lt. |
---|
341 | #a #b #c #ltab #ltbc elim ltbc; /2/; qed. |
---|
342 | |
---|
343 | theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m. |
---|
344 | #n #m #lenm elim lenm; /2/; qed. |
---|
345 | |
---|
346 | theorem le_one_n : ∀n:Pos. one ≤ n. |
---|
347 | @pos_elim /2/; qed. |
---|
348 | |
---|
349 | theorem le_n_succn : ∀n:Pos. n ≤ succ n. |
---|
350 | /2/; qed. |
---|
351 | |
---|
352 | theorem le_pred_n : ∀n:Pos. pred n ≤ n. |
---|
353 | @pos_elim //; qed. |
---|
354 | |
---|
355 | theorem monotonic_pred: monotonic Pos le pred. |
---|
356 | #n #m #lenm elim lenm; /2/;qed. |
---|
357 | |
---|
358 | theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m. |
---|
359 | /2/; qed. |
---|
360 | |
---|
361 | (* lt vs. le *) |
---|
362 | theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one. |
---|
363 | #n % #H inversion H /2/; qed. |
---|
364 | |
---|
365 | theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m. |
---|
366 | #n #m @not_to_not @le_S_S_to_le qed. |
---|
367 | |
---|
368 | theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m. |
---|
369 | #n #m @not_to_not /2/ qed. |
---|
370 | |
---|
371 | theorem decidable_le: ∀n,m:Pos. decidable (n≤m). |
---|
372 | @pos_elim2 #n /2/; |
---|
373 | #m *; /3/; qed. |
---|
374 | |
---|
375 | theorem decidable_lt: ∀n,m:Pos. decidable (n < m). |
---|
376 | #n #m @decidable_le qed. |
---|
377 | |
---|
378 | theorem not_le_succ_n: ∀n:Pos. succ n ≰ n. |
---|
379 | @pos_elim //; |
---|
380 | #m #IH @not_le_to_not_le_succ_succ //; |
---|
381 | qed. |
---|
382 | |
---|
383 | theorem not_le_to_lt: ∀n,m:Pos. n ≰ m → m < n. |
---|
384 | @pos_elim2 #n |
---|
385 | [#abs @False_ind /2/; |
---|
386 | |/2/; |
---|
387 | |#m #Hind #HnotleSS @le_succ_succ /3/; |
---|
388 | ] |
---|
389 | qed. |
---|
390 | |
---|
391 | theorem lt_to_not_le: ∀n,m:Pos. n < m → m ≰ n. |
---|
392 | #n #m #Hltnm elim Hltnm; |
---|
393 | [ // |
---|
394 | | #p #H @not_to_not /2/; |
---|
395 | ] qed. |
---|
396 | |
---|
397 | theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n. |
---|
398 | /4/; qed. |
---|
399 | |
---|
400 | |
---|
401 | theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n. |
---|
402 | #n #m #H @lt_to_not_le /2/;qed. |
---|
403 | |
---|
404 | (* lt and le trans *) |
---|
405 | |
---|
406 | theorem lt_to_le_to_lt: ∀n,m,p:Pos. n < m → m ≤ p → n < p. |
---|
407 | #n #m #p #H #H1 elim H1; /2/; qed. |
---|
408 | |
---|
409 | theorem le_to_lt_to_lt: ∀n,m,p:Pos. n ≤ m → m < p → n < p. |
---|
410 | #n #m #p #H elim H; /3/; qed. |
---|
411 | |
---|
412 | theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m. |
---|
413 | /2/; qed. |
---|
414 | |
---|
415 | theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m. |
---|
416 | /2/; qed. |
---|
417 | |
---|
418 | theorem lt_one_n_elim: ∀n:Pos. one < n → |
---|
419 | ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n. |
---|
420 | @pos_elim //; #abs @False_ind /2/; |
---|
421 | qed. |
---|
422 | |
---|
423 | (* le to lt or eq *) |
---|
424 | theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m. |
---|
425 | #n #m #lenm elim lenm; /3/; qed. |
---|
426 | |
---|
427 | (* not eq *) |
---|
428 | theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m. |
---|
429 | #n #m #H @not_to_not /2/; qed. |
---|
430 | |
---|
431 | theorem not_eq_to_le_to_lt: ∀n,m:Pos. n≠m → n≤m → n<m. |
---|
432 | #n #m #Hneq #Hle cases (le_to_or_lt_eq ?? Hle); //; |
---|
433 | #Heq /3/; qed. |
---|
434 | |
---|
435 | (* le elimination *) |
---|
436 | theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n. |
---|
437 | @pos_cases //; #a ; #abs |
---|
438 | @False_ind /2/;qed. |
---|
439 | |
---|
440 | theorem le_n_one_elim: ∀n:Pos. n ≤ one → ∀P: Pos →Prop. P one → P n. |
---|
441 | @pos_cases //; #a #abs |
---|
442 | @False_ind /2/; qed. |
---|
443 | |
---|
444 | theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m → |
---|
445 | ∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P. |
---|
446 | #n #m #Hle #P elim Hle; /3/; qed. |
---|
447 | |
---|
448 | (* le and eq *) |
---|
449 | |
---|
450 | theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m. |
---|
451 | @pos_elim2 /4 by le_n_one_to_eq, monotonic_pred, eq_f, sym_eq/ |
---|
452 | qed. |
---|
453 | |
---|
454 | theorem lt_one_S : ∀n:Pos. one < succ n. |
---|
455 | /2/; qed. |
---|
456 | |
---|
457 | (* well founded induction principles *) |
---|
458 | |
---|
459 | theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop. |
---|
460 | (∀m.(∀p. p < m → P p) → P m) → P n. |
---|
461 | #n #P #H |
---|
462 | cut (∀q:Pos. q ≤ n → P q);/2/; |
---|
463 | @(pos_elim … n) |
---|
464 | [#q #HleO (* applica male *) |
---|
465 | @(le_n_one_elim ? HleO) |
---|
466 | @H #p #ltpO |
---|
467 | @False_ind /2/; (* 3 *) |
---|
468 | |#p #Hind #q #HleS |
---|
469 | @H #a #lta @Hind |
---|
470 | @le_S_S_to_le /2/; |
---|
471 | ] |
---|
472 | qed. |
---|
473 | |
---|
474 | (*********************** monotonicity ***************************) |
---|
475 | theorem monotonic_le_plus_r: |
---|
476 | ∀n:Pos.monotonic Pos le (λm.n + m). |
---|
477 | #n #a #b @(pos_elim … n) normalize; /2/; |
---|
478 | #m #H #leab /3/; qed. |
---|
479 | |
---|
480 | theorem monotonic_le_plus_l: |
---|
481 | ∀m:Pos.monotonic Pos le (λn.n + m). |
---|
482 | /2/; qed. |
---|
483 | |
---|
484 | theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2 → m1 ≤ m2 |
---|
485 | → n1 + m1 ≤ n2 + m2. |
---|
486 | #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2)) |
---|
487 | /2/; qed. |
---|
488 | |
---|
489 | theorem le_plus_n :∀n,m:Pos. m ≤ n + m. |
---|
490 | /3/; qed. |
---|
491 | |
---|
492 | lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m. |
---|
493 | /2/; qed. |
---|
494 | |
---|
495 | lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m. |
---|
496 | /2/; qed. |
---|
497 | |
---|
498 | theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n. |
---|
499 | /2/; qed. |
---|
500 | |
---|
501 | theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n. |
---|
502 | //; qed. |
---|
503 | |
---|
504 | theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m. |
---|
505 | @pos_elim normalize; /3/; qed. |
---|
506 | |
---|
507 | theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m. |
---|
508 | /2/; qed. |
---|
509 | |
---|
510 | (* plus & lt *) |
---|
511 | |
---|
512 | theorem monotonic_lt_plus_r: |
---|
513 | ∀n:Pos.monotonic Pos lt (λm.n+m). |
---|
514 | /2/; qed. |
---|
515 | |
---|
516 | theorem monotonic_lt_plus_l: |
---|
517 | ∀n:Pos.monotonic Pos lt (λm.m+n). |
---|
518 | /2/; qed. |
---|
519 | |
---|
520 | theorem lt_plus: ∀n,m,p,q:Pos. n < m → p < q → n + p < m + q. |
---|
521 | #n #m #p #q #ltnm #ltpq |
---|
522 | @(transitive_lt ? (n+q)) /2/; qed. |
---|
523 | |
---|
524 | theorem le_lt_plus_pos: ∀n,m,p:Pos. n ≤ m → n < m + p. |
---|
525 | #n #m #p #H @(le_to_lt_to_lt … H) |
---|
526 | /2/; qed. |
---|
527 | |
---|
528 | theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q. |
---|
529 | /2/; qed. |
---|
530 | |
---|
531 | theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q. |
---|
532 | /2/; qed. |
---|
533 | |
---|
534 | (* times *) |
---|
535 | theorem monotonic_le_times_r: |
---|
536 | ∀n:Pos.monotonic Pos le (λm. n * m). |
---|
537 | #n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*) |
---|
538 | #a #lea /2/; |
---|
539 | qed. |
---|
540 | |
---|
541 | theorem le_times: ∀n1,n2,m1,m2:Pos. |
---|
542 | n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2. |
---|
543 | #n1 #n2 #m1 #m2 #len #lem |
---|
544 | @(transitive_le ? (n1*m2)) (* /2/ slow *) |
---|
545 | [ @monotonic_le_times_r //; |
---|
546 | | applyS monotonic_le_times_r;//; |
---|
547 | ] |
---|
548 | qed. |
---|
549 | |
---|
550 | theorem lt_times_n: ∀n,m:Pos. m ≤ n*m. |
---|
551 | #n #m /2/; qed. |
---|
552 | |
---|
553 | theorem le_times_to_le: |
---|
554 | ∀a,n,m:Pos. a * n ≤ a * m → n ≤ m. |
---|
555 | #a @pos_elim2 normalize; |
---|
556 | [//; |
---|
557 | |#n >(times_n_one …) <(times_n_succm …) |
---|
558 | #H @False_ind |
---|
559 | elim (lt_to_not_le ?? (le_lt_plus_pos a a (a*n) …)); /2/; |
---|
560 | |#n #m #H #le |
---|
561 | @le_succ_succ @H /2/; |
---|
562 | ] |
---|
563 | qed. |
---|
564 | |
---|
565 | theorem le_S_times_2: ∀n,m:Pos. n ≤ m → succ n ≤ (succ one)*m. |
---|
566 | #n #m #lenm (* interessante *) |
---|
567 | applyS (le_plus n m); //; qed. |
---|
568 | |
---|
569 | (* prove injectivity of times from above *) |
---|
570 | theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m). |
---|
571 | #n #m #p #H @le_to_le_to_eq |
---|
572 | /2/; |
---|
573 | qed. |
---|
574 | |
---|
575 | theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n). |
---|
576 | /2/; qed. |
---|
577 | |
---|
578 | (* times & lt *) |
---|
579 | |
---|
580 | theorem monotonic_lt_times_l: |
---|
581 | ∀c:Pos. monotonic Pos lt (λt.(t*c)). |
---|
582 | #c #n #m #ltnm |
---|
583 | elim ltnm; normalize; |
---|
584 | [/2/; |
---|
585 | |#a #_ #lt1 @(transitive_le ??? lt1) //; |
---|
586 | ] |
---|
587 | qed. |
---|
588 | |
---|
589 | theorem monotonic_lt_times_r: |
---|
590 | ∀c:Pos. monotonic Pos lt (λt.(c*t)). |
---|
591 | #a #b #c #H |
---|
592 | >(commutative_times a b) >(commutative_times a c) |
---|
593 | /2/; qed. |
---|
594 | |
---|
595 | theorem lt_to_le_to_lt_times: |
---|
596 | ∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q. |
---|
597 | #n #m #p #q #ltnm #lepq |
---|
598 | @(le_to_lt_to_lt ? (n*q)) |
---|
599 | [@monotonic_le_times_r //; |
---|
600 | |@monotonic_lt_times_l //; |
---|
601 | ] |
---|
602 | qed. |
---|
603 | |
---|
604 | theorem lt_times:∀n,m,p,q:Pos. n<m → p<q → n*p < m*q. |
---|
605 | #n #m #p #q #ltnm #ltpq |
---|
606 | @lt_to_le_to_lt_times /2/; |
---|
607 | qed. |
---|
608 | |
---|
609 | theorem lt_times_n_to_lt_l: |
---|
610 | ∀n,p,q:Pos. p*n < q*n → p < q. |
---|
611 | #n #p #q #Hlt |
---|
612 | elim (decidable_lt p q);//; |
---|
613 | #nltpq @False_ind |
---|
614 | @(absurd ? ? (lt_to_not_le ? ? Hlt)) |
---|
615 | applyS monotonic_le_times_r;/2/; |
---|
616 | qed. |
---|
617 | |
---|
618 | theorem lt_times_n_to_lt_r: |
---|
619 | ∀n,p,q:Pos. n*p < n*q → p < q. |
---|
620 | /2/; qed. |
---|
621 | |
---|
622 | (**** minus ****) |
---|
623 | |
---|
624 | inductive minusresult : Type[0] ≝ |
---|
625 | | MinusNeg: minusresult |
---|
626 | | MinusZero: minusresult |
---|
627 | | MinusPos: Pos → minusresult. |
---|
628 | |
---|
629 | let rec partial_minus (n,m:Pos) : minusresult ≝ |
---|
630 | match n with |
---|
631 | [ one ⇒ match m with [ one ⇒ MinusZero | _ ⇒ MinusNeg ] |
---|
632 | | p0 n' ⇒ |
---|
633 | match m with |
---|
634 | [ one ⇒ MinusPos (pred n) |
---|
635 | | p0 m' ⇒ match partial_minus n' m' with |
---|
636 | [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ] |
---|
637 | | p1 m' ⇒ match partial_minus n' m' with |
---|
638 | [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusNeg | MinusPos p ⇒ MinusPos (pred (p0 p)) ] |
---|
639 | ] |
---|
640 | | p1 n' ⇒ |
---|
641 | match m with |
---|
642 | [ one ⇒ MinusPos (p0 n') |
---|
643 | | p0 m' ⇒ match partial_minus n' m' with |
---|
644 | [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusPos one | MinusPos p ⇒ MinusPos (p1 p) ] |
---|
645 | | p1 m' ⇒ match partial_minus n' m' with |
---|
646 | [ MinusNeg ⇒ MinusNeg | MinusZero ⇒ MinusZero | MinusPos p ⇒ MinusPos (p0 p) ] |
---|
647 | ] |
---|
648 | ]. |
---|
649 | |
---|
650 | example testminus0: partial_minus (p0 one) (p1 one) = MinusNeg. //; qed. |
---|
651 | example testminus1: partial_minus (p0 one) (p0 (p0 one)) = MinusNeg. //; qed. |
---|
652 | example testminus2: partial_minus (p0 (p0 one)) (p0 one) = MinusPos (p0 one). //; qed. |
---|
653 | example testminus3: partial_minus (p0 one) one = MinusPos one. //; qed. |
---|
654 | example testminus4: partial_minus (succ (p1 one)) (p1 one) = MinusPos one. //; qed. |
---|
655 | |
---|
656 | definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ]. |
---|
657 | |
---|
658 | interpretation "positive minus" 'minus x y = (minus x y). |
---|
659 | |
---|
660 | lemma partialminus_S: ∀n,m:Pos. |
---|
661 | match partial_minus (succ n) m with |
---|
662 | [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n m = MinusZero | _ ⇒ partial_minus n m = MinusPos (pred p) ] |
---|
663 | | _ ⇒ partial_minus n m = MinusNeg |
---|
664 | ]. |
---|
665 | #n elim n; |
---|
666 | [ #m cases m; |
---|
667 | [ //; |
---|
668 | | 2,3: #m' cases m'; //; |
---|
669 | ] |
---|
670 | (* The other two cases are the same. I'd combine them, but the numbering |
---|
671 | would be even more horrific. *) |
---|
672 | | #n' #IH #m cases m; |
---|
673 | [ normalize; <(pred_succ_n n') cases n'; //; |
---|
674 | | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); |
---|
675 | [ 1,2,4,5: normalize; #H >H //; |
---|
676 | | 3,6: #p cases p; [ 1,4: normalize; #H >H //; |
---|
677 | | 2,3,5,6: #p' normalize; #H >H //; |
---|
678 | ] |
---|
679 | ] |
---|
680 | ] |
---|
681 | | #n' #IH #m cases m; |
---|
682 | [ normalize; <(pred_succ_n n') cases n'; //; |
---|
683 | | 2,3: #m' normalize; lapply (IH m'); cases (partial_minus (succ n') m'); |
---|
684 | [ 1,2,4,5: normalize; #H >H //; |
---|
685 | | 3,6: #p cases p; [ 1,4: normalize; #H >H //; |
---|
686 | | 2,3,5,6: #p' normalize; #H >H //; |
---|
687 | ] |
---|
688 | ] |
---|
689 | ] |
---|
690 | ] qed. |
---|
691 | |
---|
692 | lemma partialminus_n_S: ∀n,m:Pos. |
---|
693 | match partial_minus n m with |
---|
694 | [ MinusPos p ⇒ match p with [ one ⇒ partial_minus n (succ m) = MinusZero |
---|
695 | | _ ⇒ partial_minus n (succ m) = MinusPos (pred p) |
---|
696 | ] |
---|
697 | | _ ⇒ partial_minus n (succ m) = MinusNeg |
---|
698 | ]. |
---|
699 | #n elim n; |
---|
700 | [ #m cases m; //; |
---|
701 | (* Again, lots of unnecessary duplication! *) |
---|
702 | | #n' #IH #m cases m; |
---|
703 | [ normalize; cases n'; //; |
---|
704 | | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); |
---|
705 | [ 1,2: normalize; #H >H //; |
---|
706 | | #p cases p; normalize; [ #H >H //; |
---|
707 | | 2,3: #p' #H >H //; |
---|
708 | ] |
---|
709 | ] |
---|
710 | | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); |
---|
711 | [ 1,2: normalize; #H >H //; |
---|
712 | | #p cases p; normalize; [ #H >H //; |
---|
713 | | 2,3: #p' #H >H //; |
---|
714 | ] |
---|
715 | ] |
---|
716 | ] |
---|
717 | | #n' #IH #m cases m; |
---|
718 | [ normalize; cases n'; //; |
---|
719 | | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); |
---|
720 | [ 1,2: normalize; #H >H //; |
---|
721 | | #p cases p; normalize; [ #H >H //; |
---|
722 | | 2,3: #p' #H >H //; |
---|
723 | ] |
---|
724 | ] |
---|
725 | | #m' normalize; lapply (IH m'); cases (partial_minus n' m'); |
---|
726 | [ 1,2: normalize; #H >H //; |
---|
727 | | #p cases p; normalize; [ #H >H //; |
---|
728 | | 2,3: #p' #H >H //; |
---|
729 | ] |
---|
730 | ] |
---|
731 | ] |
---|
732 | ] qed. |
---|
733 | |
---|
734 | theorem partialminus_S_S: ∀n,m:Pos. partial_minus (succ n) (succ m) = partial_minus n m. |
---|
735 | #n elim n; |
---|
736 | [ #m cases m; |
---|
737 | [ //; |
---|
738 | | 2,3: #m' cases m'; //; |
---|
739 | ] |
---|
740 | | #n' #IH #m cases m; |
---|
741 | [ normalize; cases n'; /2/; normalize; #n'' <(pred_succ_n n'') cases n'';//; |
---|
742 | | #m' normalize; >(IH ?) //; |
---|
743 | | #m' normalize; lapply (partialminus_S n' m'); cases (partial_minus (succ n') m'); |
---|
744 | [ 1,2: normalize; #H >H //; |
---|
745 | | #p cases p; [ normalize; #H >H //; |
---|
746 | | 2,3: #p' normalize; #H >H //; |
---|
747 | ] |
---|
748 | ] |
---|
749 | ] |
---|
750 | | #n' #IH #m cases m; |
---|
751 | [ normalize; cases n'; /2/; |
---|
752 | | #m' normalize; lapply (partialminus_n_S n' m'); cases (partial_minus n' m'); |
---|
753 | [ 1,2: normalize; #H >H //; |
---|
754 | | #p cases p; [ normalize; #H >H //; |
---|
755 | | 2,3: #p' normalize; #H >H //; |
---|
756 | ] |
---|
757 | ] |
---|
758 | | #m' normalize; >(IH ?) //; |
---|
759 | ] |
---|
760 | ] qed. |
---|
761 | |
---|
762 | theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m. |
---|
763 | #n #m normalize; >(partialminus_S_S n m) //; qed. |
---|
764 | |
---|
765 | theorem minus_one_n: ∀n:Pos.one=one-n. |
---|
766 | #n cases n; //; qed. |
---|
767 | |
---|
768 | theorem minus_n_one: ∀n:Pos.pred n=n-one. |
---|
769 | #n cases n; //; qed. |
---|
770 | |
---|
771 | lemma partial_minus_n_n: ∀n. partial_minus n n = MinusZero. |
---|
772 | #n elim n; |
---|
773 | [ //; |
---|
774 | | 2,3: normalize; #n' #IH >IH // |
---|
775 | ] qed. |
---|
776 | |
---|
777 | theorem minus_n_n: ∀n:Pos.one=n-n. |
---|
778 | #n normalize; >(partial_minus_n_n n) //; |
---|
779 | qed. |
---|
780 | |
---|
781 | theorem minus_Sn_n: ∀n:Pos. one = (succ n)-n. |
---|
782 | #n cut (partial_minus (succ n) n = MinusPos one); |
---|
783 | [ elim n; |
---|
784 | [ //; |
---|
785 | | normalize; #n' #IH >IH //; |
---|
786 | | normalize; #n' #IH >(partial_minus_n_n n') //; |
---|
787 | ] |
---|
788 | | #H normalize; >H //; |
---|
789 | ] qed. |
---|
790 | |
---|
791 | theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m). |
---|
792 | (* qualcosa da capire qui |
---|
793 | #n #m #lenm elim lenm; napplyS refl_eq. *) |
---|
794 | @pos_elim2 |
---|
795 | [#n #H @(lt_one_n_elim n H) //; |
---|
796 | |#n #abs @False_ind /2/ |
---|
797 | |#n #m #Hind #c applyS Hind; /2/; |
---|
798 | ] |
---|
799 | qed. |
---|
800 | |
---|
801 | theorem not_eq_to_le_to_le_minus: |
---|
802 | ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one. |
---|
803 | #n @pos_cases //; #m |
---|
804 | #H #H1 @le_S_S_to_le |
---|
805 | applyS (not_eq_to_le_to_lt n (succ m) H H1); |
---|
806 | qed. |
---|
807 | |
---|
808 | theorem eq_minus_S_pred: ∀n,m:Pos. n - (succ m) = pred(n -m). |
---|
809 | @pos_elim2 |
---|
810 | [ #n cases n; normalize; //; |
---|
811 | | #n @(pos_elim … n) //; |
---|
812 | | //; |
---|
813 | ] qed. |
---|
814 | |
---|
815 | lemma pred_Sn_plus: ∀n,m:Pos. one < n → (pred n)+m = pred (n+m). |
---|
816 | #n #m #H |
---|
817 | @(lt_one_n_elim … H) /3/; |
---|
818 | qed. |
---|
819 | |
---|
820 | theorem plus_minus: |
---|
821 | ∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m. |
---|
822 | @pos_elim2 |
---|
823 | [ #n #p #H <(minus_n_one ?) <(minus_n_one ?) /2/; |
---|
824 | |#n #p #abs @False_ind /2/; |
---|
825 | |#n #m #IH #p #H >(eq_minus_S_pred …) >(eq_minus_S_pred …) |
---|
826 | cut (n<m); [ /2/ ] #H' |
---|
827 | >(pred_Sn_plus …) |
---|
828 | [ >(minus_Sn_m …) /2/; |
---|
829 | <(pluss_succn_m …) |
---|
830 | <(pluss_succn_m …) |
---|
831 | >(minus_Sn_m …) |
---|
832 | [ <(pred_succ_n …) |
---|
833 | <(pred_succ_n …) |
---|
834 | @IH /2/; |
---|
835 | | /2/; |
---|
836 | ] |
---|
837 | | >(minus_Sn_m … H') //; |
---|
838 | ] |
---|
839 | ] qed. |
---|
840 | |
---|
841 | (* XXX: putting this in the appropriate case screws up auto?! *) |
---|
842 | theorem succ_plus_one: ∀n. succ n = n + one. |
---|
843 | #n elim n; //; qed. |
---|
844 | |
---|
845 | theorem nat_possucc: ∀p. nat_of_pos (succ p) = S (nat_of_pos p). |
---|
846 | #p elim p; normalize; |
---|
847 | [ //; |
---|
848 | | #q #IH <(plus_n_O …) <(plus_n_O …) |
---|
849 | >IH <(plus_n_Sm …) //; |
---|
850 | | //; |
---|
851 | ] qed. |
---|
852 | |
---|
853 | theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. |
---|
854 | #n elim n; //; qed. |
---|
855 | |
---|
856 | theorem minus_plus_m_m: ∀n,m:Pos.n = (n+m)-m. |
---|
857 | #n @pos_elim |
---|
858 | [ //; |
---|
859 | | #m #IH <(plus_n_succm …) |
---|
860 | >(eq_minus_S_pred …) |
---|
861 | >(minus_Sn_m …) /2/; |
---|
862 | ] qed. |
---|
863 | |
---|
864 | theorem plus_minus_m_m: ∀n,m:Pos. |
---|
865 | m < n → n = (n-m)+m. |
---|
866 | #n #m #lemn applyS sym_eq; |
---|
867 | applyS (plus_minus m n m); //; qed. |
---|
868 | |
---|
869 | theorem le_plus_minus_m_m: ∀n,m:Pos. n ≤ (n-m)+m. |
---|
870 | @pos_elim |
---|
871 | [// |
---|
872 | |#a #Hind @pos_cases //; |
---|
873 | #n |
---|
874 | >(minus_S_S …) |
---|
875 | /2/; |
---|
876 | ] |
---|
877 | qed. |
---|
878 | |
---|
879 | theorem minus_to_plus :∀n,m,p:Pos. |
---|
880 | m < n → n-m = p → n = m+p. |
---|
881 | #n #m #p #lemn #eqp applyS plus_minus_m_m; //; |
---|
882 | qed. |
---|
883 | |
---|
884 | theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p. |
---|
885 | (* /4/ done in 43.5 *) |
---|
886 | #n #m #p #eqp |
---|
887 | @sym_eq |
---|
888 | applyS (minus_plus_m_m p m); |
---|
889 | qed. |
---|
890 | |
---|
891 | theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m → |
---|
892 | pred n - pred m = n - m. |
---|
893 | #n #m #posn #posm |
---|
894 | @(lt_one_n_elim n posn) |
---|
895 | @(lt_one_n_elim m posm) //. |
---|
896 | qed. |
---|
897 | |
---|
898 | (* monotonicity and galois *) |
---|
899 | |
---|
900 | theorem monotonic_le_minus_l: |
---|
901 | ∀p,q,n:Pos. q ≤ p → q-n ≤ p-n. |
---|
902 | @pos_elim2 #p #q |
---|
903 | [#lePO @(le_n_one_elim ? lePO) //; |
---|
904 | |//; |
---|
905 | |#Hind @pos_cases |
---|
906 | [/2/; |
---|
907 | |#a #leSS >(minus_S_S …) >(minus_S_S …) @Hind /2/; |
---|
908 | ] |
---|
909 | ] |
---|
910 | qed. |
---|
911 | |
---|
912 | theorem le_minus_to_plus: ∀n,m,p:Pos. n-m ≤ p → n≤ p+m. |
---|
913 | #n #m #p #lep |
---|
914 | @transitive_le |
---|
915 | [|@le_plus_minus_m_m |
---|
916 | |@monotonic_le_plus_l //; |
---|
917 | ] |
---|
918 | qed. |
---|
919 | |
---|
920 | theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p. |
---|
921 | #n #m #p #lep |
---|
922 | (* bello *) |
---|
923 | applyS monotonic_le_minus_l;//; |
---|
924 | (* /2/; *) |
---|
925 | qed. |
---|
926 | |
---|
927 | theorem monotonic_le_minus_r: |
---|
928 | ∀p,q,n:Pos. q ≤ p → n-p ≤ n-q. |
---|
929 | #p #q #n #lepq |
---|
930 | @le_plus_to_minus |
---|
931 | @(transitive_le ??? (le_plus_minus_m_m ? q)) /2/; |
---|
932 | qed. |
---|
933 | |
---|
934 | (*********************** boolean arithmetics ********************) |
---|
935 | include "basics/bool.ma". |
---|
936 | |
---|
937 | let rec eqb n m ≝ |
---|
938 | match n with |
---|
939 | [ one ⇒ match m with [ one ⇒ true | _ ⇒ false] |
---|
940 | | p0 p ⇒ match m with [ p0 q ⇒ eqb p q | _ ⇒ false] |
---|
941 | | p1 p ⇒ match m with [ p1 q ⇒ eqb p q | _ ⇒ false] |
---|
942 | ]. |
---|
943 | |
---|
944 | theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Type[0]. |
---|
945 | (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). |
---|
946 | #n elim n; |
---|
947 | [ #m cases m normalize |
---|
948 | [ /2/ |
---|
949 | | 2,3: #m' #P #t #f @f % #H destruct |
---|
950 | ] |
---|
951 | | #n' #IH #m cases m normalize |
---|
952 | [ #P #t #f @f % #H destruct |
---|
953 | | #m' #P #t #f @IH |
---|
954 | [ /2/ |
---|
955 | | * #ne @f % #e @ne destruct @refl |
---|
956 | ] |
---|
957 | | #m' #P #t #f @f % #H destruct; |
---|
958 | ] |
---|
959 | | #n' #IH #m cases m; normalize; |
---|
960 | [ #P #t #f @f % #H destruct; |
---|
961 | | #m' #P #t #f @f % #H destruct; |
---|
962 | | #m' #P #t #f @IH |
---|
963 | [ /2/; |
---|
964 | | * #ne @f % #e @ne destruct @refl |
---|
965 | ] |
---|
966 | ] |
---|
967 | ] qed. |
---|
968 | |
---|
969 | theorem eqb_n_n: ∀n:Pos. eqb n n = true. |
---|
970 | #n elim n; normalize; //. |
---|
971 | qed. |
---|
972 | |
---|
973 | theorem eqb_true_to_eq: ∀n,m:Pos. eqb n m = true → n = m. |
---|
974 | #n #m @(eqb_elim n m) //; |
---|
975 | #_ #abs @False_ind /2/; |
---|
976 | qed. |
---|
977 | |
---|
978 | theorem eqb_false_to_not_eq: ∀n,m:Pos. eqb n m = false → n ≠ m. |
---|
979 | #n #m @(eqb_elim n m) /2/; |
---|
980 | qed. |
---|
981 | |
---|
982 | theorem eq_to_eqb_true: ∀n,m:Pos. |
---|
983 | n = m → eqb n m = true. |
---|
984 | //; qed. |
---|
985 | |
---|
986 | theorem not_eq_to_eqb_false: ∀n,m:Pos. |
---|
987 | n ≠ m → eqb n m = false. |
---|
988 | #n #m #noteq |
---|
989 | @eqb_elim //; |
---|
990 | #Heq @False_ind /2/; |
---|
991 | qed. |
---|
992 | |
---|
993 | let rec leb n m ≝ |
---|
994 | match partial_minus n m with |
---|
995 | [ MinusNeg ⇒ true |
---|
996 | | MinusZero ⇒ true |
---|
997 | | MinusPos _ ⇒ false |
---|
998 | ]. |
---|
999 | |
---|
1000 | lemma leb_unfold_hack: ∀n,m:Pos. leb n m = |
---|
1001 | match partial_minus n m with |
---|
1002 | [ MinusNeg ⇒ true |
---|
1003 | | MinusZero ⇒ true |
---|
1004 | | MinusPos _ ⇒ false |
---|
1005 | ]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed. |
---|
1006 | |
---|
1007 | theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop. |
---|
1008 | (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). |
---|
1009 | @pos_elim2 |
---|
1010 | [ #n cases n; normalize; /2/; |
---|
1011 | | #n cases n; normalize; |
---|
1012 | [ /2/; |
---|
1013 | | 2,3: #m' #P #t #f @f /2/; % #H inversion H; |
---|
1014 | [ #H' destruct; |
---|
1015 | | #p /2/; |
---|
1016 | ] |
---|
1017 | ] |
---|
1018 | | #n #m #IH #P #t #f >(leb_unfold_hack …) |
---|
1019 | >(partialminus_S_S n m) |
---|
1020 | <(leb_unfold_hack …) |
---|
1021 | @IH #H /3/; |
---|
1022 | ] qed. |
---|
1023 | |
---|
1024 | theorem leb_true_to_le:∀n,m:Pos.leb n m = true → n ≤ m. |
---|
1025 | #n #m @leb_elim |
---|
1026 | [//; |
---|
1027 | |#_ #abs @False_ind /2/; |
---|
1028 | ] |
---|
1029 | qed. |
---|
1030 | |
---|
1031 | theorem leb_false_to_not_le:∀n,m:Pos. |
---|
1032 | leb n m = false → n ≰ m. |
---|
1033 | #n #m @leb_elim |
---|
1034 | [#_ #abs @False_ind /2/; |
---|
1035 | |//; |
---|
1036 | ] |
---|
1037 | qed. |
---|
1038 | |
---|
1039 | theorem le_to_leb_true: ∀n,m:Pos. n ≤ m → leb n m = true. |
---|
1040 | #n #m @leb_elim //; |
---|
1041 | #H #H1 @False_ind /2/; |
---|
1042 | qed. |
---|
1043 | |
---|
1044 | theorem not_le_to_leb_false: ∀n,m:Pos. n ≰ m → leb n m = false. |
---|
1045 | #n #m @leb_elim //; |
---|
1046 | #H #H1 @False_ind /2/; |
---|
1047 | qed. |
---|
1048 | |
---|
1049 | theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false. |
---|
1050 | /3/; qed. |
---|
1051 | |
---|
1052 | |
---|
1053 | (***** comparison *****) |
---|
1054 | |
---|
1055 | definition pos_compare : Pos → Pos → compare ≝ |
---|
1056 | λn,m.match partial_minus n m with |
---|
1057 | [ MinusNeg ⇒ LT |
---|
1058 | | MinusZero ⇒ EQ |
---|
1059 | | MinusPos _ ⇒ GT |
---|
1060 | ]. |
---|
1061 | |
---|
1062 | theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ. |
---|
1063 | #n normalize; >(partial_minus_n_n n) |
---|
1064 | //; qed. |
---|
1065 | |
---|
1066 | theorem pos_compare_S_S: ∀n,m:Pos.pos_compare n m = pos_compare (succ n) (succ m). |
---|
1067 | #n #m normalize; |
---|
1068 | >(partialminus_S_S …) |
---|
1069 | //; |
---|
1070 | qed. |
---|
1071 | |
---|
1072 | theorem pos_compare_pred_pred: |
---|
1073 | ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m). |
---|
1074 | #n #m #Hn #Hm |
---|
1075 | @(lt_one_n_elim n Hn) |
---|
1076 | @(lt_one_n_elim m Hm) |
---|
1077 | #p #q <(pred_succ_n ?) <(pred_succ_n ?) |
---|
1078 | <(pos_compare_S_S …) //; |
---|
1079 | qed. |
---|
1080 | |
---|
1081 | theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT. |
---|
1082 | #n elim n; //; qed. |
---|
1083 | |
---|
1084 | theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT. |
---|
1085 | #n elim n; //; qed. |
---|
1086 | |
---|
1087 | theorem pos_compare_to_Prop: |
---|
1088 | ∀n,m.match (pos_compare n m) with |
---|
1089 | [ LT ⇒ n < m |
---|
1090 | | EQ ⇒ n = m |
---|
1091 | | GT ⇒ m < n ]. |
---|
1092 | #n #m |
---|
1093 | @(pos_elim2 (λn,m.match (pos_compare n m) with |
---|
1094 | [ LT ⇒ n < m |
---|
1095 | | EQ ⇒ n = m |
---|
1096 | | GT ⇒ m < n ])) |
---|
1097 | [1,2:@pos_cases |
---|
1098 | [ 1,3: /2/; |
---|
1099 | | 2,4: #m' cases m'; //; |
---|
1100 | ] |
---|
1101 | |#n1 #m1 <pos_compare_S_S cases (pos_compare n1 m1) |
---|
1102 | [1,3: #IH @le_succ_succ // |
---|
1103 | | #IH >IH // |
---|
1104 | ] |
---|
1105 | ] |
---|
1106 | qed. |
---|
1107 | |
---|
1108 | theorem pos_compare_n_m_m_n: |
---|
1109 | ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n). |
---|
1110 | #n #m |
---|
1111 | @(pos_elim2 (λn,m. pos_compare n m = compare_invert (pos_compare m n))) |
---|
1112 | [1,2:#n1 cases n1;/2/; |
---|
1113 | |#n1 #m1 |
---|
1114 | <(pos_compare_S_S …) |
---|
1115 | <(pos_compare_S_S …) |
---|
1116 | #IH normalize @IH] |
---|
1117 | qed. |
---|
1118 | |
---|
1119 | theorem pos_compare_elim : |
---|
1120 | ∀n,m:Pos. ∀P:compare → Prop. |
---|
1121 | (n < m → P LT) → (n=m → P EQ) → (m < n → P GT) → P (pos_compare n m). |
---|
1122 | #n #m #P #Hlt #Heq #Hgt |
---|
1123 | cut (match (pos_compare n m) with |
---|
1124 | [ LT ⇒ n < m |
---|
1125 | | EQ ⇒ n=m |
---|
1126 | | GT ⇒ m < n] → |
---|
1127 | P (pos_compare n m)) |
---|
1128 | [cases (pos_compare n m); |
---|
1129 | [@Hlt |
---|
1130 | |@Heq |
---|
1131 | |@Hgt] |
---|
1132 | |#Hcut @Hcut //; |
---|
1133 | qed. |
---|
1134 | |
---|
1135 | inductive cmp_cases (n,m:Pos) : CProp[0] ≝ |
---|
1136 | | cmp_le : n ≤ m → cmp_cases n m |
---|
1137 | | cmp_gt : m < n → cmp_cases n m. |
---|
1138 | |
---|
1139 | theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. |
---|
1140 | /2/; qed. |
---|
1141 | |
---|
1142 | lemma cmp_nat: ∀n,m:Pos.cmp_cases n m. |
---|
1143 | #n #m lapply (pos_compare_to_Prop n m) |
---|
1144 | cases (pos_compare n m);normalize; /3 by lt_times_n_to_lt_l, le_n, cmp_le, cmp_gt, lt_to_le/ |
---|
1145 | qed. |
---|
1146 | |
---|
1147 | |
---|
1148 | |
---|
1149 | |
---|
1150 | let rec two_power_nat (n:nat) : Pos ≝ |
---|
1151 | match n with |
---|
1152 | [ O ⇒ one |
---|
1153 | | S n' ⇒ p0 (two_power_nat n') |
---|
1154 | ]. |
---|
1155 | |
---|
1156 | definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p). |
---|
1157 | |
---|
1158 | |
---|
1159 | |
---|
1160 | definition max : Pos → Pos → Pos ≝ |
---|
1161 | λn,m. match leb n m with [ true ⇒ m | _ ⇒ n]. |
---|
1162 | |
---|
1163 | |
---|
1164 | |
---|
1165 | lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. |
---|
1166 | #n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m); |
---|
1167 | [ //; |
---|
1168 | | 2,3: #H @False_ind @(absurd ? lt ?) /3/; |
---|
1169 | ] qed. |
---|
1170 | |
---|
1171 | lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
1172 | #n #m @eqb_elim //; qed. |
---|