source: src/ASM/Util.ma @ 1075

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

nearly completed rtl -> ertl pass removing all option types with dep. types

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