source: src/ASM/Util.ma @ 856

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