source: src/ASM/Util.ma @ 907

Last change on this file since 907 was 907, checked in by boender, 9 years ago
  • added quadruples to Util
  • start of implementation of new jump expansion policy
File size: 8.7 KB
Line 
1include "basics/list.ma".
2include "basics/types.ma".
3include "arithmetics/nat.ma".
4 
5lemma eq_rect_Type0_r :
6  ∀A: Type[0].
7  ∀a:A.
8  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
9  #A #a #P #H #x #p
10  generalize in match H
11  generalize in match P
12  cases p
13  //
14qed.
15 
16let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
17  match n return λo. o < length A l → A with
18  [ O ⇒
19    match l return λm. 0 < length A m → A with
20    [ nil ⇒ λabsd1. ?
21    | cons hd tl ⇒ λprf1. hd
22    ]
23  | S n' ⇒
24    match l return λm. S n' < length A m → A with
25    [ nil ⇒ λabsd2. ?
26    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
27    ]
28  ] ?.
29  [ 1:
30    @ p
31  | 4:
32    normalize in prf2
33    normalize
34    @ le_S_S_to_le
35    assumption
36  | 2:
37    normalize in absd1;
38    cases (not_le_Sn_O O)
39    # H
40    elim (H absd1)
41  | 3:
42    normalize in absd2;
43    cases (not_le_Sn_O (S n'))
44    # H
45    elim (H absd2)
46  ]
47qed.
48 
49let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
50  match n with
51  [ O ⇒
52    match l with
53    [ nil ⇒ [ ]
54    | cons hd tl ⇒ l
55    ]
56  | S n ⇒
57    match l with
58    [ nil ⇒ [ ]
59    | cons hd tl ⇒
60      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
61    ]
62  ].
63 
64definition nub_by ≝
65  λA: Type[0].
66  λf: A → A → bool.
67  λl: list A.
68    nub_by_internal A f l (length ? l).
69 
70let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
71  match l with
72  [ nil ⇒ false
73  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
74  ].
75 
76let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
77  match n with
78  [ O ⇒ [ ]
79  | S n ⇒
80    match l with
81    [ nil ⇒ [ ]
82    | cons hd tl ⇒ hd :: take A n tl
83    ]
84  ].
85 
86let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
87  match n with
88  [ O ⇒ l
89  | S n ⇒
90    match l with
91    [ nil ⇒ [ ]
92    | cons hd tl ⇒ drop A n tl
93    ]
94  ].
95 
96definition list_split ≝
97  λA: Type[0].
98  λn: nat.
99  λl: list A.
100    〈take A n l, drop A n l〉.
101 
102let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
103                      (l: list A) on l: list B ≝
104  match l with
105  [ nil ⇒ nil ?
106  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
107  ]. 
108
109definition mapi ≝
110  λA, B: Type[0].
111  λf: nat → A → B.
112  λl: list A.
113    mapi_internal A B 0 f l.
114
115let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
116  match l with
117  [ nil ⇒ Some ? (nil (A × B))
118  | cons hd tl ⇒
119    match r with
120    [ nil ⇒ None ?
121    | cons hd' tl' ⇒
122      match zip ? ? tl tl' with
123      [ None ⇒ None ?
124      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
125      ]
126    ]
127  ].
128
129let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
130  match l with
131  [ nil ⇒ a
132  | cons hd tl ⇒ foldl A B f (f a hd) tl
133  ].
134
135definition flatten ≝
136  λA: Type[0].
137  λl: list (list A).
138    foldr ? ? (append ?) [ ] l.
139
140let rec rev (A: Type[0]) (l: list A) on l ≝
141  match l with
142  [ nil ⇒ nil A
143  | cons hd tl ⇒ (rev A tl) @ [ hd ]
144  ].
145   
146notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
147 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
148notation < "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
149 for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
150
151let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
152                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
153  match l with
154    [ nil ⇒ x
155    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
156    ].
157
158definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
159
160notation "hvbox(t⌈o ↦ h⌉)"
161  with precedence 45
162  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
163
164definition function_apply ≝
165  λA, B: Type[0].
166  λf: A → B.
167  λa: A.
168    f a.
169   
170notation "f break $ x"
171  left associative with precedence 99
172  for @{ 'function_apply $f $x }.
173 
174interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
175
176let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
177  match n with
178    [ O ⇒ a
179    | S o ⇒ f (iterate A f a o)
180    ].
181   
182notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
183 with precedence 10
184for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
185
186(* Yeah, I probably ought to do something more general... *)
187notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
188with precedence 90 for @{ 'triple $a $b $c}.
189interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
190
191notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
192with precedence 90 for @{ 'quadruple $a $b $c $d}.
193interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
194
195notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
196 with precedence 10
197for @{ 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 ] ] ] }.
198
199notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
200 with precedence 10
201for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
202
203notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
204 with precedence 10
205for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
206
207notation "⊥" with precedence 90
208  for @{ match ? in False with [ ] }.
209
210let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
211  match b with
212    [ true ⇒
213      match c with
214        [ false ⇒ true
215        | true ⇒ false
216        ]
217    | false ⇒
218      match c with
219        [ false ⇒ false
220        | true ⇒ true
221        ]
222    ].
223   
224definition ltb ≝
225  λm, n: nat.
226    leb (S m) n.
227   
228definition geb ≝
229  λm, n: nat.
230    ltb n m.
231
232definition gtb ≝
233  λm, n: nat.
234    leb n m.
235   
236(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
237let rec eq_nat (n: nat) (m: nat) on n: bool ≝
238  match n with
239  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
240  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
241  ].
242
243(* dpm: conflicts with library definitions
244interpretation "Nat less than" 'lt m n = (ltb m n).
245interpretation "Nat greater than" 'gt m n = (gtb m n).
246interpretation "Nat greater than eq" 'geq m n = (geb m n).
247*)
248
249let rec division_aux (m: nat) (n : nat) (p: nat) ≝
250  match ltb n (S p) with
251    [ true ⇒ O
252    | false ⇒
253      match m with
254        [ O ⇒ O
255        | (S q) ⇒ S (division_aux q (n - (S p)) p)
256        ]
257    ].
258   
259definition division ≝
260  λm, n: nat.
261    match n with
262      [ O ⇒ S m
263      | S o ⇒ division_aux m m o
264      ].
265     
266notation "hvbox(n break ÷ m)"
267  right associative with precedence 47
268  for @{ 'division $n $m }.
269 
270interpretation "Nat division" 'division n m = (division n m).
271
272let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
273  match leb n p with
274    [ true ⇒ n
275    | false ⇒
276      match m with
277        [ O ⇒ n
278        | S o ⇒ modulus_aux o (n - (S p)) p
279        ]
280    ].
281   
282definition modulus ≝
283  λm, n: nat.
284    match n with
285      [ O ⇒ m
286      | S o ⇒ modulus_aux m m o
287      ].
288   
289notation "hvbox(n break 'mod' m)"
290  right associative with precedence 47
291  for @{ 'modulus $n $m }.
292 
293interpretation "Nat modulus" 'modulus m n = (modulus m n).
294
295definition divide_with_remainder ≝
296  λm, n: nat.
297    pair ? ? (m ÷ n) (modulus m n).
298   
299let rec exponential (m: nat) (n: nat) on n ≝
300  match n with
301    [ O ⇒ S O
302    | S o ⇒ m * exponential m o
303    ].
304
305interpretation "Nat exponential" 'exp n m = (exponential n m).
306   
307notation "hvbox(a break ⊎ b)"
308 left associative with precedence 50
309for @{ 'disjoint_union $a $b }.
310interpretation "sum" 'disjoint_union A B = (Sum A B).
311
312theorem less_than_or_equal_monotone:
313  ∀m, n: nat.
314    m ≤ n → (S m) ≤ (S n).
315 #m #n #H
316 elim H
317 /2/
318qed.
319
320theorem less_than_or_equal_b_complete:
321  ∀m, n: nat.
322    leb m n = false → ¬(m ≤ n).
323 #m;
324 elim m;
325 normalize
326 [ #n #H
327   destruct
328 | #y #H1 #z
329   cases z
330   normalize
331   [ #H
332     /2/
333   | /3/
334   ]
335 ]
336qed.
337
338theorem less_than_or_equal_b_correct:
339  ∀m, n: nat.
340    leb m n = true → m ≤ n.
341 #m
342 elim m
343 //
344 #y #H1 #z
345 cases z
346 normalize
347 [ #H
348   destruct
349 | #n #H lapply (H1 … H) /2/
350 ]
351qed.
352
353definition less_than_or_equal_b_elim:
354 ∀m, n: nat.
355 ∀P: bool → Type[0].
356   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
357 #m #n #P #H1 #H2;
358 lapply (less_than_or_equal_b_correct m n)
359 lapply (less_than_or_equal_b_complete m n)
360 cases (leb m n)
361 /3/
362qed.
Note: See TracBrowser for help on using the repository browser.