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/finset.ma".
14 record Vector (A:Type[0]) (n:nat): Type[0] ≝
19 definition vec_tail ≝ λA.λn.λv:Vector A n.
20 mk_Vector A (pred n) (tail A v) ?.
21 >length_tail >(len A n v) //
24 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
25 mk_Vector A (S n) (cons A a v) ?.
26 normalize >(len A n v) //
29 definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
30 mk_Vector A (n1+n2) (v1@v2).
32 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
33 mk_Vector B n (map ?? f v)
34 (trans_eq … (length_map …) (len A n v)).
36 let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
42 |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
46 lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
47 length C (pmap A B C f l1 l2) =
48 min (length A l1) (length B l2).
49 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
50 #b #tlB lapply (Hind tlB) normalize
51 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
55 definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
56 mk_Vector C n (pmap A B C f vA vB) ?.
57 >length_pmap >(len A n vA) >(len B n vB) normalize
58 >(le_to_leb_true … (le_n n)) //