1 include "basics/types.ma".
2 include "basics/nat.ma".
4 inductive list (A:Type[0]) : Type[0] :=
6 | cons: A -> list A -> list A.
8 notation "hvbox(hd break :: tl)"
9 right associative with precedence 47
12 notation "[ list0 x sep ; ]"
13 non associative with precedence 90
14 for ${fold right @'nil rec acc @{'cons $x $acc}}.
16 notation "hvbox(l1 break @ l2)"
17 right associative with precedence 47
18 for @{'append $l1 $l2 }.
20 interpretation "nil" 'nil = (nil ?).
21 interpretation "cons" 'cons hd tl = (cons ? hd tl).
23 definition not_nil: ∀A:Type[0].list A → Prop ≝
24 λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
27 ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
28 #A #l #a @nmk #Heq (change with (not_nil ? (a::l))) >Heq //
32 let rec id_list A (l: list A) on l :=
35 | (cons hd tl) => hd :: id_list A tl ]. *)
37 let rec append A (l1: list A) l2 on l1 ≝
40 | cons hd tl ⇒ hd :: append A tl l2 ].
42 definition hd ≝ λA.λl: list A.λd:A.
43 match l with [ nil ⇒ d | cons a _ ⇒ a].
45 definition tail ≝ λA.λl: list A.
46 match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
48 interpretation "append" 'append l1 l2 = (append ? l1 l2).
50 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
51 #A #l (elim l) normalize // qed.
53 theorem associative_append:
54 ∀A.associative (list A) (append A).
55 #A #l1 #l2 #l3 (elim l1) normalize // qed.
57 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
58 #A #a #l #l1 >associative_append // qed.
60 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
61 l1@l2=[] → P (nil A) (nil A) → P l1 l2.
62 #A #l1 #l2 #P (cases l1) normalize //
66 theorem nil_to_nil: ∀A.∀l1,l2:list A.
67 l1@l2 = [] → l1 = [] ∧ l2 = [].
68 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
71 (**************************** iterators ******************************)
73 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
74 match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
76 lemma map_append : ∀A,B,f,l1,l2.
77 (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
80 | #h #t #IH #l2 normalize //
83 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
84 match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
88 foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
90 (* compose f [a1;...;an] [b1;...;bm] =
91 [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
93 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
94 foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
96 lemma filter_true : ∀A,l,a,p. p a = true →
97 filter A p (a::l) = a :: filter A p l.
98 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
100 lemma filter_false : ∀A,l,a,p. p a = false →
101 filter A p (a::l) = filter A p l.
102 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
104 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
105 #A #B #f #g #l #eqfg (elim l) normalize // qed.
107 (**************************** reverse *****************************)
108 let rec rev_append S (l1,l2:list S) on l1 ≝
111 | cons a tl ⇒ rev_append S tl (a::l2)
115 definition reverse ≝λS.λl.rev_append S l [].
117 lemma reverse_single : ∀S,a. reverse S [a] = [a].
120 lemma rev_append_def : ∀S,l1,l2.
121 rev_append S l1 l2 = (reverse S l1) @ l2 .
122 #S #l1 elim l1 normalize //
125 lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
126 #S #a #l whd in ⊢ (??%?); //
129 lemma reverse_append: ∀S,l1,l2.
130 reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
131 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
132 >reverse_cons // qed.
134 lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
135 #S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
138 (* an elimination principle for lists working on the tail;
139 useful for strings *)
140 lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
141 (∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
142 #S #P #Pnil #Pstep #l <(reverse_reverse … l)
143 generalize in match (reverse S l); #l elim l //
144 #a #tl #H >reverse_cons @Pstep //
147 (**************************** length ******************************)
149 let rec length (A:Type[0]) (l:list A) on l ≝
152 | cons a tl ⇒ S (length A tl)].
154 notation "|M|" non associative with precedence 60 for @{'norm $M}.
155 interpretation "norm" 'norm l = (length ? l).
157 lemma length_append: ∀A.∀l1,l2:list A.
159 #A #l1 elim l1 // normalize /2/
162 (****************************** nth ********************************)
163 let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
166 |S m ⇒ nth m A (tail A l) d].
168 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
169 #A #a #i elim i normalize //
172 (****************************** nth_opt ********************************)
173 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
176 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
179 (**************************** All *******************************)
181 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
184 | cons h t ⇒ P h ∧ All A P t
187 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
188 #A #P #Q #H #l elim l normalize //
192 lemma All_nth : ∀A,P,n,l.
195 nth_opt A n l = Some A a →
198 [ * [ #_ #a #E whd in E:(??%?); destruct
199 | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
202 [ #_ #a #E whd in E:(??%?); destruct
203 | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
207 (**************************** Exists *******************************)
209 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
212 | cons h t ⇒ (P h) ∨ (Exists A P t)
215 lemma Exists_append : ∀A,P,l1,l2.
216 Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
221 | #H cases (IH l2 H) /3/
225 lemma Exists_append_l : ∀A,P,l1,l2.
226 Exists A P l1 → Exists A P (l1@l2).
227 #A #P #l1 #l2 elim l1
235 lemma Exists_append_r : ∀A,P,l1,l2.
236 Exists A P l2 → Exists A P (l1@l2).
237 #A #P #l1 #l2 elim l1
239 | #h #t #IH #H %2 @IH @H
242 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
243 #A #P #l1 #x #l2 elim l1
245 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
248 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
249 #A #P #l1 #x #l2 #H elim l1
254 lemma Exists_map : ∀A,B,P,Q,f,l.
257 Exists B Q (map A B f l).
258 #A #B #P #Q #f #l elim l //
259 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
261 lemma Exists_All : ∀A,P,Q,l.
265 #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
268 (**************************** fold *******************************)
270 let rec fold (A,B:Type[0]) (op:B → B → B) (b:B) (p:A→bool) (f:A→B) (l:list A) on l :B ≝
274 if p a then op (f a) (fold A B op b p f l)
275 else fold A B op b p f l].
277 notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
279 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
281 notation "\fold [ op , nil ]_{ident i ∈ l } f"
283 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
285 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
288 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
289 \fold[op,nil]_{i ∈ a::l| p i} (f i) =
290 op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
291 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
294 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
295 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
296 \fold[op,nil]_{i ∈ l| p i} (f i).
297 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
300 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
301 \fold[op,nil]_{i ∈ l| p i} (f i) =
302 \fold[op,nil]_{i ∈ (filter A p l)} (f i).
303 #A #B #a #l #p #op #nil #f elim l //
304 #a #tl #Hind cases(true_or_false (p a)) #pa
305 [ >filter_true // > fold_true // >fold_true //
306 | >filter_false // >fold_false // ]
309 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
311 nill:∀a. op nil a = a;
312 nilr:∀a. op a nil = a;
313 assoc: ∀a,b,c.op a (op b c) = op (op a b) c
316 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
317 op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
318 \fold[op,nil]_{i∈(I@J)} (f i).
319 #A #B #I #J #nil #op #f (elim I) normalize
320 [>nill //|#a #tl #Hind <assoc //]