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 | ]. |
---|
8 | |
---|
9 | let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝ |
---|
10 | match l with |
---|
11 | [ nil ⇒ True |
---|
12 | | cons h t ⇒ P h ∧ All A P t |
---|
13 | ]. |
---|
14 | |
---|
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 | |
---|
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 | |
---|
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) |
---|
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 | |
---|
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 | |
---|
93 | lemma Exists_exists : ∀A,P,l. |
---|
94 | Exists A P l → |
---|
95 | ∃x. P x. |
---|
96 | #A #P #l elim l [ * | #hd #tl #IH * [ #H %{hd} @H | @IH ] |
---|
97 | qed. |
---|
98 | |
---|
99 | lemma Exists_All : ∀A,P,Q,l. |
---|
100 | Exists A P l → |
---|
101 | All A Q l → |
---|
102 | ∃x. P x ∧ Q x. |
---|
103 | #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ] |
---|
104 | qed. |
---|
105 | |
---|
106 | lemma map_append : ∀A,B,f,l1,l2. |
---|
107 | (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). |
---|
108 | #A #B #f #l1 elim l1 |
---|
109 | [ #l2 @refl |
---|
110 | | #h #t #IH #l2 normalize // |
---|
111 | ] qed. |
---|
112 | |
---|
113 | let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝ |
---|
114 | match l with |
---|
115 | [ nil ⇒ None B |
---|
116 | | cons h t ⇒ |
---|
117 | match f h with |
---|
118 | [ None ⇒ find A B f t |
---|
119 | | Some b ⇒ Some B b |
---|
120 | ] |
---|
121 | ]. |
---|