source: src/ASM/Util.ma @ 1057

Last change on this file since 1057 was 1057, checked in by mulligan, 8 years ago

changes from today

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