source: src/ASM/Util.ma @ 1598

Last change on this file since 1598 was 1598, checked in by mulligan, 8 years ago

changes over the last couple of days

File size: 22.3 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 lapply H lapply P cases p //
380qed.
381 
382let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
383  match n return λo. o < length A l → A with
384  [ O ⇒
385    match l return λm. 0 < length A m → A with
386    [ nil ⇒ λabsd1. ?
387    | cons hd tl ⇒ λprf1. hd
388    ]
389  | S n' ⇒
390    match l return λm. S n' < length A m → A with
391    [ nil ⇒ λabsd2. ?
392    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
393    ]
394  ] ?.
395  [ 1:
396    @ p
397  | 4:
398    normalize in prf2;
399    normalize
400    @ le_S_S_to_le
401    assumption
402  | 2:
403    normalize in absd1;
404    cases (not_le_Sn_O O)
405    # H
406    elim (H absd1)
407  | 3:
408    normalize in absd2;
409    cases (not_le_Sn_O (S n'))
410    # H
411    elim (H absd2)
412  ]
413qed.
414 
415let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
416  match n with
417  [ O ⇒
418    match l with
419    [ nil ⇒ [ ]
420    | cons hd tl ⇒ l
421    ]
422  | S n ⇒
423    match l with
424    [ nil ⇒ [ ]
425    | cons hd tl ⇒
426      hd :: nub_by_internal A f (filter ? (λy. notb (f y hd)) tl) n
427    ]
428  ].
429 
430definition nub_by ≝
431  λA: Type[0].
432  λf: A → A → bool.
433  λl: list A.
434    nub_by_internal A f l (length ? l).
435 
436let rec member (A: Type[0]) (eq: A → A → bool) (a: A) (l: list A) on l ≝
437  match l with
438  [ nil ⇒ false
439  | cons hd tl ⇒ orb (eq a hd) (member A eq a tl)
440  ].
441 
442let rec take (A: Type[0]) (n: nat) (l: list A) on n: list A ≝
443  match n with
444  [ O ⇒ [ ]
445  | S n ⇒
446    match l with
447    [ nil ⇒ [ ]
448    | cons hd tl ⇒ hd :: take A n tl
449    ]
450  ].
451 
452let rec drop (A: Type[0]) (n: nat) (l: list A) on n ≝
453  match n with
454  [ O ⇒ l
455  | S n ⇒
456    match l with
457    [ nil ⇒ [ ]
458    | cons hd tl ⇒ drop A n tl
459    ]
460  ].
461 
462definition list_split ≝
463  λA: Type[0].
464  λn: nat.
465  λl: list A.
466    〈take A n l, drop A n l〉.
467 
468let rec mapi_internal (A: Type[0]) (B: Type[0]) (n: nat) (f: nat → A → B)
469                      (l: list A) on l: list B ≝
470  match l with
471  [ nil ⇒ nil ?
472  | cons hd tl ⇒ (f n hd) :: (mapi_internal A B (n + 1) f tl)
473  ]. 
474
475definition mapi ≝
476  λA, B: Type[0].
477  λf: nat → A → B.
478  λl: list A.
479    mapi_internal A B 0 f l.
480
481let rec zip_pottier
482  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B)
483    on left ≝
484  match left with
485  [ nil ⇒ [ ]
486  | cons hd tl ⇒
487    match right with
488    [ nil ⇒ [ ]
489    | cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl'
490    ]
491  ].
492
493let rec zip_safe
494  (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: |left| = |right|)
495    on left ≝
496  match left return λx. |x| = |right| → list (A × B) with
497  [ nil ⇒ λnil_prf.
498    match right return λx. |[ ]| = |x| → list (A × B) with
499    [ nil ⇒ λnil_nil_prf. [ ]
500    | cons hd tl ⇒ λnil_cons_absrd. ?
501    ] nil_prf
502  | cons hd tl ⇒ λcons_prf.
503    match right return λx. |hd::tl| = |x| → list (A × B) with
504    [ nil ⇒ λcons_nil_absrd. ?
505    | cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ?
506    ] cons_prf
507  ] prf.
508  [ 1: normalize in nil_cons_absrd;
509       destruct(nil_cons_absrd)
510  | 2: normalize in cons_nil_absrd;
511       destruct(cons_nil_absrd)
512  | 3: normalize in cons_cons_prf;
513       @injective_S
514       assumption
515  ]
516qed.
517
518let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝
519  match l with
520  [ nil ⇒ Some ? (nil (A × B))
521  | cons hd tl ⇒
522    match r with
523    [ nil ⇒ None ?
524    | cons hd' tl' ⇒
525      match zip ? ? tl tl' with
526      [ None ⇒ None ?
527      | Some tail ⇒ Some ? (〈hd, hd'〉 :: tail)
528      ]
529    ]
530  ].
531
532let rec foldl (A: Type[0]) (B: Type[0]) (f: A → B → A) (a: A) (l: list B) on l ≝
533  match l with
534  [ nil ⇒ a
535  | cons hd tl ⇒ foldl A B f (f a hd) tl
536  ].
537
538lemma foldl_step:
539 ∀A:Type[0].
540  ∀B: Type[0].
541   ∀H: A → B → A.
542    ∀acc: A.
543     ∀pre: list B.
544      ∀hd:B.
545       foldl A B H acc (pre@[hd]) = (H (foldl A B H acc pre) hd).
546 #A #B #H #acc #pre generalize in match acc; -acc; elim pre
547  [ normalize; //
548  | #hd #tl #IH #acc #X normalize; @IH ]
549qed.
550
551lemma foldl_append:
552 ∀A:Type[0].
553  ∀B: Type[0].
554   ∀H: A → B → A.
555    ∀acc: A.
556     ∀suff,pre: list B.
557      foldl A B H acc (pre@suff) = (foldl A B H (foldl A B H acc pre) suff).
558 #A #B #H #acc #suff elim suff
559  [ #pre >append_nil %
560  | #hd #tl #IH #pre whd in ⊢ (???%); <(foldl_step … H ??) applyS (IH (pre@[hd])) ]
561qed.
562
563definition flatten ≝
564  λA: Type[0].
565  λl: list (list A).
566    foldr ? ? (append ?) [ ] l.
567
568let rec rev (A: Type[0]) (l: list A) on l ≝
569  match l with
570  [ nil ⇒ nil A
571  | cons hd tl ⇒ (rev A tl) @ [ hd ]
572  ].
573
574lemma append_length:
575  ∀A: Type[0].
576  ∀l, r: list A.
577    |(l @ r)| = |l| + |r|.
578  #A #L #R
579  elim L
580  [ %
581  | #HD #TL #IH
582    normalize >IH %
583  ]
584qed.
585
586lemma append_nil:
587  ∀A: Type[0].
588  ∀l: list A.
589    l @ [ ] = l.
590  #A #L
591  elim L //
592qed.
593
594lemma rev_append:
595  ∀A: Type[0].
596  ∀l, r: list A.
597    rev A (l @ r) = rev A r @ rev A l.
598  #A #L #R
599  elim L
600  [ normalize >append_nil %
601  | #HD #TL #IH
602    normalize >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 #IH
615    normalize
616    >(append_length A (rev A TL) [HD])
617    normalize /2/
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   
651notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
652 for @{ match $e in bool with [ true ⇒ $t | false ⇒ $f]  }.
653notation < "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
654 for @{ match $e with [ true ⇒ $t | false ⇒ $f]  }.
655
656let rec fold_left_i_aux (A: Type[0]) (B: Type[0])
657                        (f: nat → A → B → A) (x: A) (i: nat) (l: list B) on l ≝
658  match l with
659    [ nil ⇒ x
660    | cons hd tl ⇒ fold_left_i_aux A B f (f i x hd) (S i) tl
661    ].
662
663definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
664
665notation "hvbox(t⌈o ↦ h⌉)"
666  with precedence 45
667  for @{ match (? : $o=$h) with [ refl ⇒ $t ] }.
668
669definition function_apply ≝
670  λA, B: Type[0].
671  λf: A → B.
672  λa: A.
673    f a.
674   
675notation "f break $ x"
676  left associative with precedence 99
677  for @{ 'function_apply $f $x }.
678 
679interpretation "Function application" 'function_apply f x = (function_apply ? ? f x).
680
681let rec iterate (A: Type[0]) (f: A → A) (a: A) (n: nat) on n ≝
682  match n with
683    [ O ⇒ a
684    | S o ⇒ f (iterate A f a o)
685    ].
686
687(* Yeah, I probably ought to do something more general... *)
688notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c\rangle)"
689with precedence 90 for @{ 'triple $a $b $c}.
690interpretation "Triple construction" 'triple x y z = (mk_Prod ? ? (mk_Prod ? ? x y) z).
691
692notation "hvbox(\langle term 19 a, break term 19 b, break term 19 c, break term 19 d\rangle)"
693with precedence 90 for @{ 'quadruple $a $b $c $d}.
694interpretation "Quadruple construction" 'quadruple w x y z = (mk_Prod ? ? (mk_Prod ? ? w x) (mk_Prod ? ? y z)).
695
696notation > "hvbox('let' 〈ident w,ident x,ident y,ident z〉 ≝ t 'in' s)"
697 with precedence 10
698for @{ 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 ] ] ] }.
699
700notation > "hvbox('let' 〈ident x,ident y,ident z〉 ≝ t 'in' s)"
701 with precedence 10
702for @{ match $t with [ pair ${fresh xy} ${ident z} ⇒ match ${fresh xy} with [ pair ${ident x} ${ident y} ⇒ $s ] ] }.
703
704notation < "hvbox('let' \nbsp hvbox(〈ident x,ident y〉\nbsp ≝ break t \nbsp 'in' \nbsp) break s)"
705 with precedence 10
706for @{ match $t with [ pair (${ident x}:$ignore) (${ident y}:$ignora) ⇒ $s ] }.
707
708axiom pair_elim':
709  ∀A,B,C: Type[0].
710  ∀T: A → B → C.
711  ∀p.
712  ∀P: A×B → C → Prop.
713    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt)) →
714      P p (let 〈lft, rgt〉 ≝ p in T lft rgt).
715
716axiom pair_elim'':
717  ∀A,B,C,C': Type[0].
718  ∀T: A → B → C.
719  ∀T': A → B → C'.
720  ∀p.
721  ∀P: A×B → C → C' → Prop.
722    (∀lft, rgt. p = 〈lft,rgt〉 → P 〈lft,rgt〉 (T lft rgt) (T' lft rgt)) →
723      P p (let 〈lft, rgt〉 ≝ p in T lft rgt) (let 〈lft, rgt〉 ≝ p in T' lft rgt).
724
725lemma pair_destruct_1:
726 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c.
727 #A #B #a #b *; /2/
728qed.
729
730lemma pair_destruct_2:
731 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c.
732 #A #B #a #b *; /2/
733qed.
734
735
736let rec exclusive_disjunction (b: bool) (c: bool) on b ≝
737  match b with
738    [ true ⇒
739      match c with
740        [ false ⇒ true
741        | true ⇒ false
742        ]
743    | false ⇒
744      match c with
745        [ false ⇒ false
746        | true ⇒ true
747        ]
748    ].
749
750(* dpm: conflicts with library definitions
751interpretation "Nat less than" 'lt m n = (ltb m n).
752interpretation "Nat greater than" 'gt m n = (gtb m n).
753interpretation "Nat greater than eq" 'geq m n = (geb m n).
754*)
755
756let rec division_aux (m: nat) (n : nat) (p: nat) ≝
757  match ltb n (S p) with
758    [ true ⇒ O
759    | false ⇒
760      match m with
761        [ O ⇒ O
762        | (S q) ⇒ S (division_aux q (n - (S p)) p)
763        ]
764    ].
765   
766definition division ≝
767  λm, n: nat.
768    match n with
769      [ O ⇒ S m
770      | S o ⇒ division_aux m m o
771      ].
772     
773notation "hvbox(n break ÷ m)"
774  right associative with precedence 47
775  for @{ 'division $n $m }.
776 
777interpretation "Nat division" 'division n m = (division n m).
778
779let rec modulus_aux (m: nat) (n: nat) (p: nat) ≝
780  match leb n p with
781    [ true ⇒ n
782    | false ⇒
783      match m with
784        [ O ⇒ n
785        | S o ⇒ modulus_aux o (n - (S p)) p
786        ]
787    ].
788   
789definition modulus ≝
790  λm, n: nat.
791    match n with
792      [ O ⇒ m
793      | S o ⇒ modulus_aux m m o
794      ].
795   
796notation "hvbox(n break 'mod' m)"
797  right associative with precedence 47
798  for @{ 'modulus $n $m }.
799 
800interpretation "Nat modulus" 'modulus m n = (modulus m n).
801
802definition divide_with_remainder ≝
803  λm, n: nat.
804    mk_Prod … (m ÷ n) (modulus m n).
805   
806let rec exponential (m: nat) (n: nat) on n ≝
807  match n with
808    [ O ⇒ S O
809    | S o ⇒ m * exponential m o
810    ].
811
812interpretation "Nat exponential" 'exp n m = (exponential n m).
813   
814notation "hvbox(a break ⊎ b)"
815 left associative with precedence 50
816for @{ 'disjoint_union $a $b }.
817interpretation "sum" 'disjoint_union A B = (Sum A B).
818
819theorem less_than_or_equal_monotone:
820  ∀m, n: nat.
821    m ≤ n → (S m) ≤ (S n).
822 #m #n #H
823 elim H
824 /2/
825qed.
826
827theorem less_than_or_equal_b_complete:
828  ∀m, n: nat.
829    leb m n = false → ¬(m ≤ n).
830 #m;
831 elim m;
832 normalize
833 [ #n #H
834   destruct
835 | #y #H1 #z
836   cases z
837   normalize
838   [ #H
839     /2/
840   | /3/
841   ]
842 ]
843qed.
844
845theorem less_than_or_equal_b_correct:
846  ∀m, n: nat.
847    leb m n = true → m ≤ n.
848 #m
849 elim m
850 //
851 #y #H1 #z
852 cases z
853 normalize
854 [ #H
855   destruct
856 | #n #H lapply (H1 … H) /2/
857 ]
858qed.
859
860definition less_than_or_equal_b_elim:
861 ∀m, n: nat.
862 ∀P: bool → Type[0].
863   (m ≤ n → P true) → (¬(m ≤ n) → P false) → P (leb m n).
864 #m #n #P #H1 #H2;
865 lapply (less_than_or_equal_b_correct m n)
866 lapply (less_than_or_equal_b_complete m n)
867 cases (leb m n)
868 /3/
869qed.
870
871lemma inclusive_disjunction_true:
872  ∀b, c: bool.
873    (orb b c) = true → b = true ∨ c = true.
874  # b
875  # c
876  elim b
877  [ normalize
878    # H
879    @ or_introl
880    %
881  | normalize
882    /2/
883  ]
884qed.
885
886lemma conjunction_true:
887  ∀b, c: bool.
888    andb b c = true → b = true ∧ c = true.
889  # b
890  # c
891  elim b
892  normalize
893  [ /2/
894  | # K
895    destruct
896  ]
897qed.
898
899lemma eq_true_false: false=true → False.
900 # K
901 destruct
902qed.
903
904lemma inclusive_disjunction_b_true: ∀b. orb b true = true.
905 # b
906 cases b
907 %
908qed.
909
910definition bool_to_Prop ≝
911 λb. match b with [ true ⇒ True | false ⇒ False ].
912
913coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].
914
915lemma eq_false_to_notb: ∀b. b = false → ¬ b.
916 *; /2/
917qed.
918
919lemma length_append:
920 ∀A.∀l1,l2:list A.
921  |l1 @ l2| = |l1| + |l2|.
922 #A #l1 elim l1
923  [ //
924  | #hd #tl #IH #l2 normalize <IH //]
925qed.
Note: See TracBrowser for help on using the repository browser.