source: src/ASM/Util.ma @ 1228

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

work on colouring algorithm halted as it can be axiomatised. now implementing interference graphs (objects!)

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