source: src/ASM/Util.ma @ 998

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

Half repaired, half broken. Most functions no longer return option types,
taking in input dependent types.

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