source: src/ASM/Util.ma @ 998

Last change on this file since 998 was 998, checked in by sacerdot, 10 years ago

Half repaired, half broken. Most functions no longer return option types,
taking in input dependent types.

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