source: src/ASM/Util.ma @ 1064

Last change on this file since 1064 was 1064, checked in by mulligan, 9 years ago

changes from today, nearly complete rtlabs translation pass

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