[766] | 1 | include "basics/list.ma". |
---|
| 2 | |
---|
| 3 | let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝ |
---|
| 4 | match l with |
---|
| 5 | [ nil ⇒ None ? |
---|
| 6 | | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ] |
---|
| 7 | ]. |
---|
[780] | 8 | |
---|
[816] | 9 | let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ |
---|
| 10 | match l with |
---|
[1087] | 11 | [ nil ⇒ True |
---|
[816] | 12 | | cons h t ⇒ P h ∧ All A P t |
---|
| 13 | ]. |
---|
| 14 | |
---|
[1087] | 15 | lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l. |
---|
| 16 | #A #P #Q #H #l elim l normalize // |
---|
| 17 | #h #t #IH * /3/ |
---|
| 18 | qed. |
---|
| 19 | |
---|
[1105] | 20 | lemma All_nth : ∀A,P,n,l. |
---|
| 21 | All A P l → |
---|
| 22 | ∀a. |
---|
| 23 | nth_opt A n l = Some A a → |
---|
| 24 | P a. |
---|
| 25 | #A #P #n elim n |
---|
| 26 | [ * [ #_ #a #E whd in E:(??%?); destruct |
---|
| 27 | | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H |
---|
| 28 | ] |
---|
| 29 | | #m #IH * |
---|
| 30 | [ #_ #a #E whd in E:(??%?); destruct |
---|
| 31 | | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?) @IH |
---|
| 32 | ] |
---|
| 33 | ] qed. |
---|
| 34 | |
---|
[780] | 35 | let rec exists (A:Type[0]) (p:A → bool) (l:list A) on l : bool ≝ |
---|
| 36 | match l with |
---|
| 37 | [ nil ⇒ false |
---|
| 38 | | cons h t ⇒ orb (p h) (exists A p t) |
---|
[1087] | 39 | ]. |
---|
| 40 | |
---|
| 41 | let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ |
---|
| 42 | match l with |
---|
| 43 | [ nil ⇒ False |
---|
| 44 | | cons h t ⇒ (P h) ∨ (Exists A P t) |
---|
| 45 | ]. |
---|
| 46 | |
---|
| 47 | lemma Exists_append : ∀A,P,l1,l2. |
---|
| 48 | Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2. |
---|
| 49 | #A #P #l1 elim l1 |
---|
| 50 | [ normalize /2/ |
---|
| 51 | | #h #t #IH #l2 * |
---|
| 52 | [ #H /3/ |
---|
| 53 | | #H cases (IH l2 H) /3/ |
---|
| 54 | ] |
---|
| 55 | ] qed. |
---|
| 56 | |
---|
[1102] | 57 | lemma Exists_append_l : ∀A,P,l1,l2. |
---|
| 58 | Exists A P l1 → Exists A P (l1@l2). |
---|
| 59 | #A #P #l1 #l2 elim l1 |
---|
| 60 | [ * |
---|
| 61 | | #h #t #IH * |
---|
| 62 | [ #H %1 @H |
---|
| 63 | | #H %2 @IH @H |
---|
| 64 | ] |
---|
| 65 | ] qed. |
---|
| 66 | |
---|
| 67 | lemma Exists_append_r : ∀A,P,l1,l2. |
---|
| 68 | Exists A P l2 → Exists A P (l1@l2). |
---|
| 69 | #A #P #l1 #l2 elim l1 |
---|
| 70 | [ #H @H |
---|
| 71 | | #h #t #IH #H %2 @IH @H |
---|
| 72 | ] qed. |
---|
| 73 | |
---|
| 74 | lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2). |
---|
| 75 | #A #P #l1 #x #l2 elim l1 |
---|
| 76 | [ normalize #H %2 @H |
---|
| 77 | | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ] |
---|
| 78 | qed. |
---|
| 79 | |
---|
| 80 | lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2). |
---|
| 81 | #A #P #l1 #x #l2 #H elim l1 |
---|
| 82 | [ %1 @H |
---|
| 83 | | #h #t #IH %2 @IH |
---|
| 84 | ] qed. |
---|
| 85 | |
---|
| 86 | lemma Exists_map : ∀A,B,P,Q,f,l. |
---|
| 87 | Exists A P l → |
---|
| 88 | (∀a.P a → Q (f a)) → |
---|
| 89 | Exists B Q (map A B f l). |
---|
| 90 | #A #B #P #Q #f #l elim l // |
---|
| 91 | #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed. |
---|
| 92 | |
---|
[1087] | 93 | lemma map_append : ∀A,B,f,l1,l2. |
---|
| 94 | (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). |
---|
| 95 | #A #B #f #l1 elim l1 |
---|
| 96 | [ #l2 @refl |
---|
| 97 | | #h #t #IH #l2 normalize // |
---|
[1102] | 98 | ] qed. |
---|
[1197] | 99 | |
---|
| 100 | let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝ |
---|
| 101 | match l with |
---|
| 102 | [ nil ⇒ None B |
---|
| 103 | | cons h t ⇒ |
---|
| 104 | match f h with |
---|
| 105 | [ None ⇒ find A B f t |
---|
| 106 | | Some b ⇒ Some B b |
---|
| 107 | ] |
---|
| 108 | ]. |
---|