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 lemma Vector_of_list ≝ λA,l.
20 mk_Vector A (|l|) l (refl ??).
22 lemma Vector_eq : ∀A,n,v1,v2.
23 vec A n v1 = vec A n v2 → v1 = v2.
24 #A #n * #l1 #H1 * #l2 #H2 #eql1l2 generalize in match H1;
28 definition vec_tail ≝ λA.λn.λv:Vector A n.
29 mk_Vector A (pred n) (tail A v) ?.
30 >length_tail >(len A n v) //
33 definition vec_cons ≝ λA.λa.λn.λv:Vector A n.
34 mk_Vector A (S n) (cons A a v) ?.
35 normalize >(len A n v) //
38 definition vec_hd ≝ λA.λn.λv:Vector A (S n).
39 hd A v ?. elim v * [normalize #H destruct | #a #H #eq @a]
42 lemma vec_expand: ∀A,n,v.
43 v = vec_cons A (vec_hd A n v) n (vec_tail A (S n) v).
44 #A #n * #l cases l [normalize in ⊢ (%→?); #H destruct |//]
47 lemma vector_nil: ∀A.∀v:Vector A 0.
48 v = mk_Vector A 0 (nil A) (refl ??).
49 #A * * // #a #tl normalize #H destruct
52 definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2.
53 mk_Vector A (n1+n2) (v1@v2).
55 definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n.
56 mk_Vector B n (map ?? f v)
57 (trans_eq … (length_map …) (len A n v)).
59 lemma nth_default : ∀A,i,n.∀v:Vector A n.∀d1,d2. i < n →
60 nth i ? v d1 = nth i ? v d2.
62 [#n #v #d1 #d2 #ltOn lapply v @(lt_O_n_elim … ltOn)
63 -v #m #v >(vec_expand … v) //
64 |#i #Hind #n #v #d1 #d2 #ltn lapply ltn lapply v @(lt_O_n_elim … (ltn_to_ltO … ltn))
65 -v -ltn #m #v #ltim >(vec_expand … v) @(Hind m (vec_tail A (S m) v) d1 d2 ?)
70 lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d.
71 (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2.
73 [#v1 #v2 #H >(vector_nil A v1) >(vector_nil A v2) //
74 |#n #Hind #v1 #v2 #d #H >(vec_expand … v1) >(vec_expand … v2)
75 >(Hind (vec_tail … v1) (vec_tail … v2) d)
76 [cut (vec_hd A n v1 = vec_hd A n v2) //
77 cut (∀i,d1,d2. i < S n → nth i A v1 d1 = nth i A v2 d2)
78 [#i #d1 #d2 #Hi >(nth_default ????? d) // >(nth_default ???? d2 d) // @H //]
80 |#i #ltin @(H (S i)) @le_S_S //
86 ∀A,B,f,i,n.∀v:Vector A n.∀d.
87 f (nth i ? v d) = nth i ? (vec_map A B f n v) (f d).
90 [ #v #d >(vector_nil … v) %
91 | #n0 #v #d >(vec_expand … v) % ]
93 [ #v #d >(vector_nil … v) normalize cases i0 //
94 | #n #v #d >(vec_expand … v) whd in ⊢ (??(?%)%);
95 >(IH n (vec_tail A (S n) v) d) % ] ]
99 (* mapi: map with index to move in list.ma *)
100 let rec change_vec (A:Type[0]) (n:nat) on n ≝
101 match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with
105 [ O ⇒ vec_cons A a m (vec_tail … v)
106 | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j)
110 lemma nth_change_vec : ∀A,i,n,v,a,d. i < n →
111 nth i ? (change_vec A n v a i) d = a.
113 [#n #v #a #d #ltOn lapply v -v @(lt_O_n_elim n ltOn ??) //
114 |#m #Hind #n #v #a #d #Hlt
115 lapply Hlt lapply v @(lt_O_n_elim … (ltn_to_ltO … Hlt))
116 #p #v #ltmp @Hind @le_S_S_to_le //
120 lemma nth_change_vec_neq : ∀A,j,i,n,v,a,d. i ≠ j →
121 nth j ? (change_vec A n v a i) d = nth j ? v d.
123 [#i * // #n #v #a #d cases i
124 [#H @False_ind @(absurd ?? H) //
125 |#i0 #_ >(vec_expand ?? v) in ⊢ (???%); //
127 |#m #Hind #i * // cases i // #i0 #n #v #a #d #neqim
128 whd in ⊢(??%?); whd in match (tail ??); >Hind
129 [>(vec_expand ??v) in ⊢ (???%); // |@(not_to_not … neqim) // ]
133 lemma change_vec_same : ∀sig,n,v,i,d.
134 change_vec sig n v (nth i ? v d) i = v.
135 #sig #n #v #i #d @(eq_vec … d)
136 #i0 #Hi0 cases (decidable_eq_nat i i0) #Hi0
137 [ >Hi0 >nth_change_vec //
138 | >nth_change_vec_neq //
142 lemma change_vec_cons_tail :∀A,n,vA,a,b,i.
143 change_vec A (S n) (vec_cons ? a n vA) b (S i) =
144 vec_cons ? a n (change_vec A n vA b i).
145 #A #n #vA cases vA //
148 lemma change_vec_commute : ∀A,n,v,a,b,i,j. i ≠ j →
149 change_vec A n (change_vec A n v a i) b j
150 = change_vec A n (change_vec A n v b j) a i.
151 #A #n #v #a #b #i #j #Hij @(eq_vec … a)
152 #k #Hk cases (decidable_eq_nat k i) #Hki
153 [ >Hki >nth_change_vec // >(nth_change_vec_neq ??????? (sym_not_eq … Hij))
155 | cases (decidable_eq_nat k j) #Hkj
156 [ >Hkj >nth_change_vec // >(nth_change_vec_neq ??????? Hij) >nth_change_vec //
157 | >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
158 >(nth_change_vec_neq ??????? (sym_not_eq … Hkj))
159 >(nth_change_vec_neq ??????? (sym_not_eq … Hki))
160 >(nth_change_vec_neq ??????? (sym_not_eq … Hkj)) //
165 lemma change_vec_change_vec : ∀A,n,v,a,b,i.
166 change_vec A n (change_vec A n v a i) b i = change_vec A n v b i.
167 #A #n #v #a #b #i @(eq_vec … a) #i0 #Hi0
168 cases (decidable_eq_nat i i0) #Hii0
169 [ >Hii0 >nth_change_vec // >nth_change_vec //
170 | >nth_change_vec_neq // >nth_change_vec_neq //
171 >nth_change_vec_neq // ]
176 lemma length_make_listi: ∀A,a,n,i.
177 |make_listi A a n i| = n.
178 #A #a #n elim n // #m #Hind normalize //
180 definition change_vec ≝ λA,n,v,a,i.
181 make_veci A (λj.if (eqb i j) then a else (nth j A v a)) n 0.
183 let rec mapi (A,B:Type[0]) (f: nat → A → B) (l:list A) (i:nat) on l: list B ≝
186 | cons x tl ⇒ f i x :: (mapi A B f tl (S i))].
188 lemma length_mapi: ∀A,B,l.∀f:nat→A→B.∀i.
189 |mapi ?? f l i| = |l|.
190 #A #B #l #f elim l // #a #tl #Hind normalize //
193 let rec make_listi (A:Type[0]) (a:nat→A) (n,i:nat) on n : list A ≝
196 | S m ⇒ a i::(make_listi A a m (S i))
199 lemma length_make_listi: ∀A,a,n,i.
200 |make_listi A a n i| = n.
201 #A #a #n elim n // #m #Hind normalize //
204 definition vec_mapi ≝ λA,B.λf:nat→A→B.λn.λv:Vector A n.λi.
205 mk_Vector B n (mapi ?? f v i)
206 (trans_eq … (length_mapi …) (len A n v)).
208 definition make_veci ≝ λA.λa:nat→A.λn,i.
209 mk_Vector A n (make_listi A a n i) (length_make_listi A a n i).
212 let rec pmap A B C (f:A→B→C) l1 l2 on l1 ≝
218 |cons b tlB ⇒ (f a b)::pmap A B C f tlA tlB
222 lemma length_pmap: ∀A,B,C.∀f:A→B→C.∀l1,l2.
223 length C (pmap A B C f l1 l2) =
224 min (length A l1) (length B l2).
225 #A #B #C #f #l1 elim l1 // #a #tlA #Hind #l2 cases l2 //
226 #b #tlB lapply (Hind tlB) normalize
227 cases (true_or_false (leb (length A tlA) (length B tlB))) #H >H
231 definition pmap_vec ≝ λA,B,C.λf:A→B→C.λn.λvA:Vector A n.λvB:Vector B n.
232 mk_Vector C n (pmap A B C f vA vB) ?.
233 >length_pmap >(len A n vA) >(len B n vB) normalize
234 >(le_to_leb_true … (le_n n)) //
237 lemma pmap_vec_cons :∀A,B,C,f,n,vA,vB,a,b.
238 pmap_vec A B C f (S n) (vec_cons ? a n vA) (vec_cons ? b n vB) =
239 vec_cons ? (f a b) n (pmap_vec A B C f n vA vB).
242 lemma pmap_change : ∀A,B,C,f,n,vA,vB,a,b,i.
243 pmap_vec A B C f n (change_vec ? n vA a i) (change_vec ? n vB b i) =
244 change_vec ? n (pmap_vec A B C f n vA vB) (f a b) i.
245 #A #B #C #f #n elim n //
246 #m #Hind #vA #vB #a #b >(vec_expand … vA) >(vec_expand … vB) * //
247 #i >pmap_vec_cons >pmap_vec_cons >change_vec_cons_tail @eq_f @Hind