source: src/ASM/Util.ma @ 1323

Last change on this file since 1323 was 1323, checked in by campbell, 8 years ago

Reduce number of notations for destructive let on pairs to one.

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