source: src/ASM/Util.ma @ 1062

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

separated jmeq and coercions from foldstuff.ma in order to fix the ongoing mess in util.ma surrounding reduce_strong

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