source: src/ASM/Util.ma @ 1094

Last change on this file since 1094 was 1094, checked in by mulligan, 8 years ago

some changes from today to do with liveness analyses

File size: 21.6 KB
Line 
1include "basics/list.ma".
2include "basics/types.ma".
3include "arithmetics/nat.ma".
4
5include "ASM/JMCoercions.ma".
6
7(* let's implement a daemon not used by automation *)
8inductive DAEMONXXX: Type[0] ≝ K1DAEMONXXX: DAEMONXXX | K2DAEMONXXX: DAEMONXXX.
9axiom IMPOSSIBLE: K1DAEMONXXX = K2DAEMONXXX.
10example daemon: False. generalize in match IMPOSSIBLE; #IMPOSSIBLE destruct(IMPOSSIBLE) qed.
11example not_implemented: False. cases daemon qed.
12
13notation > "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
14 with precedence 10
15for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
16
17definition ltb ≝
18  λm, n: nat.
19    leb (S m) n.
20   
21definition geb ≝
22  λm, n: nat.
23    ltb n m.
24
25definition gtb ≝
26  λm, n: nat.
27    leb n m.
28
29(* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)
30let rec eq_nat (n: nat) (m: nat) on n: bool ≝
31  match n with
32  [ O ⇒ match m with [ O ⇒ true | _ ⇒ false ]
33  | S n' ⇒ match m with [ S m' ⇒ eq_nat n' m' | _ ⇒ false ]
34  ].
35
36let rec prefix
37  (A: Type[0]) (k: nat) (l: list A)
38    on l ≝
39  match l with
40  [ nil ⇒ [ ]
41  | cons hd tl ⇒
42    match k with
43    [ O ⇒ [ ]
44    | S k' ⇒ hd :: prefix A k' tl
45    ]
46  ].
47 
48let rec fold_left2
49  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A)
50  (left: list B) (right: list C) (proof: |left| = |right|)
51    on left: A ≝
52  match left return λx. |x| = |right| → A with
53  [ nil ⇒ λnil_prf.
54    match right return λx. |[ ]| = |x| → A with
55    [ nil ⇒ λnil_nil_prf. accu
56    | cons hd tl ⇒ λcons_nil_absrd. ?
57    ] nil_prf
58  | cons hd tl ⇒ λcons_prf.
59    match right return λx. |hd::tl| = |x| → A with
60    [ nil ⇒ λcons_nil_absrd. ?
61    | cons hd' tl' ⇒ λcons_cons_prf.
62        fold_left2 …  f (f accu hd hd') tl tl' ?
63    ] cons_prf
64  ] proof.
65  [ 1: normalize in cons_nil_absrd;
66       destruct(cons_nil_absrd)
67  | 2: normalize in cons_nil_absrd;
68       destruct(cons_nil_absrd)
69  | 3: normalize in cons_cons_prf;
70       @injective_S
71       assumption
72  ]
73qed.
74
75let rec remove_n_first_internal
76  (i: nat) (A: Type[0]) (l: list A) (n: nat)
77    on l ≝
78  match l with
79  [ nil ⇒ [ ]
80  | cons hd tl ⇒
81    match eq_nat i n with
82    [ true ⇒ l
83    | _ ⇒ remove_n_first_internal (S i) A tl n
84    ]
85  ].
86
87definition remove_n_first ≝
88  λA: Type[0].
89  λn: nat.
90  λl: list A.
91    remove_n_first_internal 0 A l n.
92   
93let rec foldi_from_until_internal
94  (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A)
95    on rem ≝
96  match rem with
97  [ nil ⇒ res
98  | cons e tl ⇒
99    match geb i m with
100    [ true ⇒ res
101    | _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f
102    ]
103  ].
104
105definition foldi_from_until ≝
106  λA: Type[0].
107  λn: nat.
108  λm: nat.
109  λf: ?.
110  λa: ?.
111  λl: ?.
112    foldi_from_until_internal A 0 a (remove_n_first A n l) m f.
113
114definition foldi_from ≝
115  λA: Type[0].
116  λn.
117  λf.
118  λa.
119  λl.
120    foldi_from_until A n (|l|) f a l.
121
122definition foldi_until ≝
123  λA: Type[0].
124  λm.
125  λf.
126  λa.
127  λl.
128    foldi_from_until A 0 m f a l.
129
130definition foldi ≝
131  λA: Type[0].
132  λf.
133  λa.
134  λl.
135    foldi_from_until A 0 (|l|) f a l.
136
137definition hd_safe ≝
138  λA: Type[0].
139  λl: list A.
140  λproof: 0 < |l|.
141  match l return λx. 0 < |x| → A with
142  [ nil ⇒ λnil_absrd. ?
143  | cons hd tl ⇒ λcons_prf. hd
144  ] proof.
145  normalize in nil_absrd;
146  cases(not_le_Sn_O 0)
147  #HYP
148  cases(HYP nil_absrd)
149qed.
150
151definition tail_safe ≝
152  λA: Type[0].
153  λl: list A.
154  λproof: 0 < |l|.
155  match l return λx. 0 < |x| → list A with
156  [ nil ⇒ λnil_absrd. ?
157  | cons hd tl ⇒ λcons_prf. tl
158  ] proof.
159  normalize in nil_absrd;
160  cases(not_le_Sn_O 0)
161  #HYP
162  cases(HYP nil_absrd)
163qed.
164
165let rec split
166  (A: Type[0]) (l: list A) (index: nat) (proof: index ≤ |l|)
167    on index ≝
168  match index return λx. x ≤ |l| → (list A) × (list A) with
169  [ O ⇒ λzero_prf. 〈[], l〉
170  | S index' ⇒ λsucc_prf.
171    match l return λx. S index' ≤ |x| → (list A) × (list A) with
172    [ nil ⇒ λnil_absrd. ?
173    | cons hd tl ⇒ λcons_prf.
174      let 〈l1, l2〉 ≝ split A tl index' ? in
175        〈hd :: l1, l2〉
176    ] succ_prf
177  ] proof.
178  [1: normalize in nil_absrd;
179      cases(not_le_Sn_O index')
180      #HYP
181      cases(HYP nil_absrd)
182  |2: normalize in cons_prf;
183      @le_S_S_to_le
184      assumption
185  ]
186qed.
187
188let rec nth_safe
189  (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
190  (proof: index < | the_list |)
191    on index ≝
192  match index return λs. s < | the_list | → elt_type with
193  [ O ⇒
194    match the_list return λt. 0 < | t | → elt_type with
195    [ nil        ⇒ λnil_absurd. ?
196    | cons hd tl ⇒ λcons_proof. hd
197    ]
198  | S index' ⇒
199    match the_list return λt. S index' < | t | → elt_type with
200    [ nil ⇒ λnil_absurd. ?
201    | cons hd tl ⇒
202      λcons_proof. nth_safe elt_type index' tl ?
203    ]
204  ] proof.
205  [ normalize in nil_absurd;
206    cases (not_le_Sn_O 0)
207    #ABSURD
208    elim (ABSURD nil_absurd)
209  | normalize in nil_absurd;
210    cases (not_le_Sn_O (S index'))
211    #ABSURD
212    elim (ABSURD nil_absurd)
213  | normalize in cons_proof
214    @le_S_S_to_le
215    assumption
216  ]
217qed.
218
219definition last_safe ≝
220  λelt_type: Type[0].
221  λthe_list: list elt_type.
222  λproof   : 0 < | the_list |.
223    nth_safe elt_type (|the_list| - 1) the_list ?.
224  normalize /2/
225qed.
226
227let rec reduce
228  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝
229  match left with
230  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
231  | cons hd tl ⇒
232    match right with
233    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
234    | cons hd' tl' ⇒
235      let 〈cleft, cright〉 ≝ reduce A B tl tl' in
236      let 〈commonl, restl〉 ≝ cleft in
237      let 〈commonr, restr〉 ≝ cright in
238        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
239    ]
240  ].
241
242(*
243axiom reduce_strong:
244  ∀A: Type[0].
245  ∀left: list A.
246  ∀right: list A.
247    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
248*)
249
250let rec reduce_strong
251  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
252    on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). |\fst (\fst ret)| = |\fst (\snd ret)|  ≝
253  match left with
254  [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉
255  | cons hd tl ⇒
256    match right with
257    [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉
258    | cons hd' tl' ⇒
259      let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in
260      let 〈commonl, restl〉 ≝ cleft in
261      let 〈commonr, restr〉 ≝ cright in
262        〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉
263    ]
264  ].
265  [ 1: normalize %
266  | 2: normalize %
267  | 3: normalize
268       generalize in match (sig2 … (reduce_strong A B tl tl1));
269       >p2 >p3 >p4 normalize in ⊢ (% → ?)
270       #HYP //
271  ]
272qed.
273   
274let rec map2_opt
275  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
276  (left: list A) (right: list B) on left ≝
277  match left with
278  [ nil ⇒
279    match right with
280    [ nil ⇒ Some ? (nil C)
281    | _ ⇒ None ?
282    ]
283  | cons hd tl ⇒
284    match right with
285    [ nil ⇒ None ?
286    | cons hd' tl' ⇒
287      match map2_opt A B C f tl tl' with
288      [ None ⇒ None ?
289      | Some tail ⇒ Some ? (f hd hd' :: tail)
290      ]
291    ]
292  ].
293
294let rec map2
295  (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C)
296  (left: list A) (right: list B) (proof: | left | = | right |) on left ≝
297  match left return λx. | x | = | right | → list C with
298  [ nil ⇒
299    match right return λy. | [] | = | y | → list C with
300    [ nil ⇒ λnil_prf. nil C
301    | _ ⇒ λcons_absrd. ?
302    ]
303  | cons hd tl ⇒
304    match right return λy. | hd::tl | = | y | → list C with
305    [ nil ⇒ λnil_absrd. ?
306    | cons hd' tl' ⇒ λcons_prf. (f hd hd') :: map2 A B C f tl tl' ?
307    ]
308  ] proof.
309  [1: normalize in cons_absrd;
310      destruct(cons_absrd)
311  |2: normalize in nil_absrd;
312      destruct(nil_absrd)
313  |3: normalize in cons_prf;
314      destruct(cons_prf)
315      assumption
316  ]
317qed.
318
319let rec map3
320  (A: Type[0]) (B: Type[0]) (C: Type[0]) (D: Type[0]) (f: A → B → C → D)
321  (left: list A) (centre: list B) (right: list C)
322  (prflc: |left| = |centre|) (prfcr: |centre| = |right|) on left ≝
323  match left return λx. |x| = |centre| → list D with
324  [ nil ⇒ λnil_prf.
325    match centre return λx. |x| = |right| → list D with
326    [ nil ⇒ λnil_nil_prf.
327      match right return λx. |nil ?| = |x| → list D with
328      [ nil        ⇒ λnil_nil_nil_prf. nil D
329      | cons hd tl ⇒ λcons_nil_nil_absrd. ?
330      ] nil_nil_prf
331    | cons hd tl ⇒ λnil_cons_absrd. ?
332    ] prfcr
333  | cons hd tl ⇒ λcons_prf.
334    match centre return λx. |x| = |right| → list D with
335    [ nil ⇒ λcons_nil_absrd. ?
336    | cons hd' tl' ⇒ λcons_cons_prf.
337      match right return λx. |right| = |x| → |cons ? hd' tl'| = |x| → list D with
338      [ nil ⇒ λrefl_prf. λcons_cons_nil_absrd. ?
339      | cons hd'' tl'' ⇒ λrefl_prf. λcons_cons_cons_prf.
340        (f hd hd' hd'') :: (map3 A B C D f tl tl' tl'' ? ?)
341      ] (refl ? (|right|)) cons_cons_prf
342    ] prfcr
343  ] prflc.
344  [ 1: normalize in cons_nil_nil_absrd;
345       destruct(cons_nil_nil_absrd)
346  | 2: generalize in match nil_cons_absrd;
347       <prfcr <nil_prf #HYP
348       normalize in HYP;
349       destruct(HYP)
350  | 3: generalize in match cons_nil_absrd;
351       <prfcr <cons_prf #HYP
352       normalize in HYP;
353       destruct(HYP)
354  | 4: normalize in cons_cons_nil_absrd;
355       destruct(cons_cons_nil_absrd)
356  | 5: normalize in cons_cons_cons_prf;
357       destruct(cons_cons_cons_prf)
358       assumption
359  | 6: generalize in match cons_cons_cons_prf;
360       <refl_prf <prfcr <cons_prf #HYP
361       normalize in HYP;
362       destruct(HYP)
363       @sym_eq assumption
364  ]
365qed.
366 
367lemma eq_rect_Type0_r :
368  ∀A: Type[0].
369  ∀a:A.
370  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
371  #A #a #P #H #x #p
372  generalize in match H
373  generalize in match P
374  cases p
375  //
376qed.
377 
378let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
379  match n return λo. o < length A l → A with
380  [ O ⇒
381    match l return λm. 0 < length A m → A with
382    [ nil ⇒ λabsd1. ?
383    | cons hd tl ⇒ λprf1. hd
384    ]
385  | S n' ⇒
386    match l return λm. S n' < length A m → A with
387    [ nil ⇒ λabsd2. ?
388    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
389    ]
390  ] ?.
391  [ 1:
392    @ p
393  | 4:
394    normalize in prf2
395    normalize
396    @ le_S_S_to_le
397    assumption
398  | 2:
399    normalize in absd1;
400    cases (not_le_Sn_O O)
401    # H
402    elim (H absd1)
403  | 3:
404    normalize in absd2;
405    cases (not_le_Sn_O (S n'))
406    # H
407    elim (H absd2)
408  ]
409qed.
410 
411let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
412  match n with
413  [ O ⇒
414    match l with
415    [ nil ⇒ [ ]
416    | cons hd tl ⇒ l
417    ]
418  | S n ⇒
419    match l with
420    [ nil ⇒ [ ]
421    | cons hd tl ⇒
422      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
423    ]
424  ].
425 
426definition nub_by ≝
427  λA: Type[0].
428  λf: A → A → bool.
429  λl: list A.
430    nub_by_internal A f l (length ? l).
431 
432let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
433  match l with
434  [ nil ⇒ false
435  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
436  ].
437 
438let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
439  match n with
440  [ O ⇒ [ ]
441  | S n ⇒
442    match l with
443    [ nil ⇒ [ ]
444    | cons hd tl ⇒ hd :: take A n tl
445    ]
446  ].
447 
448let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
449  match n with
450  [ O ⇒ l
451  | S n ⇒
452    match l with
453    [ nil ⇒ [ ]
454    | cons hd tl ⇒ drop A n tl
455    ]
456  ].
457 
458definition list_split ≝
459  λA: Type[0].
460  λn: nat.
461  λl: list A.
462    〈take A n l, drop A n l〉.
463 
464let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
465                      (l: list A) on l: list B ≝
466  match l with
467  [ nil ⇒ nil ?
468  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
469  ]. 
470
471definition mapi ≝
472  λA, B: Type[0].
473  λf: nat → A → B.
474  λl: list A.
475    mapi_internal A B 0 f l.
476
477let rec zip_pottier
478  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
479    on left ≝
480  match left with
481  [ nil ⇒ [ ]
482  | cons hd tl ⇒
483    match right with
484    [ nil ⇒ [ ]
485    | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
486    ]
487  ].
488
489let rec zip_safe
490  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
491    on left ≝
492  match left return λx. |x| = |right| → list (A × B) with
493  [ nil ⇒ λnil_prf.
494    match right return λx. |[ ]| = |x| → list (A × B) with
495    [ nil ⇒ λnil_nil_prf. [ ]
496    | cons hd tl ⇒ λnil_cons_absrd. ?
497    ] nil_prf
498  | cons hd tl ⇒ λcons_prf.
499    match right return λx. |hd::tl| = |x| → list (A × B) with
500    [ nil ⇒ λcons_nil_absrd. ?
501    | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
502    ] cons_prf
503  ] prf.
504  [ 1: normalize in nil_cons_absrd;
505       destruct(nil_cons_absrd)
506  | 2: normalize in cons_nil_absrd;
507       destruct(cons_nil_absrd)
508  | 3: normalize in cons_cons_prf;
509       @injective_S
510       assumption
511  ]
512qed.
513
514let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
515  match l with
516  [ nil ⇒ Some ? (nil (A × B))
517  | cons hd tl ⇒
518    match r with
519    [ nil ⇒ None ?
520    | cons hd' tl' ⇒
521      match zip ? ? tl tl' with
522      [ None ⇒ None ?
523      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
524      ]
525    ]
526  ].
527
528let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
529  match l with
530  [ nil ⇒ a
531  | cons hd tl ⇒ foldl A B f (f a hd) tl
532  ].
533
534lemma foldl_step:
535 ∀A:Type[0].
536  ∀B: Type[0].
537   ∀H: A → B → A.
538    ∀acc: A.
539     ∀pre: list B.
540      ∀hd:B.
541       foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
542 #A #B #H #acc #pre generalize in match acc; -acc; elim pre
543  [ normalize; //
544  | #hd #tl #IH #acc #X normalize; @IH ]
545qed.
546
547lemma foldl_append:
548 ∀A:Type[0].
549  ∀B: Type[0].
550   ∀H: A → B → A.
551    ∀acc: A.
552     ∀suff,pre: list B.
553      foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
554 #A #B #H #acc #suff elim suff
555  [ #pre >append_nil %
556  | #hd #tl #IH #pre whd in ⊢ (???%) <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
557qed.
558
559definition flatten ≝
560  λA: Type[0].
561  λl: list (list A).
562    foldr ? ? (append ?) [ ] l.
563
564let rec rev (A: Type[0]) (l: list A) on l ≝
565  match l with
566  [ nil ⇒ nil A
567  | cons hd tl ⇒ (rev A tl) @ [ hd ]
568  ].
569
570lemma append_length:
571  ∀A: Type[0].
572  ∀l, r: list A.
573    |(l @ r)| = |l| + |r|.
574  #A #L #R
575  elim L
576  [ %
577  | #HD #TL #IH
578    normalize >IH %
579  ]
580qed.
581
582lemma append_nil:
583  ∀A: Type[0].
584  ∀l: list A.
585    l @ [ ] = l.
586  #A #L
587  elim L //
588qed.
589
590lemma rev_append:
591  ∀A: Type[0].
592  ∀l, r: list A.
593    rev A (l @ r) = rev A r @ rev A l.
594  #A #L #R
595  elim L
596  [ normalize >append_nil %
597  | #HD #TL #IH
598    normalize >IH
599    @associative_append
600  ]
601qed.
602
603lemma rev_length:
604  ∀A: Type[0].
605  ∀l: list A.
606    |rev A l| = |l|.
607  #A #L
608  elim L
609  [ %
610  | #HD #TL #IH
611    normalize
612    >(append_length A (rev A TL) [HD])
613    normalize /2/
614  ]
615qed.
616   
617notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
618 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
619notation < "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
620 for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
621
622let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
623                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
624  match l with
625    [ nil ⇒ x
626    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
627    ].
628
629definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
630
631notation "hvbox(t⌈o ↦ h⌉)"
632  with precedence 45
633  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
634
635definition function_apply ≝
636  λA, B: Type[0].
637  λf: A → B.
638  λa: A.
639    f a.
640   
641notation "f break $ x"
642  left associative with precedence 99
643  for @{ 'function_apply $f $x }.
644 
645interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
646
647let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
648  match n with
649    [ O ⇒ a
650    | S o ⇒ f (iterate A f a o)
651    ].
652
653(* Yeah, I probably ought to do something more general... *)
654notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
655with precedence 90 for @{ 'triple $a $b $c}.
656interpretation "Triple construction" 'triple x y z = (pair ? ? (pair ? ? x y) z).
657
658notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
659with precedence 90 for @{ 'quadruple $a $b $c $d}.
660interpretation "Quadruple construction" 'quadruple w x y z = (pair ? ? (pair ? ? w x) (pair ? ? y z)).
661
662notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
663 with precedence 10
664for @{ 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 ] ] ] }.
665
666notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
667 with precedence 10
668for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
669
670notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
671 with precedence 10
672for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
673
674axiom pair_elim':
675  ∀A,B,C: Type[0].
676  ∀T: A → B → C.
677  ∀p.
678  ∀P: A×B → C → Prop.
679    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
680      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
681
682axiom pair_elim'':
683  ∀A,B,C,C': Type[0].
684  ∀T: A → B → C.
685  ∀T': A → B → C'.
686  ∀p.
687  ∀P: A×B → C → C' → Prop.
688    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
689      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
690
691lemma pair_destruct_1:
692 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
693 #A #B #a #b *; /2/
694qed.
695
696lemma pair_destruct_2:
697 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
698 #A #B #a #b *; /2/
699qed.
700
701
702notation "⊥" with precedence 90
703  for @{ match ? in False with [ ] }.
704
705let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
706  match b with
707    [ true ⇒
708      match c with
709        [ false ⇒ true
710        | true ⇒ false
711        ]
712    | false ⇒
713      match c with
714        [ false ⇒ false
715        | true ⇒ true
716        ]
717    ].
718
719(* dpm: conflicts with library definitions
720interpretation "Nat less than" 'lt m n = (ltb m n).
721interpretation "Nat greater than" 'gt m n = (gtb m n).
722interpretation "Nat greater than eq" 'geq m n = (geb m n).
723*)
724
725let rec division_aux (m: nat) (n : nat) (p: nat) ≝
726  match ltb n (S p) with
727    [ true ⇒ O
728    | false ⇒
729      match m with
730        [ O ⇒ O
731        | (S q) ⇒ S (division_aux q (n - (S p)) p)
732        ]
733    ].
734   
735definition division ≝
736  λm, n: nat.
737    match n with
738      [ O ⇒ S m
739      | S o ⇒ division_aux m m o
740      ].
741     
742notation "hvbox(n break ÷ m)"
743  right associative with precedence 47
744  for @{ 'division $n $m }.
745 
746interpretation "Nat division" 'division n m = (division n m).
747
748let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
749  match leb n p with
750    [ true ⇒ n
751    | false ⇒
752      match m with
753        [ O ⇒ n
754        | S o ⇒ modulus_aux o (n - (S p)) p
755        ]
756    ].
757   
758definition modulus ≝
759  λm, n: nat.
760    match n with
761      [ O ⇒ m
762      | S o ⇒ modulus_aux m m o
763      ].
764   
765notation "hvbox(n break 'mod' m)"
766  right associative with precedence 47
767  for @{ 'modulus $n $m }.
768 
769interpretation "Nat modulus" 'modulus m n = (modulus m n).
770
771definition divide_with_remainder ≝
772  λm, n: nat.
773    pair ? ? (m ÷ n) (modulus m n).
774   
775let rec exponential (m: nat) (n: nat) on n ≝
776  match n with
777    [ O ⇒ S O
778    | S o ⇒ m * exponential m o
779    ].
780
781interpretation "Nat exponential" 'exp n m = (exponential n m).
782   
783notation "hvbox(a break ⊎ b)"
784 left associative with precedence 50
785for @{ 'disjoint_union $a $b }.
786interpretation "sum" 'disjoint_union A B = (Sum A B).
787
788theorem less_than_or_equal_monotone:
789  ∀m, n: nat.
790    m ≤ n → (S m) ≤ (S n).
791 #m #n #H
792 elim H
793 /2/
794qed.
795
796theorem less_than_or_equal_b_complete:
797  ∀m, n: nat.
798    leb m n = false → ¬(m ≤ n).
799 #m;
800 elim m;
801 normalize
802 [ #n #H
803   destruct
804 | #y #H1 #z
805   cases z
806   normalize
807   [ #H
808     /2/
809   | /3/
810   ]
811 ]
812qed.
813
814theorem less_than_or_equal_b_correct:
815  ∀m, n: nat.
816    leb m n = true → m ≤ n.
817 #m
818 elim m
819 //
820 #y #H1 #z
821 cases z
822 normalize
823 [ #H
824   destruct
825 | #n #H lapply (H1 … H) /2/
826 ]
827qed.
828
829definition less_than_or_equal_b_elim:
830 ∀m, n: nat.
831 ∀P: bool → Type[0].
832   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
833 #m #n #P #H1 #H2;
834 lapply (less_than_or_equal_b_correct m n)
835 lapply (less_than_or_equal_b_complete m n)
836 cases (leb m n)
837 /3/
838qed.
839
840lemma inclusive_disjunction_true:
841  ∀b, c: bool.
842    (orb b c) = true → b = true ∨ c = true.
843  # b
844  # c
845  elim b
846  [ normalize
847    # H
848    @ or_introl
849    %
850  | normalize
851    /2/
852  ]
853qed.
854
855lemma conjunction_true:
856  ∀b, c: bool.
857    andb b c = true → b = true ∧ c = true.
858  # b
859  # c
860  elim b
861  normalize
862  [ /2/
863  | # K
864    destruct
865  ]
866qed.
867
868lemma eq_true_false: false=true → False.
869 # K
870 destruct
871qed.
872
873lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
874 # b
875 cases b
876 %
877qed.
878
879definition bool_to_Prop ≝
880 λb. match b with [ true ⇒ True | false ⇒ False ].
881
882coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
883
884lemma eq_false_to_notb: ∀b. b = false → ¬ b.
885 *; /2/
886qed.
887
888lemma length_append:
889 ∀A.∀l1,l2:list A.
890  |l1 @ l2| = |l1| + |l2|.
891 #A #l1 elim l1
892  [ //
893  | #hd #tl #IH #l2 normalize <IH //]
894qed.
Note: See TracBrowser for help on using the repository browser.