source: src/ASM/Util.ma @ 777

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

Lots of work on RTL to ERTL pass from today.

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