[10] | 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 | |
---|
[487] | 17 | include "basics/logic.ma". |
---|
[10] | 18 | include "arithmetics/nat.ma". |
---|
| 19 | |
---|
[487] | 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] ≝ |
---|
[10] | 35 | | one : Pos |
---|
| 36 | | p1 : Pos → Pos |
---|
| 37 | | p0 : Pos → Pos. |
---|
| 38 | |
---|
[487] | 39 | let rec pred (n:Pos) ≝ |
---|
[10] | 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 | |
---|
[487] | 46 | example test : pred (p0 (p0 (p0 one))) = p1 (p1 one). |
---|
| 47 | //; qed. |
---|
[10] | 48 | |
---|
[487] | 49 | let rec succ (n:Pos) ≝ |
---|
[10] | 50 | match n with |
---|
| 51 | [ one ⇒ p0 one |
---|
| 52 | | p0 ps ⇒ p1 ps |
---|
| 53 | | p1 ps ⇒ p0 (succ ps) |
---|
| 54 | ]. |
---|
| 55 | |
---|
[487] | 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. |
---|
[10] | 58 | |
---|
[487] | 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. |
---|
[10] | 64 | (* |
---|
[487] | 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; |
---|
[10] | 70 | *) |
---|
[487] | 71 | theorem succ_injective: injective Pos Pos succ. |
---|
| 72 | //; qed. |
---|
[10] | 73 | |
---|
[487] | 74 | let rec nat_of_pos (p:Pos) : nat ≝ |
---|
[10] | 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 | |
---|
[487] | 81 | let rec succ_pos_of_nat (n:nat) : Pos ≝ |
---|
[10] | 82 | match n with |
---|
| 83 | [ O ⇒ one |
---|
| 84 | | S n' ⇒ succ (succ_pos_of_nat n') |
---|
| 85 | ]. |
---|
| 86 | |
---|
[487] | 87 | theorem succ_nat_pos: ∀n:nat. succ_pos_of_nat (S n) = succ (succ_pos_of_nat n). |
---|
| 88 | //; qed. |
---|
[10] | 89 | |
---|
[487] | 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. |
---|
[10] | 101 | |
---|
[487] | 102 | example test2 : nat_of_pos (p0 (p1 one)) = 6. //; qed. |
---|
[10] | 103 | |
---|
| 104 | (* Usual induction principle; proof roughly following Coq's, |
---|
| 105 | apparently due to Conor McBride. *) |
---|
| 106 | |
---|
[487] | 107 | inductive possucc : Pos → Prop ≝ |
---|
[10] | 108 | | psone : possucc one |
---|
| 109 | | pssucc : ∀n. possucc n → possucc (succ n). |
---|
| 110 | |
---|
[487] | 111 | let rec possucc0 (n:Pos) (p:possucc n) on p : possucc (p0 n) ≝ |
---|
[10] | 112 | match p return λn',p'.possucc (p0 n') with |
---|
| 113 | [ psone ⇒ pssucc ? psone |
---|
| 114 | | pssucc _ p'' ⇒ pssucc ? (pssucc ? (possucc0 ? p'')) |
---|
| 115 | ]. |
---|
| 116 | |
---|
[487] | 117 | let rec possucc1 (n:Pos) (p:possucc n) on p : possucc (p1 n) ≝ |
---|
[10] | 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 | |
---|
[487] | 123 | let rec possuccinj (n:Pos) : possucc n ≝ |
---|
[10] | 124 | match n with |
---|
| 125 | [ one ⇒ psone |
---|
| 126 | | p0 ps ⇒ possucc0 ? (possuccinj ps) |
---|
| 127 | | p1 ps ⇒ possucc1 ? (possuccinj ps) |
---|
| 128 | ]. |
---|
| 129 | |
---|
[487] | 130 | let rec possucc_elim |
---|
[10] | 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 | |
---|
[487] | 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. |
---|
[10] | 143 | |
---|
[487] | 144 | let rec possucc_cases |
---|
[10] | 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 | |
---|
[487] | 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. |
---|
[10] | 157 | |
---|
[487] | 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. |
---|
[10] | 163 | |
---|
[487] | 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. |
---|
[10] | 169 | |
---|
[487] | 170 | theorem not_eq_n_succn: ∀n:Pos. n ≠ succ n. |
---|
| 171 | #n elim n; |
---|
| 172 | [ //; |
---|
| 173 | | *: #n' #IH normalize; % #H destruct |
---|
| 174 | ] qed. |
---|
[10] | 175 | |
---|
[487] | 176 | theorem pos_elim2: |
---|
[10] | 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. |
---|
[487] | 182 | #R #ROn #RSO #RSS @pos_elim //; |
---|
| 183 | #n0 #Rn0m @pos_elim /2/; qed. |
---|
[10] | 184 | |
---|
| 185 | |
---|
[487] | 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. |
---|
[10] | 192 | |
---|
[487] | 193 | let rec plus n m ≝ |
---|
[10] | 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 | |
---|
[487] | 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/; |
---|
| 216 | normalize; cases n'; //; |
---|
| 217 | ] qed. |
---|
[10] | 218 | |
---|
[487] | 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. |
---|
[10] | 224 | |
---|
[487] | 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. |
---|
[10] | 228 | |
---|
[487] | 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. |
---|
[10] | 242 | |
---|
[487] | 243 | theorem injective_plus_r: ∀n:Pos.injective Pos Pos (λm.n+m). |
---|
| 244 | @pos_elim normalize; /3/; qed. |
---|
[10] | 245 | |
---|
[487] | 246 | theorem injective_plus_l: ∀n:Pos.injective Pos Pos (λm.m+n). |
---|
| 247 | /2/; qed. |
---|
[10] | 248 | |
---|
[487] | 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. |
---|
[10] | 256 | |
---|
[487] | 257 | let rec times n m ≝ |
---|
[10] | 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 | |
---|
[487] | 266 | lemma p0_times2: ∀n. p0 n = (succ one) * n. |
---|
| 267 | //; qed. |
---|
[10] | 268 | |
---|
[487] | 269 | lemma plus_times2: ∀n. n + n = (succ one) * n. |
---|
| 270 | #n elim n; |
---|
| 271 | [ //; |
---|
| 272 | | 2,3: #n' #IH normalize; >IH //; |
---|
| 273 | ] qed. |
---|
[10] | 274 | |
---|
| 275 | |
---|
[487] | 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. |
---|
[10] | 282 | |
---|
[487] | 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/; |
---|
| 287 | ] qed. |
---|
[10] | 288 | |
---|
[487] | 289 | theorem times_n_one: ∀n:Pos. n * one = n. |
---|
| 290 | #n elim n; /3/; qed. |
---|
[10] | 291 | |
---|
[487] | 292 | theorem commutative_times: commutative Pos times. |
---|
| 293 | @pos_elim /2/; qed. |
---|
[10] | 294 | |
---|
[487] | 295 | theorem distributive_times_plus : distributive Pos times plus. |
---|
| 296 | @pos_elim /2/; qed. |
---|
[10] | 297 | |
---|
[487] | 298 | theorem distributive_times_plus_r: ∀a,b,c:Pos. (b+c)*a = b*a + c*a. |
---|
| 299 | //; qed. |
---|
[10] | 300 | |
---|
[487] | 301 | theorem associative_times: associative Pos times. |
---|
| 302 | @pos_elim |
---|
| 303 | [ //; |
---|
| 304 | | #x #IH #y #z <(times_succn_m …) <(times_succn_m …) //; |
---|
| 305 | ] qed. |
---|
[10] | 306 | |
---|
[487] | 307 | lemma times_times: ∀x,y,z:Pos. x*(y*z) = y*(x*z). |
---|
| 308 | //; qed. |
---|
[10] | 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 | |
---|
[487] | 315 | inductive le (n:Pos) : Pos → Prop ≝ |
---|
[10] | 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 | |
---|
[487] | 322 | definition lt: Pos → Pos → Prop ≝ λn,m. succ n ≤ m. |
---|
[10] | 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 | |
---|
[487] | 327 | definition ge: Pos → Pos → Prop ≝ λn,m:Pos. m ≤ n. |
---|
[10] | 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 | |
---|
[487] | 332 | definition gt: Pos → Pos → Prop ≝ λn,m. m<n. |
---|
[10] | 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 | |
---|
[487] | 337 | theorem transitive_le: transitive Pos le. |
---|
| 338 | #a #b #c #leab #lebc elim lebc; /2/; qed. |
---|
[10] | 339 | |
---|
[487] | 340 | theorem transitive_lt: transitive Pos lt. |
---|
| 341 | #a #b #c #ltab #ltbc elim ltbc; /2/; qed. |
---|
[10] | 342 | |
---|
[487] | 343 | theorem le_succ_succ: ∀n,m:Pos. n ≤ m → succ n ≤ succ m. |
---|
| 344 | #n #m #lenm elim lenm; /2/; qed. |
---|
[10] | 345 | |
---|
[487] | 346 | theorem le_one_n : ∀n:Pos. one ≤ n. |
---|
| 347 | @pos_elim /2/; qed. |
---|
[10] | 348 | |
---|
[487] | 349 | theorem le_n_succn : ∀n:Pos. n ≤ succ n. |
---|
| 350 | /2/; qed. |
---|
[10] | 351 | |
---|
[487] | 352 | theorem le_pred_n : ∀n:Pos. pred n ≤ n. |
---|
| 353 | @pos_elim //; qed. |
---|
[10] | 354 | |
---|
[487] | 355 | theorem monotonic_pred: monotonic Pos le pred. |
---|
| 356 | #n #m #lenm elim lenm; /2/;qed. |
---|
[10] | 357 | |
---|
[487] | 358 | theorem le_S_S_to_le: ∀n,m:Pos. succ n ≤ succ m → n ≤ m. |
---|
| 359 | /2/; qed. |
---|
[10] | 360 | |
---|
| 361 | (* lt vs. le *) |
---|
[487] | 362 | theorem not_le_succ_one: ∀ n:Pos. succ n ≰ one. |
---|
| 363 | #n % #H inversion H /2/; qed. |
---|
[10] | 364 | |
---|
[487] | 365 | theorem not_le_to_not_le_succ_succ: ∀ n,m:Pos. n ≰ m → succ n ≰ succ m. |
---|
[697] | 366 | #n #m @not_to_not @le_S_S_to_le qed. |
---|
[10] | 367 | |
---|
[487] | 368 | theorem not_le_succ_succ_to_not_le: ∀ n,m:Pos. succ n ≰ succ m → n ≰ m. |
---|
[697] | 369 | #n #m @not_to_not /2/ qed. |
---|
[10] | 370 | |
---|
[487] | 371 | theorem decidable_le: ∀n,m:Pos. decidable (n≤m). |
---|
| 372 | @pos_elim2 #n /2/; |
---|
| 373 | #m *; /3/; qed. |
---|
[10] | 374 | |
---|
[487] | 375 | theorem decidable_lt: ∀n,m:Pos. decidable (n < m). |
---|
| 376 | #n #m @decidable_le qed. |
---|
[10] | 377 | |
---|
[487] | 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. |
---|
[10] | 382 | |
---|
[487] | 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. |
---|
[10] | 390 | |
---|
[487] | 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. |
---|
[10] | 396 | |
---|
[487] | 397 | theorem not_lt_to_le: ∀n,m:Pos. n ≮ m → m ≤ n. |
---|
| 398 | /4/; qed. |
---|
[10] | 399 | |
---|
| 400 | |
---|
[487] | 401 | theorem le_to_not_lt: ∀n,m:Pos. n ≤ m → m ≮ n. |
---|
| 402 | #n #m #H @lt_to_not_le /2/;qed. |
---|
[10] | 403 | |
---|
| 404 | (* lt and le trans *) |
---|
| 405 | |
---|
[487] | 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. |
---|
[10] | 408 | |
---|
[487] | 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. |
---|
[10] | 411 | |
---|
[487] | 412 | theorem lt_succ_to_lt: ∀n,m:Pos. succ n < m → n < m. |
---|
| 413 | /2/; qed. |
---|
[10] | 414 | |
---|
[487] | 415 | theorem ltn_to_lt_one: ∀n,m:Pos. n < m → one < m. |
---|
| 416 | /2/; qed. |
---|
[10] | 417 | |
---|
[487] | 418 | theorem lt_one_n_elim: ∀n:Pos. one < n → |
---|
[10] | 419 | ∀P:Pos → Prop.(∀m:Pos.P (succ m)) → P n. |
---|
[487] | 420 | @pos_elim //; #abs @False_ind /2/; |
---|
| 421 | qed. |
---|
[10] | 422 | |
---|
| 423 | (* le to lt or eq *) |
---|
[487] | 424 | theorem le_to_or_lt_eq: ∀n,m:Pos. n ≤ m → n < m ∨ n = m. |
---|
| 425 | #n #m #lenm elim lenm; /3/; qed. |
---|
[10] | 426 | |
---|
| 427 | (* not eq *) |
---|
[487] | 428 | theorem lt_to_not_eq : ∀n,m:Pos. n < m → n ≠ m. |
---|
| 429 | #n #m #H @not_to_not /2/; qed. |
---|
[10] | 430 | |
---|
[487] | 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. |
---|
[10] | 434 | |
---|
| 435 | (* le elimination *) |
---|
[487] | 436 | theorem le_n_one_to_eq : ∀n:Pos. n ≤ one → one=n. |
---|
| 437 | @pos_cases //; #a ; #abs |
---|
| 438 | @False_ind /2/;qed. |
---|
[10] | 439 | |
---|
[487] | 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. |
---|
[10] | 443 | |
---|
[487] | 444 | theorem le_n_Sm_elim : ∀n,m:Pos.n ≤ succ m → |
---|
[10] | 445 | ∀P:Prop. (succ n ≤ succ m → P) → (n=succ m → P) → P. |
---|
[487] | 446 | #n #m #Hle #P elim Hle; /3/; qed. |
---|
[10] | 447 | |
---|
| 448 | (* le and eq *) |
---|
| 449 | |
---|
[487] | 450 | theorem le_to_le_to_eq: ∀n,m:Pos. n ≤ m → m ≤ n → n = m. |
---|
| 451 | @pos_elim2 /4/; |
---|
| 452 | qed. |
---|
[10] | 453 | |
---|
[487] | 454 | theorem lt_one_S : ∀n:Pos. one < succ n. |
---|
| 455 | /2/; qed. |
---|
[10] | 456 | |
---|
| 457 | (* well founded induction principles *) |
---|
| 458 | |
---|
[487] | 459 | theorem pos_elim1 : ∀n:Pos.∀P:Pos → Prop. |
---|
[10] | 460 | (∀m.(∀p. p < m → P p) → P m) → P n. |
---|
[487] | 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. |
---|
[10] | 473 | |
---|
| 474 | (*********************** monotonicity ***************************) |
---|
[487] | 475 | theorem monotonic_le_plus_r: |
---|
[10] | 476 | ∀n:Pos.monotonic Pos le (λm.n + m). |
---|
[487] | 477 | #n #a #b @(pos_elim … n) normalize; /2/; |
---|
| 478 | #m #H #leab /3/; qed. |
---|
[10] | 479 | |
---|
[487] | 480 | theorem monotonic_le_plus_l: |
---|
[10] | 481 | ∀m:Pos.monotonic Pos le (λn.n + m). |
---|
[487] | 482 | /2/; qed. |
---|
[10] | 483 | |
---|
[487] | 484 | theorem le_plus: ∀n1,n2,m1,m2:Pos. n1 ≤ n2 → m1 ≤ m2 |
---|
[10] | 485 | → n1 + m1 ≤ n2 + m2. |
---|
[487] | 486 | #n1 #n2 #m1 #m2 #len #lem @(transitive_le ? (n1+m2)) |
---|
| 487 | /2/; qed. |
---|
[10] | 488 | |
---|
[487] | 489 | theorem le_plus_n :∀n,m:Pos. m ≤ n + m. |
---|
| 490 | /3/; qed. |
---|
[10] | 491 | |
---|
[487] | 492 | lemma le_plus_a: ∀a,n,m:Pos. n ≤ m → n ≤ a + m. |
---|
| 493 | /2/; qed. |
---|
[10] | 494 | |
---|
[487] | 495 | lemma le_plus_b: ∀b,n,m:Pos. n + b ≤ m → n ≤ m. |
---|
| 496 | /2/; qed. |
---|
[10] | 497 | |
---|
[487] | 498 | theorem le_plus_n_r :∀n,m:Pos. m ≤ m + n. |
---|
| 499 | /2/; qed. |
---|
[10] | 500 | |
---|
[487] | 501 | theorem eq_plus_to_le: ∀n,m,p:Pos.n=m+p → m ≤ n. |
---|
| 502 | //; qed. |
---|
[10] | 503 | |
---|
[487] | 504 | theorem le_plus_to_le: ∀a,n,m:Pos. a + n ≤ a + m → n ≤ m. |
---|
| 505 | @pos_elim normalize; /3/; qed. |
---|
[10] | 506 | |
---|
[487] | 507 | theorem le_plus_to_le_r: ∀a,n,m:Pos. n + a ≤ m +a → n ≤ m. |
---|
| 508 | /2/; qed. |
---|
[10] | 509 | |
---|
| 510 | (* plus & lt *) |
---|
| 511 | |
---|
[487] | 512 | theorem monotonic_lt_plus_r: |
---|
[10] | 513 | ∀n:Pos.monotonic Pos lt (λm.n+m). |
---|
[487] | 514 | /2/; qed. |
---|
[10] | 515 | |
---|
[487] | 516 | theorem monotonic_lt_plus_l: |
---|
[10] | 517 | ∀n:Pos.monotonic Pos lt (λm.m+n). |
---|
[487] | 518 | /2/; qed. |
---|
[10] | 519 | |
---|
[487] | 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. |
---|
[10] | 523 | |
---|
[487] | 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. |
---|
[10] | 527 | |
---|
[487] | 528 | theorem lt_plus_to_lt_l :∀n,p,q:Pos. p+n < q+n → p<q. |
---|
| 529 | /2/; qed. |
---|
[10] | 530 | |
---|
[487] | 531 | theorem lt_plus_to_lt_r :∀n,p,q:Pos. n+p < n+q → p<q. |
---|
| 532 | /2/; qed. |
---|
[10] | 533 | |
---|
| 534 | (* times *) |
---|
[487] | 535 | theorem monotonic_le_times_r: |
---|
[10] | 536 | ∀n:Pos.monotonic Pos le (λm. n * m). |
---|
[487] | 537 | #n #x #y #lexy @(pos_elim … n) normalize;//;(* lento /2/;*) |
---|
| 538 | #a #lea /2/; |
---|
| 539 | qed. |
---|
[10] | 540 | |
---|
[487] | 541 | theorem le_times: ∀n1,n2,m1,m2:Pos. |
---|
[10] | 542 | n1 ≤ n2 → m1 ≤ m2 → n1*m1 ≤ n2*m2. |
---|
[487] | 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. |
---|
[10] | 549 | |
---|
[487] | 550 | theorem lt_times_n: ∀n,m:Pos. m ≤ n*m. |
---|
| 551 | #n #m /2/; qed. |
---|
[10] | 552 | |
---|
[487] | 553 | theorem le_times_to_le: |
---|
[10] | 554 | ∀a,n,m:Pos. a * n ≤ a * m → n ≤ m. |
---|
[487] | 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. |
---|
[10] | 564 | |
---|
[487] | 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. |
---|
[10] | 568 | |
---|
| 569 | (* prove injectivity of times from above *) |
---|
[487] | 570 | theorem injective_times_r: ∀n:Pos.injective Pos Pos (λm.n*m). |
---|
| 571 | #n #m #p #H @le_to_le_to_eq |
---|
[10] | 572 | /2/; |
---|
[487] | 573 | qed. |
---|
[10] | 574 | |
---|
[487] | 575 | theorem injective_times_l: ∀n:Pos.injective Pos Pos (λm.m*n). |
---|
| 576 | /2/; qed. |
---|
[10] | 577 | |
---|
| 578 | (* times & lt *) |
---|
| 579 | |
---|
[487] | 580 | theorem monotonic_lt_times_l: |
---|
[10] | 581 | ∀c:Pos. monotonic Pos lt (λt.(t*c)). |
---|
[487] | 582 | #c #n #m #ltnm |
---|
| 583 | elim ltnm; normalize; |
---|
| 584 | [/2/; |
---|
| 585 | |#a #_ #lt1 @(transitive_le ??? lt1) //; |
---|
| 586 | ] |
---|
| 587 | qed. |
---|
[10] | 588 | |
---|
[487] | 589 | theorem monotonic_lt_times_r: |
---|
[10] | 590 | ∀c:Pos. monotonic Pos lt (λt.(c*t)). |
---|
[487] | 591 | #a #b #c #H |
---|
| 592 | >(commutative_times a b) >(commutative_times a c) |
---|
| 593 | /2/; qed. |
---|
[10] | 594 | |
---|
[487] | 595 | theorem lt_to_le_to_lt_times: |
---|
[10] | 596 | ∀n,m,p,q:Pos. n < m → p ≤ q → n*p < m*q. |
---|
[487] | 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. |
---|
[10] | 603 | |
---|
[487] | 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. |
---|
[10] | 608 | |
---|
[487] | 609 | theorem lt_times_n_to_lt_l: |
---|
[10] | 610 | ∀n,p,q:Pos. p*n < q*n → p < q. |
---|
[487] | 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. |
---|
[10] | 617 | |
---|
[487] | 618 | theorem lt_times_n_to_lt_r: |
---|
[10] | 619 | ∀n,p,q:Pos. n*p < n*q → p < q. |
---|
[487] | 620 | /2/; qed. |
---|
[10] | 621 | |
---|
| 622 | (**** minus ****) |
---|
| 623 | |
---|
[487] | 624 | inductive minusresult : Type[0] ≝ |
---|
[10] | 625 | | MinusNeg: minusresult |
---|
| 626 | | MinusZero: minusresult |
---|
| 627 | | MinusPos: Pos → minusresult. |
---|
| 628 | |
---|
[487] | 629 | let rec partial_minus (n,m:Pos) : minusresult ≝ |
---|
[10] | 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 | |
---|
[487] | 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. |
---|
[10] | 655 | |
---|
[487] | 656 | definition minus ≝ λn,m. match partial_minus n m with [ MinusPos p ⇒ p | _ ⇒ one ]. |
---|
[10] | 657 | |
---|
| 658 | interpretation "natural minus" 'minus x y = (minus x y). |
---|
| 659 | |
---|
[487] | 660 | lemma partialminus_S: ∀n,m:Pos. |
---|
[10] | 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 | ]. |
---|
[487] | 665 | #n elim n; |
---|
| 666 | [ #m cases m; |
---|
| 667 | [ //; |
---|
| 668 | | 2,3: #m' cases m'; //; |
---|
| 669 | ] |
---|
[10] | 670 | (* The other two cases are the same. I'd combine them, but the numbering |
---|
| 671 | would be even more horrific. *) |
---|
[487] | 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. |
---|
[10] | 691 | |
---|
[487] | 692 | lemma partialminus_n_S: ∀n,m:Pos. |
---|
[10] | 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 | ]. |
---|
[487] | 699 | #n elim n; |
---|
| 700 | [ #m cases m; //; |
---|
[10] | 701 | (* Again, lots of unnecessary duplication! *) |
---|
[487] | 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. |
---|
[10] | 733 | |
---|
[487] | 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. |
---|
[10] | 761 | |
---|
[487] | 762 | theorem minus_S_S: ∀n,m:Pos. (succ n) - (succ m) = n-m. |
---|
| 763 | #n #m normalize; >(partialminus_S_S n m) //; qed. |
---|
[10] | 764 | |
---|
[487] | 765 | theorem minus_one_n: ∀n:Pos.one=one-n. |
---|
| 766 | #n cases n; //; qed. |
---|
[10] | 767 | |
---|
[487] | 768 | theorem minus_n_one: ∀n:Pos.pred n=n-one. |
---|
| 769 | #n cases n; //; qed. |
---|
[10] | 770 | |
---|
[487] | 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. |
---|
[10] | 776 | |
---|
[487] | 777 | theorem minus_n_n: ∀n:Pos.one=n-n. |
---|
| 778 | #n normalize; >(partial_minus_n_n n) //; |
---|
| 779 | qed. |
---|
[10] | 780 | |
---|
[487] | 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. |
---|
[10] | 790 | |
---|
[487] | 791 | theorem minus_Sn_m: ∀m,n:Pos. m < n → succ n -m = succ (n-m). |
---|
[10] | 792 | (* qualcosa da capire qui |
---|
[487] | 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. |
---|
[10] | 800 | |
---|
[487] | 801 | theorem not_eq_to_le_to_le_minus: |
---|
[10] | 802 | ∀n,m:Pos.n ≠ m → n ≤ m → n ≤ m - one. |
---|
[487] | 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. |
---|
[10] | 807 | |
---|
[487] | 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. |
---|
[10] | 814 | |
---|
[487] | 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. |
---|
[10] | 819 | |
---|
[487] | 820 | theorem plus_minus: |
---|
[10] | 821 | ∀m,n,p:Pos. m < n → (n-m)+p = (n+p)-m. |
---|
[487] | 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. |
---|
[10] | 840 | |
---|
| 841 | (* XXX: putting this in the appropriate case screws up auto?! *) |
---|
[487] | 842 | theorem succ_plus_one: ∀n. succ n = n + one. |
---|
| 843 | #n elim n; //; qed. |
---|
[10] | 844 | |
---|
[487] | 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. |
---|
[10] | 852 | |
---|
[487] | 853 | theorem nat_succ_pos: ∀n. nat_of_pos (succ_pos_of_nat n) = S n. |
---|
| 854 | #n elim n; //; qed. |
---|
[10] | 855 | |
---|
[487] | 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. |
---|
[10] | 863 | |
---|
[487] | 864 | theorem plus_minus_m_m: ∀n,m:Pos. |
---|
[10] | 865 | m < n → n = (n-m)+m. |
---|
[487] | 866 | #n #m #lemn applyS sym_eq; |
---|
| 867 | applyS (plus_minus m n m); //; qed. |
---|
[10] | 868 | |
---|
[487] | 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 …) |
---|
[10] | 875 | /2/; |
---|
[487] | 876 | ] |
---|
| 877 | qed. |
---|
[10] | 878 | |
---|
[487] | 879 | theorem minus_to_plus :∀n,m,p:Pos. |
---|
[10] | 880 | m < n → n-m = p → n = m+p. |
---|
[487] | 881 | #n #m #p #lemn #eqp applyS plus_minus_m_m; //; |
---|
| 882 | qed. |
---|
[10] | 883 | |
---|
[487] | 884 | theorem plus_to_minus :∀n,m,p:Pos.n = m+p → n-m = p. |
---|
[10] | 885 | (* /4/ done in 43.5 *) |
---|
[487] | 886 | #n #m #p #eqp |
---|
| 887 | @sym_eq |
---|
| 888 | applyS (minus_plus_m_m p m); |
---|
| 889 | qed. |
---|
[10] | 890 | |
---|
[487] | 891 | theorem minus_pred_pred : ∀n,m:Pos. one < n → one < m → |
---|
[10] | 892 | pred n - pred m = n - m. |
---|
[487] | 893 | #n #m #posn #posm |
---|
| 894 | @(lt_one_n_elim n posn) |
---|
| 895 | @(lt_one_n_elim m posm) //. |
---|
| 896 | qed. |
---|
[10] | 897 | |
---|
| 898 | (* monotonicity and galois *) |
---|
| 899 | |
---|
[487] | 900 | theorem monotonic_le_minus_l: |
---|
[10] | 901 | ∀p,q,n:Pos. q ≤ p → q-n ≤ p-n. |
---|
[487] | 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. |
---|
[10] | 911 | |
---|
[487] | 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 | [|apply le_plus_minus_m_m |
---|
| 916 | |@monotonic_le_plus_l //; |
---|
| 917 | ] |
---|
| 918 | qed. |
---|
[10] | 919 | |
---|
[487] | 920 | theorem le_plus_to_minus: ∀n,m,p:Pos. n ≤ p+m → n-m ≤ p. |
---|
| 921 | #n #m #p #lep |
---|
[10] | 922 | (* bello *) |
---|
[487] | 923 | applyS monotonic_le_minus_l;//; |
---|
[10] | 924 | (* /2/; *) |
---|
[487] | 925 | qed. |
---|
[10] | 926 | |
---|
[487] | 927 | theorem monotonic_le_minus_r: |
---|
[10] | 928 | ∀p,q,n:Pos. q ≤ p → n-p ≤ n-q. |
---|
[487] | 929 | #p #q #n #lepq |
---|
| 930 | @le_plus_to_minus |
---|
| 931 | @(transitive_le ??? (le_plus_minus_m_m ? q)) /2/; |
---|
| 932 | qed. |
---|
[10] | 933 | |
---|
| 934 | (*********************** boolean arithmetics ********************) |
---|
| 935 | include "basics/bool.ma". |
---|
| 936 | |
---|
[487] | 937 | let rec eqb n m ≝ |
---|
[10] | 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 | ]. |
---|
[487] | 943 | |
---|
| 944 | theorem eqb_elim : ∀ n,m:Pos.∀ P:bool → Prop. |
---|
[10] | 945 | (n=m → (P true)) → (n ≠ m → (P false)) → (P (eqb n m)). |
---|
[487] | 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. |
---|
[10] | 968 | |
---|
[487] | 969 | theorem eqb_n_n: ∀n:Pos. eqb n n = true. |
---|
| 970 | #n elim n; normalize; //. |
---|
| 971 | qed. |
---|
[10] | 972 | |
---|
[487] | 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. |
---|
[10] | 977 | |
---|
[487] | 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. |
---|
[10] | 981 | |
---|
[487] | 982 | theorem eq_to_eqb_true: ∀n,m:Pos. |
---|
[10] | 983 | n = m → eqb n m = true. |
---|
[487] | 984 | //; qed. |
---|
[10] | 985 | |
---|
[487] | 986 | theorem not_eq_to_eqb_false: ∀n,m:Pos. |
---|
[10] | 987 | n ≠ m → eqb n m = false. |
---|
[487] | 988 | #n #m #noteq |
---|
| 989 | @eqb_elim //; |
---|
| 990 | #Heq @False_ind /2/; |
---|
| 991 | qed. |
---|
[10] | 992 | |
---|
[487] | 993 | let rec leb n m ≝ |
---|
[10] | 994 | match partial_minus n m with |
---|
| 995 | [ MinusNeg ⇒ true |
---|
| 996 | | MinusZero ⇒ true |
---|
| 997 | | MinusPos _ ⇒ false |
---|
| 998 | ]. |
---|
| 999 | |
---|
[487] | 1000 | lemma leb_unfold_hack: ∀n,m:Pos. leb n m = |
---|
[10] | 1001 | match partial_minus n m with |
---|
| 1002 | [ MinusNeg ⇒ true |
---|
| 1003 | | MinusZero ⇒ true |
---|
| 1004 | | MinusPos _ ⇒ false |
---|
[487] | 1005 | ]. #n #m (* XXX: why on earth do I need to case split? *) cases n; //; qed. |
---|
[10] | 1006 | |
---|
[487] | 1007 | theorem leb_elim: ∀n,m:Pos. ∀P:bool → Prop. |
---|
[10] | 1008 | (n ≤ m → P true) → (n ≰ m → P false) → P (leb n m). |
---|
[487] | 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. |
---|
[10] | 1023 | |
---|
[487] | 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. |
---|
[10] | 1030 | |
---|
[487] | 1031 | theorem leb_false_to_not_le:∀n,m:Pos. |
---|
[10] | 1032 | leb n m = false → n ≰ m. |
---|
[487] | 1033 | #n #m @leb_elim |
---|
| 1034 | [#_ #abs @False_ind /2/; |
---|
| 1035 | |//; |
---|
| 1036 | ] |
---|
| 1037 | qed. |
---|
[10] | 1038 | |
---|
[487] | 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. |
---|
[10] | 1043 | |
---|
[487] | 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. |
---|
[10] | 1048 | |
---|
[487] | 1049 | theorem lt_to_leb_false: ∀n,m:Pos. m < n → leb n m = false. |
---|
| 1050 | /3/; qed. |
---|
[10] | 1051 | |
---|
| 1052 | |
---|
| 1053 | (***** comparison *****) |
---|
| 1054 | |
---|
[487] | 1055 | definition pos_compare : Pos → Pos → compare ≝ |
---|
[10] | 1056 | λn,m.match partial_minus n m with |
---|
| 1057 | [ MinusNeg ⇒ LT |
---|
| 1058 | | MinusZero ⇒ EQ |
---|
| 1059 | | MinusPos _ ⇒ GT |
---|
| 1060 | ]. |
---|
| 1061 | |
---|
[487] | 1062 | theorem pos_compare_n_n: ∀n:Pos. pos_compare n n = EQ. |
---|
| 1063 | #n normalize; >(partial_minus_n_n n) |
---|
| 1064 | //; qed. |
---|
[10] | 1065 | |
---|
[487] | 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 …) |
---|
[10] | 1069 | //; |
---|
[487] | 1070 | qed. |
---|
[10] | 1071 | |
---|
[487] | 1072 | theorem pos_compare_pred_pred: |
---|
[10] | 1073 | ∀n,m.one < n → one < m → pos_compare n m = pos_compare (pred n) (pred m). |
---|
[487] | 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. |
---|
[10] | 1080 | |
---|
[487] | 1081 | theorem pos_compare_S_one: ∀n:Pos. pos_compare (succ n) one = GT. |
---|
| 1082 | #n elim n; //; qed. |
---|
[10] | 1083 | |
---|
[487] | 1084 | theorem pos_compare_one_S: ∀n:Pos. pos_compare one (succ n) = LT. |
---|
| 1085 | #n elim n; //; qed. |
---|
[10] | 1086 | |
---|
[487] | 1087 | theorem pos_compare_to_Prop: |
---|
[10] | 1088 | ∀n,m.match (pos_compare n m) with |
---|
| 1089 | [ LT ⇒ n < m |
---|
| 1090 | | EQ ⇒ n = m |
---|
| 1091 | | GT ⇒ m < n ]. |
---|
[487] | 1092 | #n #m |
---|
| 1093 | @(pos_elim2 (λn,m.match (pos_compare n m) with |
---|
[10] | 1094 | [ LT ⇒ n < m |
---|
| 1095 | | EQ ⇒ n = m |
---|
[891] | 1096 | | GT ⇒ m < n ])) |
---|
[487] | 1097 | [1,2:@pos_cases |
---|
| 1098 | [ 1,3: /2/; |
---|
| 1099 | | 2,4: #m' cases m'; //; |
---|
| 1100 | ] |
---|
[891] | 1101 | |#n1 #m1 <pos_compare_S_S cases (pos_compare n1 m1) |
---|
| 1102 | [1,3: #IH @le_succ_succ // |
---|
| 1103 | | #IH >IH // |
---|
| 1104 | ] |
---|
| 1105 | ] |
---|
[487] | 1106 | qed. |
---|
[10] | 1107 | |
---|
[487] | 1108 | theorem pos_compare_n_m_m_n: |
---|
[10] | 1109 | ∀n,m:Pos.pos_compare n m = compare_invert (pos_compare m n). |
---|
[487] | 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. |
---|
[10] | 1118 | |
---|
[487] | 1119 | theorem pos_compare_elim : |
---|
[10] | 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). |
---|
[487] | 1122 | #n #m #P #Hlt #Heq #Hgt |
---|
| 1123 | cut (match (pos_compare n m) with |
---|
[10] | 1124 | [ LT ⇒ n < m |
---|
| 1125 | | EQ ⇒ n=m |
---|
| 1126 | | GT ⇒ m < n] → |
---|
| 1127 | P (pos_compare n m)) |
---|
[487] | 1128 | [cases (pos_compare n m); |
---|
| 1129 | [@Hlt |
---|
| 1130 | |@Heq |
---|
| 1131 | |@Hgt] |
---|
| 1132 | |#Hcut @Hcut //; |
---|
| 1133 | qed. |
---|
[10] | 1134 | |
---|
[487] | 1135 | inductive cmp_cases (n,m:Pos) : CProp[0] ≝ |
---|
[10] | 1136 | | cmp_le : n ≤ m → cmp_cases n m |
---|
| 1137 | | cmp_gt : m < n → cmp_cases n m. |
---|
| 1138 | |
---|
[487] | 1139 | theorem lt_to_le : ∀n,m:Pos. n < m → n ≤ m. |
---|
[10] | 1140 | (* sic |
---|
[487] | 1141 | #n #m #H elim H |
---|
| 1142 | [// |
---|
| 1143 | |/2/] *) |
---|
| 1144 | /2/; qed. |
---|
[10] | 1145 | |
---|
[487] | 1146 | lemma cmp_nat: ∀n,m:Pos.cmp_cases n m. |
---|
| 1147 | #n #m lapply (pos_compare_to_Prop n m) |
---|
| 1148 | cases (pos_compare n m);normalize; /3/; |
---|
| 1149 | qed. |
---|
[10] | 1150 | |
---|
| 1151 | |
---|
| 1152 | |
---|
| 1153 | |
---|
[487] | 1154 | let rec two_power_nat (n:nat) : Pos ≝ |
---|
[10] | 1155 | match n with |
---|
| 1156 | [ O ⇒ one |
---|
| 1157 | | S n' ⇒ p0 (two_power_nat n') |
---|
| 1158 | ]. |
---|
| 1159 | |
---|
[487] | 1160 | definition two_power_pos : Pos → Pos ≝ λp.two_power_nat (nat_of_pos p). |
---|