[475] | 1 | include "basics/list.ma". |
---|
[697] | 2 | include "basics/types.ma". |
---|
[712] | 3 | include "arithmetics/nat.ma". |
---|
[990] | 4 | |
---|
| 5 | (* let's implement a daemon not used by automation *) |
---|
| 6 | inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX. |
---|
| 7 | axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX. |
---|
| 8 | example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed. |
---|
| 9 | example not_implemented: False. cases daemon qed. |
---|
[1059] | 10 | |
---|
| 11 | notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)" |
---|
| 12 | with precedence 10 |
---|
| 13 | for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. |
---|
| 14 | |
---|
[1060] | 15 | let rec nth_safe |
---|
| 16 | (elt_type: Type[0]) (index: nat) (the_list: list elt_type) |
---|
| 17 | (proof: index < | the_list |) |
---|
| 18 | on index ≝ |
---|
| 19 | match index return λs. s < | the_list | → elt_type with |
---|
| 20 | [ O ⇒ |
---|
| 21 | match the_list return λt. 0 < | t | → elt_type with |
---|
| 22 | [ nil ⇒ λnil_absurd. ? |
---|
| 23 | | cons hd tl ⇒ λcons_proof. hd |
---|
| 24 | ] |
---|
| 25 | | S index' ⇒ |
---|
| 26 | match the_list return λt. S index' < | t | → elt_type with |
---|
| 27 | [ nil ⇒ λnil_absurd. ? |
---|
| 28 | | cons hd tl ⇒ |
---|
| 29 | λcons_proof. nth_safe elt_type index' tl ? |
---|
| 30 | ] |
---|
| 31 | ] proof. |
---|
| 32 | [ normalize in nil_absurd; |
---|
| 33 | cases (not_le_Sn_O 0) |
---|
| 34 | #ABSURD |
---|
| 35 | elim (ABSURD nil_absurd) |
---|
| 36 | | normalize in nil_absurd; |
---|
| 37 | cases (not_le_Sn_O (S index')) |
---|
| 38 | #ABSURD |
---|
| 39 | elim (ABSURD nil_absurd) |
---|
| 40 | | normalize in cons_proof |
---|
| 41 | @le_S_S_to_le |
---|
| 42 | assumption |
---|
| 43 | ] |
---|
| 44 | qed. |
---|
| 45 | |
---|
| 46 | definition last_safe ≝ |
---|
| 47 | λelt_type: Type[0]. |
---|
| 48 | λthe_list: list elt_type. |
---|
| 49 | λproof : 0 < | the_list |. |
---|
| 50 | nth_safe elt_type (|the_list| - 1) the_list ?. |
---|
| 51 | normalize /2/ |
---|
| 52 | qed. |
---|
| 53 | |
---|
[1059] | 54 | let rec reduce |
---|
| 55 | (A: Type[0]) (left: list A) (right: list A) on left ≝ |
---|
| 56 | match left with |
---|
| 57 | [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 |
---|
| 58 | | cons hd tl ⇒ |
---|
| 59 | match right with |
---|
| 60 | [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 |
---|
| 61 | | cons hd' tl' ⇒ |
---|
| 62 | let 〈cleft, cright〉 ≝ reduce A tl tl' in |
---|
| 63 | let 〈commonl, restl〉 ≝ cleft in |
---|
| 64 | let 〈commonr, restr〉 ≝ cright in |
---|
| 65 | 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 |
---|
| 66 | ] |
---|
| 67 | ]. |
---|
| 68 | |
---|
[1060] | 69 | axiom reduce_strong: |
---|
| 70 | ∀A: Type[0]. |
---|
| 71 | ∀left: list A. |
---|
| 72 | ∀right: list A. |
---|
| 73 | Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |. |
---|
| 74 | |
---|
[1059] | 75 | (* |
---|
| 76 | let rec reduce_strong |
---|
| 77 | (A: Type[0]) (left: list A) (right: list A) (prf: | left | = | right |) on left ≝ |
---|
| 78 | match left return λx. |x| = |right| → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with |
---|
| 79 | [ nil ⇒ |
---|
| 80 | match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with |
---|
[1060] | 81 | [ nil ⇒ λnil_nil_prf. ? |
---|
| 82 | | cons hd tl ⇒ λnil_cons_absrd_prf. ? |
---|
[1059] | 83 | ] |
---|
| 84 | | cons hd tl ⇒ |
---|
| 85 | match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with |
---|
| 86 | [ nil ⇒ λcons_nil_absrd_prf. ? |
---|
[1060] | 87 | | cons hd' tl' ⇒ λcons_cons_prf. |
---|
| 88 | let tail_call ≝ reduce_strong A tl tl' ? in ? |
---|
[1059] | 89 | ] |
---|
| 90 | ] prf. |
---|
[1060] | 91 | [ 5: normalize in cons_cons_prf; |
---|
| 92 | destruct(cons_cons_prf) |
---|
| 93 | assumption |
---|
| 94 | | 2: normalize in nil_cons_absrd_prf; |
---|
| 95 | destruct(nil_cons_absrd_prf) |
---|
| 96 | | 3: normalize in cons_nil_absrd_prf; |
---|
| 97 | destruct(cons_nil_absrd_prf) |
---|
| 98 | ] |
---|
| 99 | qed. |
---|
| 100 | *) |
---|
| 101 | |
---|
[1059] | 102 | axiom reduce_length: |
---|
| 103 | ∀A: Type[0]. |
---|
| 104 | ∀left, right: list A. |
---|
| 105 | ∀prf: | left | = | right |. |
---|
| 106 | \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)). |
---|
| 107 | |
---|
[1057] | 108 | let rec map2_opt |
---|
| 109 | (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) |
---|
| 110 | (left: list A) (right: list B) on left ≝ |
---|
| 111 | match left with |
---|
| 112 | [ nil ⇒ |
---|
| 113 | match right with |
---|
| 114 | [ nil ⇒ Some ? (nil C) |
---|
| 115 | | _ ⇒ None ? |
---|
| 116 | ] |
---|
| 117 | | cons hd tl ⇒ |
---|
| 118 | match right with |
---|
| 119 | [ nil ⇒ None ? |
---|
| 120 | | cons hd' tl' ⇒ |
---|
| 121 | match map2_opt A B C f tl tl' with |
---|
| 122 | [ None ⇒ None ? |
---|
| 123 | | Some tail ⇒ Some ? (f hd hd' :: tail) |
---|
| 124 | ] |
---|
| 125 | ] |
---|
| 126 | ]. |
---|
| 127 | |
---|
| 128 | let rec map2 |
---|
| 129 | (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C) |
---|
| 130 | (left: list A) (right: list B) (proof: | left | = | right |) on left ≝ |
---|
| 131 | match left return λx. | x | = | right | → list C with |
---|
| 132 | [ nil ⇒ |
---|
| 133 | match right return λy. | [] | = | y | → list C with |
---|
| 134 | [ nil ⇒ λnil_prf. nil C |
---|
| 135 | | _ ⇒ λcons_absrd. ? |
---|
| 136 | ] |
---|
| 137 | | cons hd tl ⇒ |
---|
| 138 | match right return λy. | hd::tl | = | y | → list C with |
---|
| 139 | [ nil ⇒ λnil_absrd. ? |
---|
| 140 | | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ? |
---|
| 141 | ] |
---|
| 142 | ] proof. |
---|
| 143 | [1: normalize in cons_absrd; |
---|
| 144 | destruct(cons_absrd) |
---|
| 145 | |2: normalize in nil_absrd; |
---|
| 146 | destruct(nil_absrd) |
---|
| 147 | |3: normalize in cons_prf; |
---|
| 148 | destruct(cons_prf) |
---|
| 149 | assumption |
---|
| 150 | ] |
---|
| 151 | qed. |
---|
| 152 | |
---|
[782] | 153 | lemma eq_rect_Type0_r : |
---|
| 154 | ∀A: Type[0]. |
---|
| 155 | ∀a:A. |
---|
| 156 | ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. |
---|
| 157 | #A #a #P #H #x #p |
---|
| 158 | generalize in match H |
---|
| 159 | generalize in match P |
---|
| 160 | cases p |
---|
| 161 | // |
---|
| 162 | qed. |
---|
| 163 | |
---|
| 164 | let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝ |
---|
| 165 | match n return λo. o < length A l → A with |
---|
| 166 | [ O ⇒ |
---|
| 167 | match l return λm. 0 < length A m → A with |
---|
| 168 | [ nil ⇒ λabsd1. ? |
---|
| 169 | | cons hd tl ⇒ λprf1. hd |
---|
| 170 | ] |
---|
| 171 | | S n' ⇒ |
---|
| 172 | match l return λm. S n' < length A m → A with |
---|
| 173 | [ nil ⇒ λabsd2. ? |
---|
| 174 | | cons hd tl ⇒ λprf2. safe_nth A n' tl ? |
---|
| 175 | ] |
---|
| 176 | ] ?. |
---|
| 177 | [ 1: |
---|
| 178 | @ p |
---|
| 179 | | 4: |
---|
| 180 | normalize in prf2 |
---|
| 181 | normalize |
---|
| 182 | @ le_S_S_to_le |
---|
| 183 | assumption |
---|
| 184 | | 2: |
---|
| 185 | normalize in absd1; |
---|
| 186 | cases (not_le_Sn_O O) |
---|
| 187 | # H |
---|
| 188 | elim (H absd1) |
---|
| 189 | | 3: |
---|
| 190 | normalize in absd2; |
---|
| 191 | cases (not_le_Sn_O (S n')) |
---|
| 192 | # H |
---|
| 193 | elim (H absd2) |
---|
| 194 | ] |
---|
| 195 | qed. |
---|
| 196 | |
---|
[777] | 197 | let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ |
---|
| 198 | match n with |
---|
| 199 | [ O ⇒ |
---|
| 200 | match l with |
---|
| 201 | [ nil ⇒ [ ] |
---|
| 202 | | cons hd tl ⇒ l |
---|
| 203 | ] |
---|
| 204 | | S n ⇒ |
---|
| 205 | match l with |
---|
| 206 | [ nil ⇒ [ ] |
---|
| 207 | | cons hd tl ⇒ |
---|
| 208 | hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n |
---|
| 209 | ] |
---|
| 210 | ]. |
---|
| 211 | |
---|
| 212 | definition nub_by ≝ |
---|
| 213 | λA: Type[0]. |
---|
| 214 | λf: A → A → bool. |
---|
| 215 | λl: list A. |
---|
| 216 | nub_by_internal A f l (length ? l). |
---|
| 217 | |
---|
| 218 | let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝ |
---|
| 219 | match l with |
---|
| 220 | [ nil ⇒ false |
---|
| 221 | | cons hd tl ⇒ orb (eq a hd) (member A eq a tl) |
---|
| 222 | ]. |
---|
| 223 | |
---|
| 224 | let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝ |
---|
| 225 | match n with |
---|
| 226 | [ O ⇒ [ ] |
---|
| 227 | | S n ⇒ |
---|
| 228 | match l with |
---|
| 229 | [ nil ⇒ [ ] |
---|
| 230 | | cons hd tl ⇒ hd :: take A n tl |
---|
| 231 | ] |
---|
| 232 | ]. |
---|
| 233 | |
---|
| 234 | let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝ |
---|
| 235 | match n with |
---|
| 236 | [ O ⇒ l |
---|
| 237 | | S n ⇒ |
---|
| 238 | match l with |
---|
| 239 | [ nil ⇒ [ ] |
---|
| 240 | | cons hd tl ⇒ drop A n tl |
---|
| 241 | ] |
---|
| 242 | ]. |
---|
| 243 | |
---|
| 244 | definition list_split ≝ |
---|
| 245 | λA: Type[0]. |
---|
| 246 | λn: nat. |
---|
| 247 | λl: list A. |
---|
| 248 | 〈take A n l, drop A n l〉. |
---|
| 249 | |
---|
| 250 | let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B) |
---|
| 251 | (l: list A) on l: list B ≝ |
---|
| 252 | match l with |
---|
| 253 | [ nil ⇒ nil ? |
---|
| 254 | | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl) |
---|
| 255 | ]. |
---|
[475] | 256 | |
---|
[777] | 257 | definition mapi ≝ |
---|
| 258 | λA, B: Type[0]. |
---|
| 259 | λf: nat → A → B. |
---|
| 260 | λl: list A. |
---|
| 261 | mapi_internal A B 0 f l. |
---|
| 262 | |
---|
| 263 | let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ |
---|
| 264 | match l with |
---|
| 265 | [ nil ⇒ Some ? (nil (A × B)) |
---|
| 266 | | cons hd tl ⇒ |
---|
| 267 | match r with |
---|
| 268 | [ nil ⇒ None ? |
---|
| 269 | | cons hd' tl' ⇒ |
---|
| 270 | match zip ? ? tl tl' with |
---|
| 271 | [ None ⇒ None ? |
---|
| 272 | | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail) |
---|
| 273 | ] |
---|
| 274 | ] |
---|
| 275 | ]. |
---|
| 276 | |
---|
[698] | 277 | let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝ |
---|
| 278 | match l with |
---|
| 279 | [ nil ⇒ a |
---|
| 280 | | cons hd tl ⇒ foldl A B f (f a hd) tl |
---|
| 281 | ]. |
---|
| 282 | |
---|
[998] | 283 | lemma foldl_step: |
---|
| 284 | ∀A:Type[0]. |
---|
| 285 | ∀B: Type[0]. |
---|
| 286 | ∀H: A → B → A. |
---|
| 287 | ∀acc: A. |
---|
| 288 | ∀pre: list B. |
---|
| 289 | ∀hd:B. |
---|
| 290 | foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd). |
---|
| 291 | #A #B #H #acc #pre generalize in match acc; -acc; elim pre |
---|
| 292 | [ normalize; // |
---|
| 293 | | #hd #tl #IH #acc #X normalize; @IH ] |
---|
| 294 | qed. |
---|
| 295 | |
---|
| 296 | lemma foldl_append: |
---|
| 297 | ∀A:Type[0]. |
---|
| 298 | ∀B: Type[0]. |
---|
| 299 | ∀H: A → B → A. |
---|
| 300 | ∀acc: A. |
---|
| 301 | ∀suff,pre: list B. |
---|
| 302 | foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff). |
---|
| 303 | #A #B #H #acc #suff elim suff |
---|
| 304 | [ #pre >append_nil % |
---|
| 305 | | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ] |
---|
| 306 | qed. |
---|
| 307 | |
---|
[698] | 308 | definition flatten ≝ |
---|
| 309 | λA: Type[0]. |
---|
| 310 | λl: list (list A). |
---|
[900] | 311 | foldr ? ? (append ?) [ ] l. |
---|
[698] | 312 | |
---|
[715] | 313 | let rec rev (A: Type[0]) (l: list A) on l ≝ |
---|
| 314 | match l with |
---|
| 315 | [ nil ⇒ nil A |
---|
| 316 | | cons hd tl ⇒ (rev A tl) @ [ hd ] |
---|
| 317 | ]. |
---|
[475] | 318 | |
---|
[856] | 319 | notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 |
---|
| 320 | for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f] }. |
---|
[858] | 321 | notation < "hvbox('if' \nbsp term 19 e \nbsp break 'then' \nbsp term 19 t \nbsp break 'else' \nbsp term 48 f \nbsp)" non associative with precedence 19 |
---|
[856] | 322 | for @{ match $e with [ true ⇒ $t | false ⇒ $f] }. |
---|
[475] | 323 | |
---|
| 324 | let rec fold_left_i_aux (A: Type[0]) (B: Type[0]) |
---|
| 325 | (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝ |
---|
| 326 | match l with |
---|
| 327 | [ nil ⇒ x |
---|
| 328 | | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl |
---|
| 329 | ]. |
---|
| 330 | |
---|
| 331 | definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. |
---|
| 332 | |
---|
| 333 | notation "hvbox(t⌈o ↦ h⌉)" |
---|
| 334 | with precedence 45 |
---|
| 335 | for @{ match (? : $o=$h) with [ refl ⇒ $t ] }. |
---|
| 336 | |
---|
| 337 | definition function_apply ≝ |
---|
| 338 | λA, B: Type[0]. |
---|
| 339 | λf: A → B. |
---|
| 340 | λa: A. |
---|
| 341 | f a. |
---|
| 342 | |
---|
| 343 | notation "f break $ x" |
---|
| 344 | left associative with precedence 99 |
---|
| 345 | for @{ 'function_apply $f $x }. |
---|
| 346 | |
---|
| 347 | interpretation "Function application" 'function_apply f x = (function_apply ? ? f x). |
---|
| 348 | |
---|
| 349 | let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝ |
---|
| 350 | match n with |
---|
| 351 | [ O ⇒ a |
---|
| 352 | | S o ⇒ f (iterate A f a o) |
---|
| 353 | ]. |
---|
| 354 | |
---|
[764] | 355 | (* Yeah, I probably ought to do something more general... *) |
---|
| 356 | notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)" |
---|
| 357 | with precedence 90 for @{ 'triple $a $b $c}. |
---|
| 358 | interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z). |
---|
| 359 | |
---|
[907] | 360 | notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)" |
---|
| 361 | with precedence 90 for @{ 'quadruple $a $b $c $d}. |
---|
| 362 | interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)). |
---|
| 363 | |
---|
| 364 | notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)" |
---|
| 365 | with precedence 10 |
---|
| 366 | for @{ match $t with [ pair ${fresh wx} ${fresh yz} ⇒ match ${fresh wx} with [ pair ${ident w} ${ident x} ⇒ match ${fresh yz} with [ pair ${ident y} ${ident z} ⇒ $s ] ] ] }. |
---|
| 367 | |
---|
[764] | 368 | notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)" |
---|
| 369 | with precedence 10 |
---|
| 370 | for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }. |
---|
| 371 | |
---|
[857] | 372 | notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)" |
---|
[856] | 373 | with precedence 10 |
---|
| 374 | for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }. |
---|
| 375 | |
---|
[993] | 376 | axiom pair_elim': |
---|
| 377 | ∀A,B,C: Type[0]. |
---|
| 378 | ∀T: A → B → C. |
---|
| 379 | ∀p. |
---|
| 380 | ∀P: A×B → C → Prop. |
---|
| 381 | (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) → |
---|
| 382 | P p (let 〈lft, rgt〉 ≝ p in T lft rgt). |
---|
| 383 | |
---|
| 384 | axiom pair_elim'': |
---|
| 385 | ∀A,B,C,C': Type[0]. |
---|
| 386 | ∀T: A → B → C. |
---|
| 387 | ∀T': A → B → C'. |
---|
| 388 | ∀p. |
---|
| 389 | ∀P: A×B → C → C' → Prop. |
---|
| 390 | (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) → |
---|
| 391 | P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt). |
---|
| 392 | |
---|
| 393 | lemma pair_destruct_1: |
---|
| 394 | ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c. |
---|
| 395 | #A #B #a #b *; /2/ |
---|
| 396 | qed. |
---|
| 397 | |
---|
| 398 | lemma pair_destruct_2: |
---|
| 399 | ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. |
---|
| 400 | #A #B #a #b *; /2/ |
---|
| 401 | qed. |
---|
| 402 | |
---|
| 403 | |
---|
[475] | 404 | notation "⊥" with precedence 90 |
---|
| 405 | for @{ match ? in False with [ ] }. |
---|
| 406 | |
---|
| 407 | let rec exclusive_disjunction (b: bool) (c: bool) on b ≝ |
---|
| 408 | match b with |
---|
| 409 | [ true ⇒ |
---|
| 410 | match c with |
---|
| 411 | [ false ⇒ true |
---|
| 412 | | true ⇒ false |
---|
| 413 | ] |
---|
| 414 | | false ⇒ |
---|
| 415 | match c with |
---|
| 416 | [ false ⇒ false |
---|
| 417 | | true ⇒ true |
---|
| 418 | ] |
---|
| 419 | ]. |
---|
[712] | 420 | |
---|
[475] | 421 | definition ltb ≝ |
---|
| 422 | λm, n: nat. |
---|
| 423 | leb (S m) n. |
---|
| 424 | |
---|
| 425 | definition geb ≝ |
---|
| 426 | λm, n: nat. |
---|
| 427 | ltb n m. |
---|
| 428 | |
---|
| 429 | definition gtb ≝ |
---|
| 430 | λm, n: nat. |
---|
| 431 | leb n m. |
---|
[746] | 432 | |
---|
| 433 | (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) |
---|
| 434 | let rec eq_nat (n: nat) (m: nat) on n: bool ≝ |
---|
| 435 | match n with |
---|
| 436 | [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ] |
---|
| 437 | | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ] |
---|
| 438 | ]. |
---|
[475] | 439 | |
---|
[712] | 440 | (* dpm: conflicts with library definitions |
---|
[475] | 441 | interpretation "Nat less than" 'lt m n = (ltb m n). |
---|
| 442 | interpretation "Nat greater than" 'gt m n = (gtb m n). |
---|
| 443 | interpretation "Nat greater than eq" 'geq m n = (geb m n). |
---|
[712] | 444 | *) |
---|
[475] | 445 | |
---|
| 446 | let rec division_aux (m: nat) (n : nat) (p: nat) ≝ |
---|
[697] | 447 | match ltb n (S p) with |
---|
[475] | 448 | [ true ⇒ O |
---|
| 449 | | false ⇒ |
---|
| 450 | match m with |
---|
| 451 | [ O ⇒ O |
---|
| 452 | | (S q) ⇒ S (division_aux q (n - (S p)) p) |
---|
| 453 | ] |
---|
| 454 | ]. |
---|
| 455 | |
---|
| 456 | definition division ≝ |
---|
| 457 | λm, n: nat. |
---|
| 458 | match n with |
---|
| 459 | [ O ⇒ S m |
---|
| 460 | | S o ⇒ division_aux m m o |
---|
| 461 | ]. |
---|
| 462 | |
---|
| 463 | notation "hvbox(n break ÷ m)" |
---|
| 464 | right associative with precedence 47 |
---|
| 465 | for @{ 'division $n $m }. |
---|
| 466 | |
---|
| 467 | interpretation "Nat division" 'division n m = (division n m). |
---|
| 468 | |
---|
| 469 | let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝ |
---|
| 470 | match leb n p with |
---|
| 471 | [ true ⇒ n |
---|
| 472 | | false ⇒ |
---|
| 473 | match m with |
---|
| 474 | [ O ⇒ n |
---|
| 475 | | S o ⇒ modulus_aux o (n - (S p)) p |
---|
| 476 | ] |
---|
| 477 | ]. |
---|
| 478 | |
---|
| 479 | definition modulus ≝ |
---|
| 480 | λm, n: nat. |
---|
| 481 | match n with |
---|
| 482 | [ O ⇒ m |
---|
| 483 | | S o ⇒ modulus_aux m m o |
---|
| 484 | ]. |
---|
| 485 | |
---|
| 486 | notation "hvbox(n break 'mod' m)" |
---|
| 487 | right associative with precedence 47 |
---|
| 488 | for @{ 'modulus $n $m }. |
---|
| 489 | |
---|
| 490 | interpretation "Nat modulus" 'modulus m n = (modulus m n). |
---|
| 491 | |
---|
| 492 | definition divide_with_remainder ≝ |
---|
| 493 | λm, n: nat. |
---|
[697] | 494 | pair ? ? (m ÷ n) (modulus m n). |
---|
[475] | 495 | |
---|
| 496 | let rec exponential (m: nat) (n: nat) on n ≝ |
---|
| 497 | match n with |
---|
| 498 | [ O ⇒ S O |
---|
| 499 | | S o ⇒ m * exponential m o |
---|
| 500 | ]. |
---|
| 501 | |
---|
| 502 | interpretation "Nat exponential" 'exp n m = (exponential n m). |
---|
| 503 | |
---|
| 504 | notation "hvbox(a break ⊎ b)" |
---|
| 505 | left associative with precedence 50 |
---|
| 506 | for @{ 'disjoint_union $a $b }. |
---|
| 507 | interpretation "sum" 'disjoint_union A B = (Sum A B). |
---|
| 508 | |
---|
| 509 | theorem less_than_or_equal_monotone: |
---|
| 510 | ∀m, n: nat. |
---|
| 511 | m ≤ n → (S m) ≤ (S n). |
---|
| 512 | #m #n #H |
---|
| 513 | elim H |
---|
| 514 | /2/ |
---|
| 515 | qed. |
---|
| 516 | |
---|
| 517 | theorem less_than_or_equal_b_complete: |
---|
| 518 | ∀m, n: nat. |
---|
| 519 | leb m n = false → ¬(m ≤ n). |
---|
| 520 | #m; |
---|
| 521 | elim m; |
---|
| 522 | normalize |
---|
| 523 | [ #n #H |
---|
| 524 | destruct |
---|
| 525 | | #y #H1 #z |
---|
| 526 | cases z |
---|
| 527 | normalize |
---|
| 528 | [ #H |
---|
| 529 | /2/ |
---|
| 530 | | /3/ |
---|
| 531 | ] |
---|
| 532 | ] |
---|
| 533 | qed. |
---|
| 534 | |
---|
| 535 | theorem less_than_or_equal_b_correct: |
---|
| 536 | ∀m, n: nat. |
---|
| 537 | leb m n = true → m ≤ n. |
---|
| 538 | #m |
---|
| 539 | elim m |
---|
| 540 | // |
---|
| 541 | #y #H1 #z |
---|
| 542 | cases z |
---|
| 543 | normalize |
---|
| 544 | [ #H |
---|
| 545 | destruct |
---|
[704] | 546 | | #n #H lapply (H1 … H) /2/ |
---|
[475] | 547 | ] |
---|
| 548 | qed. |
---|
| 549 | |
---|
| 550 | definition less_than_or_equal_b_elim: |
---|
| 551 | ∀m, n: nat. |
---|
| 552 | ∀P: bool → Type[0]. |
---|
| 553 | (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n). |
---|
| 554 | #m #n #P #H1 #H2; |
---|
| 555 | lapply (less_than_or_equal_b_correct m n) |
---|
| 556 | lapply (less_than_or_equal_b_complete m n) |
---|
| 557 | cases (leb m n) |
---|
| 558 | /3/ |
---|
[856] | 559 | qed. |
---|
[985] | 560 | |
---|
| 561 | lemma inclusive_disjunction_true: |
---|
| 562 | ∀b, c: bool. |
---|
| 563 | (orb b c) = true → b = true ∨ c = true. |
---|
| 564 | # b |
---|
| 565 | # c |
---|
| 566 | elim b |
---|
| 567 | [ normalize |
---|
| 568 | # H |
---|
| 569 | @ or_introl |
---|
| 570 | % |
---|
| 571 | | normalize |
---|
| 572 | /2/ |
---|
| 573 | ] |
---|
| 574 | qed. |
---|
| 575 | |
---|
| 576 | lemma conjunction_true: |
---|
| 577 | ∀b, c: bool. |
---|
| 578 | andb b c = true → b = true ∧ c = true. |
---|
| 579 | # b |
---|
| 580 | # c |
---|
| 581 | elim b |
---|
| 582 | normalize |
---|
| 583 | [ /2/ |
---|
| 584 | | # K |
---|
| 585 | destruct |
---|
| 586 | ] |
---|
| 587 | qed. |
---|
| 588 | |
---|
| 589 | lemma eq_true_false: false=true → False. |
---|
| 590 | # K |
---|
| 591 | destruct |
---|
| 592 | qed. |
---|
| 593 | |
---|
| 594 | lemma inclusive_disjunction_b_true: ∀b. orb b true = true. |
---|
| 595 | # b |
---|
| 596 | cases b |
---|
| 597 | % |
---|
| 598 | qed. |
---|
| 599 | |
---|
| 600 | definition bool_to_Prop ≝ |
---|
| 601 | λb. match b with [ true ⇒ True | false ⇒ False ]. |
---|
| 602 | |
---|
| 603 | coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. |
---|
| 604 | |
---|
| 605 | lemma eq_false_to_notb: ∀b. b = false → ¬ b. |
---|
| 606 | *; /2/ |
---|
| 607 | qed. |
---|
| 608 | |
---|
| 609 | lemma length_append: |
---|
| 610 | ∀A.∀l1,l2:list A. |
---|
| 611 | |l1 @ l2| = |l1| + |l2|. |
---|
| 612 | #A #l1 elim l1 |
---|
| 613 | [ // |
---|
| 614 | | #hd #tl #IH #l2 normalize <IH //] |
---|
| 615 | qed. |
---|