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