source: src/ASM/Util.ma @ 782

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

More work on rtl-ertl pass from today, plus resolved conflict.

File size: 8.3 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    foldl ? ? (append ?) [ ] l.
139
140definition if_then_else ≝
141  λA: Type[0].
142  λb: bool.
143  λt: A.
144  λf: A.
145  match b with
146  [ true ⇒ t
147  | false ⇒ f
148  ].
149
150let rec rev (A: Type[0]) (l: list A) on l ≝
151  match l with
152  [ nil ⇒ nil A
153  | cons hd tl ⇒ (rev A tl) @ [ hd ]
154  ].
155   
156(*
157notation "hvbox('if' b 'then' t 'else' f)"
158  non associative with precedence 83
159  for @{ 'if_then_else $b $t $f }.
160*)
161notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
162notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }.
163
164interpretation "Bool if_then_else" 'if_then_else b t f = (if_then_else ? b t f).
165
166let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
167                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
168  match l with
169    [ nil ⇒ x
170    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
171    ].
172
173definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
174
175notation "hvbox(t⌈o ↦ h⌉)"
176  with precedence 45
177  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
178
179definition function_apply ≝
180  λA, B: Type[0].
181  λf: A → B.
182  λa: A.
183    f a.
184   
185notation "f break $ x"
186  left associative with precedence 99
187  for @{ 'function_apply $f $x }.
188 
189interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
190
191let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
192  match n with
193    [ O ⇒ a
194    | S o ⇒ f (iterate A f a o)
195    ].
196   
197notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
198 with precedence 10
199for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
200
201(* Yeah, I probably ought to do something more general... *)
202notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
203with precedence 90 for @{ 'triple $a $b $c}.
204interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
205
206notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
207 with precedence 10
208for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
209
210notation "⊥" with precedence 90
211  for @{ match ? in False with [ ] }.
212
213let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
214  match b with
215    [ true ⇒
216      match c with
217        [ false ⇒ true
218        | true ⇒ false
219        ]
220    | false ⇒
221      match c with
222        [ false ⇒ false
223        | true ⇒ true
224        ]
225    ].
226   
227definition ltb ≝
228  λm, n: nat.
229    leb (S m) n.
230   
231definition geb ≝
232  λm, n: nat.
233    ltb n m.
234
235definition gtb ≝
236  λm, n: nat.
237    leb n m.
238   
239(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
240let rec eq_nat (n: nat) (m: nat) on n: bool ≝
241  match n with
242  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
243  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
244  ].
245
246(* dpm: conflicts with library definitions
247interpretation "Nat less than" 'lt m n = (ltb m n).
248interpretation "Nat greater than" 'gt m n = (gtb m n).
249interpretation "Nat greater than eq" 'geq m n = (geb m n).
250*)
251
252let rec division_aux (m: nat) (n : nat) (p: nat) ≝
253  match ltb n (S p) with
254    [ true ⇒ O
255    | false ⇒
256      match m with
257        [ O ⇒ O
258        | (S q) ⇒ S (division_aux q (n - (S p)) p)
259        ]
260    ].
261   
262definition division ≝
263  λm, n: nat.
264    match n with
265      [ O ⇒ S m
266      | S o ⇒ division_aux m m o
267      ].
268     
269notation "hvbox(n break ÷ m)"
270  right associative with precedence 47
271  for @{ 'division $n $m }.
272 
273interpretation "Nat division" 'division n m = (division n m).
274
275let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
276  match leb n p with
277    [ true ⇒ n
278    | false ⇒
279      match m with
280        [ O ⇒ n
281        | S o ⇒ modulus_aux o (n - (S p)) p
282        ]
283    ].
284   
285definition modulus ≝
286  λm, n: nat.
287    match n with
288      [ O ⇒ m
289      | S o ⇒ modulus_aux m m o
290      ].
291   
292notation "hvbox(n break 'mod' m)"
293  right associative with precedence 47
294  for @{ 'modulus $n $m }.
295 
296interpretation "Nat modulus" 'modulus m n = (modulus m n).
297
298definition divide_with_remainder ≝
299  λm, n: nat.
300    pair ? ? (m ÷ n) (modulus m n).
301   
302let rec exponential (m: nat) (n: nat) on n ≝
303  match n with
304    [ O ⇒ S O
305    | S o ⇒ m * exponential m o
306    ].
307
308interpretation "Nat exponential" 'exp n m = (exponential n m).
309   
310notation "hvbox(a break ⊎ b)"
311 left associative with precedence 50
312for @{ 'disjoint_union $a $b }.
313interpretation "sum" 'disjoint_union A B = (Sum A B).
314
315theorem less_than_or_equal_monotone:
316  ∀m, n: nat.
317    m ≤ n → (S m) ≤ (S n).
318 #m #n #H
319 elim H
320 /2/
321qed.
322
323theorem less_than_or_equal_b_complete:
324  ∀m, n: nat.
325    leb m n = false → ¬(m ≤ n).
326 #m;
327 elim m;
328 normalize
329 [ #n #H
330   destruct
331 | #y #H1 #z
332   cases z
333   normalize
334   [ #H
335     /2/
336   | /3/
337   ]
338 ]
339qed.
340
341theorem less_than_or_equal_b_correct:
342  ∀m, n: nat.
343    leb m n = true → m ≤ n.
344 #m
345 elim m
346 //
347 #y #H1 #z
348 cases z
349 normalize
350 [ #H
351   destruct
352 | #n #H lapply (H1 … H) /2/
353 ]
354qed.
355
356definition less_than_or_equal_b_elim:
357 ∀m, n: nat.
358 ∀P: bool → Type[0].
359   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
360 #m #n #P #H1 #H2;
361 lapply (less_than_or_equal_b_correct m n)
362 lapply (less_than_or_equal_b_complete m n)
363 cases (leb m n)
364 /3/
365qed.
Note: See TracBrowser for help on using the repository browser.