2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
8 \ / This file is distributed under the terms of the
9 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "basics/types.ma".
13 include "arithmetics/nat.ma".
15 inductive list (A:Type[0]) : Type[0] :=
17 | cons: A -> list A -> list A.
19 notation "hvbox(hd break :: tl)"
20 right associative with precedence 47
23 notation "[ list0 term 19 x sep ; ]"
24 non associative with precedence 90
25 for ${fold right @'nil rec acc @{'cons $x $acc}}.
27 notation "hvbox(l1 break @ l2)"
28 right associative with precedence 47
29 for @{'append $l1 $l2 }.
31 interpretation "nil" 'nil = (nil ?).
32 interpretation "cons" 'cons hd tl = (cons ? hd tl).
34 definition is_nil: ∀A:Type[0].list A → Prop ≝
35 λA.λl.match l with [ nil ⇒ True | cons hd tl ⇒ False ].
38 ∀A:Type[0].∀l:list A.∀a:A. a::l ≠ [].
39 #A #l #a @nmk #Heq (change with (is_nil ? (a::l))) >Heq //
43 let rec id_list A (l: list A) on l :=
46 | (cons hd tl) => hd :: id_list A tl ]. *)
48 let rec append A (l1: list A) l2 on l1 ≝
51 | cons hd tl ⇒ hd :: append A tl l2 ].
53 definition hd ≝ λA.λl: list A.λd:A.
54 match l with [ nil ⇒ d | cons a _ ⇒ a].
56 definition tail ≝ λA.λl: list A.
57 match l with [ nil ⇒ [] | cons hd tl ⇒ tl].
59 definition option_hd ≝
60 λA.λl:list A. match l with
62 | cons a _ ⇒ Some ? a ].
64 interpretation "append" 'append l1 l2 = (append ? l1 l2).
66 theorem append_nil: ∀A.∀l:list A.l @ [] = l.
67 #A #l (elim l) normalize // qed.
69 theorem associative_append:
70 ∀A.associative (list A) (append A).
71 #A #l1 #l2 #l3 (elim l1) normalize // qed.
73 theorem append_cons:∀A.∀a:A.∀l,l1.l@(a::l1)=(l@[a])@l1.
74 #A #a #l #l1 >associative_append // qed.
76 theorem nil_append_elim: ∀A.∀l1,l2: list A.∀P:?→?→Prop.
77 l1@l2=[] → P (nil A) (nil A) → P l1 l2.
78 #A #l1 #l2 #P (cases l1) normalize //
82 theorem nil_to_nil: ∀A.∀l1,l2:list A.
83 l1@l2 = [] → l1 = [] ∧ l2 = [].
84 #A #l1 #l2 #isnil @(nil_append_elim A l1 l2) /2/
87 lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2.
88 #A #a1 #a2 #l1 #l2 #Heq destruct //
91 lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2.
92 #A #a1 #a2 #l1 #l2 #Heq destruct //
97 lemma compare_append : ∀A,l1,l2,l3,l4. l1@l2 = l3@l4 →
98 ∃l:list A.(l1 = l3@l ∧ l4=l@l2) ∨ (l3 = l1@l ∧ l2=l@l4).
100 [#l2 #l3 #l4 #Heq %{l3} %2 % // @Heq
101 |#a1 #tl1 #Hind #l2 #l3 cases l3
102 [#l4 #Heq %{(a1::tl1)} %1 % // @sym_eq @Heq
103 |#a3 #tl3 #l4 normalize in ⊢ (%→?); #Heq cases (Hind l2 tl3 l4 ?)
104 [#l * * #Heq1 #Heq2 %{l}
105 [%1 % // >Heq1 >(cons_injective_l ????? Heq) //
106 |%2 % // >Heq1 >(cons_injective_l ????? Heq) //
108 |@(cons_injective_r ????? Heq)
113 (**************************** iterators ******************************)
115 let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝
116 match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)].
118 lemma map_append : ∀A,B,f,l1,l2.
119 (map A B f l1) @ (map A B f l2) = map A B f (l1@l2).
122 | #h #t #IH #l2 normalize //
125 let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝
126 match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)].
130 foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T).
132 (* compose f [a1;...;an] [b1;...;bm] =
133 [f a1 b1; ... ;f an b1; ... ;f a1 bm; f an bm] *)
135 definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2.
136 foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1.
138 lemma filter_true : ∀A,l,a,p. p a = true →
139 filter A p (a::l) = a :: filter A p l.
140 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
142 lemma filter_false : ∀A,l,a,p. p a = false →
143 filter A p (a::l) = filter A p l.
144 #A #l #a #p #pa (elim l) normalize >pa normalize // qed.
146 theorem eq_map : ∀A,B,f,g,l. (∀x.f x = g x) → map A B f l = map A B g l.
147 #A #B #f #g #l #eqfg (elim l) normalize // qed.
149 (**************************** reverse *****************************)
150 let rec rev_append S (l1,l2:list S) on l1 ≝
153 | cons a tl ⇒ rev_append S tl (a::l2)
157 definition reverse ≝λS.λl.rev_append S l [].
159 lemma reverse_single : ∀S,a. reverse S [a] = [a].
162 lemma rev_append_def : ∀S,l1,l2.
163 rev_append S l1 l2 = (reverse S l1) @ l2 .
164 #S #l1 elim l1 normalize //
167 lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a].
168 #S #a #l whd in ⊢ (??%?); //
171 lemma reverse_append: ∀S,l1,l2.
172 reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
173 #S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >reverse_cons
174 >reverse_cons // qed.
176 lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l.
177 #S #l elim l // #a #tl #Hind >reverse_cons >reverse_append
180 (* an elimination principle for lists working on the tail;
181 useful for strings *)
182 lemma list_elim_left: ∀S.∀P:list S → Prop. P (nil S) →
183 (∀a.∀tl.P tl → P (tl@[a])) → ∀l. P l.
184 #S #P #Pnil #Pstep #l <(reverse_reverse … l)
185 generalize in match (reverse S l); #l elim l //
186 #a #tl #H >reverse_cons @Pstep //
189 (**************************** length ******************************)
191 let rec length (A:Type[0]) (l:list A) on l ≝
194 | cons a tl ⇒ S (length A tl)].
196 interpretation "list length" 'card l = (length ? l).
198 lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l).
202 lemma length_append: ∀A.∀l1,l2:list A.
204 #A #l1 elim l1 // normalize /2/
207 lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l.
208 #A #B #l #f elim l // #a #tl #Hind normalize //
211 lemma length_reverse: ∀A.∀l:list A.
213 #A #l elim l // #a #l0 #IH >reverse_cons >length_append normalize //
216 lemma lenght_to_nil: ∀A.∀l:list A.
218 #A * // #a #tl normalize #H destruct
221 (****************** traversing two lists in parallel *****************)
223 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:list T1 → list T2 → Prop.
224 length ? l1 = length ? l2 →
226 (∀tl1,tl2,hd1,hd2. P tl1 tl2 → P (hd1::tl1) (hd2::tl2)) →
228 #T1 #T2 #l1 #l2 #P #Hl #Pnil #Pcons
229 generalize in match Hl; generalize in match l2;
231 [#l2 cases l2 // normalize #t2 #tl2 #H destruct
232 |#t1 #tl1 #IH #l2 cases l2
233 [normalize #H destruct
234 |#t2 #tl2 #H @Pcons @IH normalize in H; destruct // ]
239 ∀T1,T2:Type[0].∀l1:list T1.∀l2:list T2.∀P:Prop.
240 length ? l1 = length ? l2 →
241 (l1 = [] → l2 = [] → P) →
242 (∀hd1,hd2,tl1,tl2.l1 = hd1::tl1 → l2 = hd2::tl2 → P) → P.
243 #T1 #T2 #l1 #l2 #P #Hl @(list_ind2 … Hl)
244 [ #Pnil #Pcons @Pnil //
245 | #tl1 #tl2 #hd1 #hd2 #IH1 #IH2 #Hp @Hp // ]
248 (*********************** properties of append ***********************)
249 lemma append_l1_injective :
250 ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l1 = l2.
251 #a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) //
252 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct @eq_f /2/
255 lemma append_l2_injective :
256 ∀A.∀l1,l2,l3,l4:list A. |l1| = |l2| → l1@l3 = l2@l4 → l3 = l4.
257 #a #l1 #l2 #l3 #l4 #Hlen @(list_ind2 … Hlen) normalize //
258 #tl1 #tl2 #hd1 #hd2 #IH normalize #Heq destruct /2/
261 lemma append_l1_injective_r :
262 ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l1 = l2.
263 #a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
264 >reverse_append >reverse_append #Heq1
265 lapply (append_l2_injective … Heq1) [ // ] #Heq2
266 lapply (eq_f … (reverse ?) … Heq2) //
269 lemma append_l2_injective_r :
270 ∀A.∀l1,l2,l3,l4:list A. |l3| = |l4| → l1@l3 = l2@l4 → l3 = l4.
271 #a #l1 #l2 #l3 #l4 #Hlen #Heq lapply (eq_f … (reverse ?) … Heq)
272 >reverse_append >reverse_append #Heq1
273 lapply (append_l1_injective … Heq1) [ // ] #Heq2
274 lapply (eq_f … (reverse ?) … Heq2) //
277 lemma length_rev_append: ∀A.∀l,acc:list A.
278 |rev_append ? l acc| = |l|+|acc|.
279 #A #l elim l // #a #tl #Hind normalize
280 #acc >Hind normalize //
283 (****************************** mem ********************************)
284 let rec mem A (a:A) (l:list A) on l ≝
287 | cons hd tl ⇒ a=hd ∨ mem A a tl
290 lemma mem_append: ∀A,a,l1,l2.mem A a (l1@l2) →
291 mem ? a l1 ∨ mem ? a l2.
296 |#Hmema cases (Hind ? Hmema) -Hmema #Hmema [%1 %2 //|%2 //]
301 lemma mem_append_l1: ∀A,a,l1,l2.mem A a l1 → mem A a (l1@l2).
302 #A #a #l1 #l2 elim l1
303 [whd in ⊢ (%→?); @False_ind
304 |#b #tl #Hind * [#eqab %1 @eqab |#Hmema %2 @Hind //]
308 lemma mem_append_l2: ∀A,a,l1,l2.mem A a l2 → mem A a (l1@l2).
309 #A #a #l1 #l2 elim l1 [//|#b #tl #Hind #Hmema %2 @Hind //]
312 lemma mem_single: ∀A,a,b. mem A a [b] → a=b.
313 #A #a #b * // @False_ind
316 lemma mem_map: ∀A,B.∀f:A→B.∀l,b.
317 mem ? b (map … f l) → ∃a. mem ? a l ∧ f a = b.
319 [#b normalize @False_ind
320 |#a #tl #Hind #b normalize *
321 [#eqb @(ex_intro … a) /3/
322 |#memb cases (Hind … memb) #a * #mema #eqb
328 lemma mem_map_forward: ∀A,B.∀f:A→B.∀a,l.
329 mem A a l → mem B (f a) (map ?? f l).
330 #A #B #f #a #l elim l
331 [normalize @False_ind
333 [#eqab <eqab normalize %1 % |#memtl normalize %2 @Hind @memtl]
337 (***************************** split *******************************)
338 let rec split_rev A (l:list A) acc n on n ≝
343 |cons a tl ⇒ split_rev A tl (a::acc) m
347 definition split ≝ λA,l,n.
348 let 〈l1,l2〉 ≝ split_rev A l [] n in 〈reverse ? l1,l2〉.
350 lemma split_rev_len: ∀A,n,l,acc. n ≤ |l| →
351 |\fst (split_rev A l acc n)| = n+|acc|.
352 #A #n elim n // #m #Hind *
353 [normalize #acc #Hfalse @False_ind /2/
354 |#a #tl #acc #Hlen normalize >Hind
355 [normalize // |@le_S_S_to_le //]
359 lemma split_len: ∀A,n,l. n ≤ |l| →
360 |\fst (split A l n)| = n.
361 #A #n #l #Hlen normalize >(eq_pair_fst_snd ?? (split_rev …))
362 normalize >length_reverse >(split_rev_len … [ ] Hlen) normalize //
365 lemma split_rev_eq: ∀A,n,l,acc. n ≤ |l| →
367 reverse ? (\fst (split_rev A l acc n))@(\snd (split_rev A l acc n)).
370 [#acc whd in ⊢ ((??%)→?); #False_ind /2/
371 |#a #tl #acc #Hlen >append_cons <reverse_single <reverse_append
372 @(Hind tl) @le_S_S_to_le @Hlen
376 lemma split_eq: ∀A,n,l. n ≤ |l| →
377 l = (\fst (split A l n))@(\snd (split A l n)).
378 #A #n #l #Hlen change with ((reverse ? [ ])@l) in ⊢ (??%?);
379 >(split_rev_eq … Hlen) normalize
380 >(eq_pair_fst_snd ?? (split_rev A l [] n)) %
383 lemma split_exists: ∀A,n.∀l:list A. n ≤ |l| →
384 ∃l1,l2. l = l1@l2 ∧ |l1| = n.
385 #A #n #l #Hlen @(ex_intro … (\fst (split A l n)))
386 @(ex_intro … (\snd (split A l n))) % /2/
389 (****************************** flatten ******************************)
390 definition flatten ≝ λA.foldr (list A) (list A) (append A) [].
392 lemma flatten_to_mem: ∀A,n,l,l1,l2.∀a:list A. 0 < n →
393 (∀x. mem ? x l → |x| = n) → |a| = n → flatten ? l = l1@a@l2 →
394 (∃q.|l1| = n*q) → mem ? a l.
396 [normalize #l1 #l2 #a #posn #Hlen #Ha #Hnil @False_ind
397 cut (|a|=0) [@sym_eq @le_n_O_to_eq
398 @(transitive_le ? (|nil A|)) // >Hnil >length_append >length_append //] /2/
399 |#hd #tl #Hind #l1 #l2 #a #posn #Hlen #Ha
400 whd in match (flatten ??); #Hflat * #q cases q
402 cut (a = hd) [>(lenght_to_nil… Hl1) in Hflat;
403 whd in ⊢ ((???%)→?); #Hflat @sym_eq @(append_l1_injective … Hflat)
406 |#q1 #Hl1 lapply (split_exists … n l1 ?) //
407 * #l11 * #l12 * #Heql1 #Hlenl11 %2
408 @(Hind l12 l2 … posn ? Ha)
409 [#x #memx @Hlen %2 //
410 |@(append_l2_injective ? hd l11)
412 |>Hflat >Heql1 >associative_append %
414 |@(ex_intro …q1) @(injective_plus_r n)
415 <Hlenl11 in ⊢ (??%?); <length_append <Heql1 >Hl1 //
421 (****************************** nth ********************************)
422 let rec nth n (A:Type[0]) (l:list A) (d:A) ≝
425 |S m ⇒ nth m A (tail A l) d].
427 lemma nth_nil: ∀A,a,i. nth i A ([]) a = a.
428 #A #a #i elim i normalize //
431 (****************************** nth_opt ********************************)
432 let rec nth_opt (A:Type[0]) (n:nat) (l:list A) on l : option A ≝
435 | cons h t ⇒ match n with [ O ⇒ Some ? h | S m ⇒ nth_opt A m t ]
438 (**************************** All *******************************)
440 let rec All (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
443 | cons h t ⇒ P h ∧ All A P t
446 lemma All_mp : ∀A,P,Q. (∀a.P a → Q a) → ∀l. All A P l → All A Q l.
447 #A #P #Q #H #l elim l normalize //
451 lemma All_nth : ∀A,P,n,l.
454 nth_opt A n l = Some A a →
457 [ * [ #_ #a #E whd in E:(??%?); destruct
458 | #hd #tl * #H #_ #a #E whd in E:(??%?); destruct @H
461 [ #_ #a #E whd in E:(??%?); destruct
462 | #hd #tl * #_ whd in ⊢ (? → ∀_.??%? → ?); @IH
466 lemma All_append: ∀A,P,l1,l2. All A P l1 → All A P l2 → All A P (l1@l2).
467 #A #P #l1 elim l1 -l1 //
468 #a #l1 #IHl1 #l2 * /3 width=1/
471 lemma All_inv_append: ∀A,P,l1,l2. All A P (l1@l2) → All A P l1 ∧ All A P l2.
472 #A #P #l1 elim l1 -l1 /2 width=1/
473 #a #l1 #IHl1 #l2 * #Ha #Hl12
474 elim (IHl1 … Hl12) -IHl1 -Hl12 /3 width=1/
477 (**************************** Allr ******************************)
479 let rec Allr (A:Type[0]) (R:relation A) (l:list A) on l : Prop ≝
482 | cons a1 l ⇒ match l with [ nil ⇒ True | cons a2 _ ⇒ R a1 a2 ∧ Allr A R l ]
485 lemma Allr_fwd_append_sn: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l1.
486 #A #R #l1 elim l1 -l1 // #a1 * // #a2 #l1 #IHl1 #l2 * /3 width=2/
489 lemma Allr_fwd_cons: ∀A,R,a,l. Allr A R (a::l) → Allr A R l.
490 #A #R #a * // #a0 #l * //
493 lemma Allr_fwd_append_dx: ∀A,R,l1,l2. Allr A R (l1@l2) → Allr A R l2.
494 #A #R #l1 elim l1 -l1 // #a1 #l1 #IHl1 #l2 #H
495 lapply (Allr_fwd_cons … (l1@l2) H) -H /2 width=1/
498 (**************************** Exists *******************************)
500 let rec Exists (A:Type[0]) (P:A → Prop) (l:list A) on l : Prop ≝
503 | cons h t ⇒ (P h) ∨ (Exists A P t)
506 lemma Exists_append : ∀A,P,l1,l2.
507 Exists A P (l1 @ l2) → Exists A P l1 ∨ Exists A P l2.
512 | #H cases (IH l2 H) /3/
516 lemma Exists_append_l : ∀A,P,l1,l2.
517 Exists A P l1 → Exists A P (l1@l2).
518 #A #P #l1 #l2 elim l1
526 lemma Exists_append_r : ∀A,P,l1,l2.
527 Exists A P l2 → Exists A P (l1@l2).
528 #A #P #l1 #l2 elim l1
530 | #h #t #IH #H %2 @IH @H
533 lemma Exists_add : ∀A,P,l1,x,l2. Exists A P (l1@l2) → Exists A P (l1@x::l2).
534 #A #P #l1 #x #l2 elim l1
536 | #h #t #IH normalize * [ #H %1 @H | #H %2 @IH @H ]
539 lemma Exists_mid : ∀A,P,l1,x,l2. P x → Exists A P (l1@x::l2).
540 #A #P #l1 #x #l2 #H elim l1
545 lemma Exists_map : ∀A,B,P,Q,f,l.
548 Exists B Q (map A B f l).
549 #A #B #P #Q #f #l elim l //
550 #h #t #IH * [ #H #F %1 @F @H | #H #F %2 @IH [ @H | @F ] ] qed.
552 lemma Exists_All : ∀A,P,Q,l.
556 #A #P #Q #l elim l [ * | #hd #tl #IH * [ #H1 * #H2 #_ %{hd} /2/ | #H1 * #_ #H2 @IH // ]
559 (**************************** fold *******************************)
561 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 ≝
565 if p a then op (f a) (fold A B op b p f l)
566 else fold A B op b p f l].
568 notation "\fold [ op , nil ]_{ ident i ∈ l | p} f"
570 for @{'fold $op $nil (λ${ident i}. $p) (λ${ident i}. $f) $l}.
572 notation "\fold [ op , nil ]_{ident i ∈ l } f"
574 for @{'fold $op $nil (λ${ident i}.true) (λ${ident i}. $f) $l}.
576 interpretation "\fold" 'fold op nil p f l = (fold ? ? op nil p f l).
579 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A→B. p a = true →
580 \fold[op,nil]_{i ∈ a::l| p i} (f i) =
581 op (f a) \fold[op,nil]_{i ∈ l| p i} (f i).
582 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
585 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f.
586 p a = false → \fold[op,nil]_{i ∈ a::l| p i} (f i) =
587 \fold[op,nil]_{i ∈ l| p i} (f i).
588 #A #B #a #l #p #op #nil #f #pa normalize >pa // qed.
591 ∀A,B.∀a:A.∀l.∀p.∀op:B→B→B.∀nil.∀f:A →B.
592 \fold[op,nil]_{i ∈ l| p i} (f i) =
593 \fold[op,nil]_{i ∈ (filter A p l)} (f i).
594 #A #B #a #l #p #op #nil #f elim l //
595 #a #tl #Hind cases(true_or_false (p a)) #pa
596 [ >filter_true // > fold_true // >fold_true //
597 | >filter_false // >fold_false // ]
600 record Aop (A:Type[0]) (nil:A) : Type[0] ≝
602 nill:∀a. op nil a = a;
603 nilr:∀a. op a nil = a;
604 assoc: ∀a,b,c.op a (op b c) = op (op a b) c
607 theorem fold_sum: ∀A,B. ∀I,J:list A.∀nil.∀op:Aop B nil.∀f.
608 op (\fold[op,nil]_{i∈I} (f i)) (\fold[op,nil]_{i∈J} (f i)) =
609 \fold[op,nil]_{i∈(I@J)} (f i).
610 #A #B #I #J #nil #op #f (elim I) normalize
611 [>nill //|#a #tl #Hind <assoc //]
614 (********************** lhd and ltl ******************************)
616 let rec lhd (A:Type[0]) (l:list A) n on n ≝ match n with
618 | S n ⇒ match l with [ nil ⇒ nil … | cons a l ⇒ a :: lhd A l n ]
621 let rec ltl (A:Type[0]) (l:list A) n on n ≝ match n with
623 | S n ⇒ ltl A (tail … l) n
626 lemma lhd_nil: ∀A,n. lhd A ([]) n = [].
630 lemma ltl_nil: ∀A,n. ltl A ([]) n = [].
631 #A #n elim n normalize //
634 lemma lhd_cons_ltl: ∀A,n,l. lhd A l n @ ltl A l n = l.
636 #n #IHn #l elim l normalize //
639 lemma length_ltl: ∀A,n,l. |ltl A l n| = |l| - n.
641 #n #IHn *; normalize /2/
644 (********************** find ******************************)
645 let rec find (A,B:Type[0]) (f:A → option B) (l:list A) on l : option B ≝
650 [ None ⇒ find A B f t
655 (********************** position_of ******************************)
656 let rec position_of_aux (A:Type[0]) (found: A → bool) (l:list A) (acc:nat) on l : option nat ≝
660 match found h with [true ⇒ Some … acc | false ⇒ position_of_aux … found t (S acc)]].
662 definition position_of: ∀A:Type[0]. (A → bool) → list A → option nat ≝
663 λA,found,l. position_of_aux A found l 0.
666 (********************** make_list ******************************)
667 let rec make_list (A:Type[0]) (a:A) (n:nat) on n : list A ≝
670 | S m ⇒ a::(make_list A a m)