source: src/ASM/Util.ma @ 1063

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

changes from today

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