source: src/ASM/Util.ma @ 1059

Last change on this file since 1059 was 1059, checked in by mulligan, 9 years ago

work from today, bit of a mess at the moment

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