source: src/ASM/Util.ma @ 1071

Last change on this file since 1071 was 1071, checked in by mulligan, 8 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.