source: src/ASM/Util.ma @ 1882

Last change on this file since 1882 was 1882, checked in by tranquil, 8 years ago

big update, alas incomplete:
joint changed a bit, and all BE languages need to be updated
started development of blocks to aid preservation results, but still incomplete
if it breaks too many things, feel free to roll back

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