source: Deliverables/D3.3/id-lookup-branch/ASM/Util.ma @ 3341

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

Merge trunk to invariants branch, sorting out the handling of temporaries
in Clight/toCminor.

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    ltb 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.