source: src/ASM/Util.ma @ 993

Last change on this file since 993 was 993, checked in by sacerdot, 8 years ago

More Russell everywhere; getting closer to the goal.

File size: 10.6 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
141definition flatten ≝
142  λA: Type[0].
143  λl: list (list A).
144    foldr ? ? (append ?) [ ] l.
145
146let rec rev (A: Type[0]) (l: list A) on l ≝
147  match l with
148  [ nil ⇒ nil A
149  | cons hd tl ⇒ (rev A tl) @ [ hd ]
150  ].
151   
152notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
153 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
154notation < "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
155 for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
156
157let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
158                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
159  match l with
160    [ nil ⇒ x
161    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
162    ].
163
164definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
165
166notation "hvbox(t⌈o ↦ h⌉)"
167  with precedence 45
168  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
169
170definition function_apply ≝
171  λA, B: Type[0].
172  λf: A → B.
173  λa: A.
174    f a.
175   
176notation "f break $ x"
177  left associative with precedence 99
178  for @{ 'function_apply $f $x }.
179 
180interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
181
182let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
183  match n with
184    [ O ⇒ a
185    | S o ⇒ f (iterate A f a o)
186    ].
187   
188notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
189 with precedence 10
190for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
191
192(* Yeah, I probably ought to do something more general... *)
193notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
194with precedence 90 for @{ 'triple $a $b $c}.
195interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
196
197notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
198with precedence 90 for @{ 'quadruple $a $b $c $d}.
199interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
200
201notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
202 with precedence 10
203for @{ 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 ] ] ] }.
204
205notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
206 with precedence 10
207for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
208
209notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
210 with precedence 10
211for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
212
213axiom pair_elim':
214  ∀A,B,C: Type[0].
215  ∀T: A → B → C.
216  ∀p.
217  ∀P: A×B → C → Prop.
218    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
219      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
220
221axiom pair_elim'':
222  ∀A,B,C,C': Type[0].
223  ∀T: A → B → C.
224  ∀T': A → B → C'.
225  ∀p.
226  ∀P: A×B → C → C' → Prop.
227    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
228      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
229
230lemma pair_destruct_1:
231 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
232 #A #B #a #b *; /2/
233qed.
234
235lemma pair_destruct_2:
236 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
237 #A #B #a #b *; /2/
238qed.
239
240
241notation "⊥" with precedence 90
242  for @{ match ? in False with [ ] }.
243
244let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
245  match b with
246    [ true ⇒
247      match c with
248        [ false ⇒ true
249        | true ⇒ false
250        ]
251    | false ⇒
252      match c with
253        [ false ⇒ false
254        | true ⇒ true
255        ]
256    ].
257   
258definition ltb ≝
259  λm, n: nat.
260    leb (S m) n.
261   
262definition geb ≝
263  λm, n: nat.
264    ltb n m.
265
266definition gtb ≝
267  λm, n: nat.
268    leb n m.
269   
270(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
271let rec eq_nat (n: nat) (m: nat) on n: bool ≝
272  match n with
273  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
274  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
275  ].
276
277(* dpm: conflicts with library definitions
278interpretation "Nat less than" 'lt m n = (ltb m n).
279interpretation "Nat greater than" 'gt m n = (gtb m n).
280interpretation "Nat greater than eq" 'geq m n = (geb m n).
281*)
282
283let rec division_aux (m: nat) (n : nat) (p: nat) ≝
284  match ltb n (S p) with
285    [ true ⇒ O
286    | false ⇒
287      match m with
288        [ O ⇒ O
289        | (S q) ⇒ S (division_aux q (n - (S p)) p)
290        ]
291    ].
292   
293definition division ≝
294  λm, n: nat.
295    match n with
296      [ O ⇒ S m
297      | S o ⇒ division_aux m m o
298      ].
299     
300notation "hvbox(n break ÷ m)"
301  right associative with precedence 47
302  for @{ 'division $n $m }.
303 
304interpretation "Nat division" 'division n m = (division n m).
305
306let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
307  match leb n p with
308    [ true ⇒ n
309    | false ⇒
310      match m with
311        [ O ⇒ n
312        | S o ⇒ modulus_aux o (n - (S p)) p
313        ]
314    ].
315   
316definition modulus ≝
317  λm, n: nat.
318    match n with
319      [ O ⇒ m
320      | S o ⇒ modulus_aux m m o
321      ].
322   
323notation "hvbox(n break 'mod' m)"
324  right associative with precedence 47
325  for @{ 'modulus $n $m }.
326 
327interpretation "Nat modulus" 'modulus m n = (modulus m n).
328
329definition divide_with_remainder ≝
330  λm, n: nat.
331    pair ? ? (m ÷ n) (modulus m n).
332   
333let rec exponential (m: nat) (n: nat) on n ≝
334  match n with
335    [ O ⇒ S O
336    | S o ⇒ m * exponential m o
337    ].
338
339interpretation "Nat exponential" 'exp n m = (exponential n m).
340   
341notation "hvbox(a break ⊎ b)"
342 left associative with precedence 50
343for @{ 'disjoint_union $a $b }.
344interpretation "sum" 'disjoint_union A B = (Sum A B).
345
346theorem less_than_or_equal_monotone:
347  ∀m, n: nat.
348    m ≤ n → (S m) ≤ (S n).
349 #m #n #H
350 elim H
351 /2/
352qed.
353
354theorem less_than_or_equal_b_complete:
355  ∀m, n: nat.
356    leb m n = false → ¬(m ≤ n).
357 #m;
358 elim m;
359 normalize
360 [ #n #H
361   destruct
362 | #y #H1 #z
363   cases z
364   normalize
365   [ #H
366     /2/
367   | /3/
368   ]
369 ]
370qed.
371
372theorem less_than_or_equal_b_correct:
373  ∀m, n: nat.
374    leb m n = true → m ≤ n.
375 #m
376 elim m
377 //
378 #y #H1 #z
379 cases z
380 normalize
381 [ #H
382   destruct
383 | #n #H lapply (H1 … H) /2/
384 ]
385qed.
386
387definition less_than_or_equal_b_elim:
388 ∀m, n: nat.
389 ∀P: bool → Type[0].
390   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
391 #m #n #P #H1 #H2;
392 lapply (less_than_or_equal_b_correct m n)
393 lapply (less_than_or_equal_b_complete m n)
394 cases (leb m n)
395 /3/
396qed.
397
398lemma inclusive_disjunction_true:
399  ∀b, c: bool.
400    (orb b c) = true → b = true ∨ c = true.
401  # b
402  # c
403  elim b
404  [ normalize
405    # H
406    @ or_introl
407    %
408  | normalize
409    /2/
410  ]
411qed.
412
413lemma conjunction_true:
414  ∀b, c: bool.
415    andb b c = true → b = true ∧ c = true.
416  # b
417  # c
418  elim b
419  normalize
420  [ /2/
421  | # K
422    destruct
423  ]
424qed.
425
426lemma eq_true_false: false=true → False.
427 # K
428 destruct
429qed.
430
431lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
432 # b
433 cases b
434 %
435qed.
436
437definition bool_to_Prop ≝
438 λb. match b with [ true ⇒ True | false ⇒ False ].
439
440coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
441
442lemma eq_false_to_notb: ∀b. b = false → ¬ b.
443 *; /2/
444qed.
445
446lemma length_append:
447 ∀A.∀l1,l2:list A.
448  |l1 @ l2| = |l1| + |l2|.
449 #A #l1 elim l1
450  [ //
451  | #hd #tl #IH #l2 normalize <IH //]
452qed.
Note: See TracBrowser for help on using the repository browser.