source: src/ASM/Util.ma @ 1071

Last change on this file since 1071 was 1071, checked in by mulligan, 10 years ago

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

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